We assume that you have succeeded in installing the Haskell Platform from haskell.org/downloads.
The code that goes with the first lecture can be found in LFPMC.hs.
You should download this file, and also the file with the code of these exercises: Exercises1.hs. Use the definitions in your solutions to the exercises. For this you should insert your own Haskell definitions in your own copy of the file. Next load the file with the Haskell interpreter and check whether your definitions compile and work as expected.
> module Exercises1 where
> import LFPMC
Write implementations of
contradiction :: Form -> Bool
tautology :: Form -> Bool
-- logical entailment
entails :: Form -> Form -> Bool
-- logical equivalence
equiv :: Form -> Form -> Bool
Next, check your definitions for correctness.
Here is a function for generating the list of all sublists of a given list:
> powlist :: Eq a => [a] -> [[a]]
> powlist [] = [[]]
> powlist (x:xs) = powlist xs ++ map (x:) (powlist xs)
Your task is to check whether this definition generates the expected number of sublists:
Check that if the elements of xs
are all different, then the lists in the output of powlist xs
are all different.
Check that if xs
has n elements, all different, then powlist xs
has 2n elements, all different.
Let's consider an alternative way to define valuations. If the domain of propositions props
is clear, valuations can be given as sublists of props
.
Use this to define the list of all valuations for a given formula. You should use powlist
from the previous exercise.
allVls :: Form -> [[Name]]
Give a function that takes a domain props
of propositions and a sublist of that domain, and produces a valuation (an object of type Valuation
).
The type of the conversion function is
names2valuation :: ([Name],[Name]) -> Valuation
Next, give a conversion function in the other direction.
valuation2names :: Valuation -> ([Name],[Name])
The first element of the output pair should give the domain, the second element the appropriate sublist.
How can you check that the two functions are inverses?
Use the valuations of type [Name]
that you defined in a previous exercise to define an alternative evaluation function that evaluates with respect to a valuation of type . The type is:
evl :: [Name] -> Form -> Bool
Let's give an alternative definition of formulas that also has box and diamond formulas:
> data Frm = Prp Name
> | Ng Frm
> | Cj [Frm]
> | Dj [Frm]
> | Imp Frm Frm
> | Eqv Frm Frm
> | Box Frm
> | Diam Frm
> deriving Eq
Think of Box
and Diam
as S5 modalities.
These can be evaluated on non-empty lists of valuations.
Write a function
s5eval :: [[Name]] -> Frm -> Bool
that does this. Take the first element of the list of valuations as the current world.
Here are some examples: you should get
s5eval [[0],[0,1]] (Box (Prp 0))
equals True
,
s5eval [[0],[0,1]] (Box (Prp 1))
equals False
s5eval [[0],[0,1]] (Prp 1)
equals False
,
s5eval [[0],[0,1]] (Prp 0)
equals True
, and so on.
Finally, implement update with formulas that contain boxes and diamonds.
upd :: Frm -> [[Name]] -> [[Name]]
upds :: [Frm] -> [[Name]] -> [[Name]]
Give an example that makes clear that updates for the s5 language are no longer commutative.
Historical reference: this is the update system proposed by Frank Veltman in (Veltman 1996).
Veltman, F. 1996. “Defaults in Update Semantics.” Journal of Philosophical Logic, 221–61.