In this exercise you will write a tautology checker in Haskell
for the datatype **Prop** found in the library file Prop.hs.

A tautology is a propositional statement that is true for every possible
assignment of all its propositional variables (e.g. **LetterP n**) to true or false.

The strategy for defining your tautology checker is:

- Turn any propositional statement into one with consecutive
integer valued propositional variables (
**alphaRename**). - For a term with n variables generate all possible 2^n assignments
of n variables to true or false (
**assignments**). - Determine if a propositianl statement is true or false under
a single assignment which assigns every variable to either true or false
(
**eval**). - Check the statement againt every possible assignment (
**tautology**).

As you work through this exercise we expect you to learn the following:

- Learn how Haskell defines new datatypes using the
**data**declaration. - Learn to write Haskell functions operating on such datatypes by pattern matching over constructor functions that define data.
- Learn how to study Haskell code written by others to aquire knowledge of writing your own functions.
- Learn to use Haskell Design recipes.

To get started on this problem set you will need the files: (1) Prop.hs, (2) Blocks.hs, and (3) ForwardProver.hs. These are the same files you used in Exercise 1 so you probably already have them. You might want to right click and download fresh copies into your Haskell code directory just in case they have changed.

You will also need the Problem 1 solution stub.
Right click on this link and download a coipy of the stub in your Haskell
code directory. Name the file **<yourname>P1.hs**. The stub looks
like this.

module Assignment1 where import Prop alphaRename :: Eq a => Prop a -> (Prop Int,[(a,Int)]) alphaRename term = (sub pairs term,pairs) where vs = letters term pairs = zip vs [0..] sub :: (Eq t) => [(t, b)] -> Prop t -> Prop b sub pairs (AndP x y) = AndP (sub pairs x) (sub pairs y) sub pairs (OrP x y) = OrP (sub pairs x) (sub pairs y) sub pairs (ImpliesP x y) = ImpliesP (sub pairs x) (sub pairs y) sub pairs (NotP x) = NotP (sub pairs x) sub pairs TruthP = TruthP sub pairs AbsurdP = AbsurdP sub pairs (LetterP x) = case lookup x pairs of Nothing -> error "Unknown LetterP" Just n -> LetterP n assignments :: Int -> [[Bool]] assignments 0 = [] assignments 1 = [[True],[False]] assignments n = undefined eval :: Prop Int -> [Bool] -> Bool eval (LetterP x) assign = assign !! x eval (AndP x y) assign = undefined eval (OrP x y) assign = undefined eval (ImpliesP x y) assign = undefined eval (NotP x) assign = undefined eval TruthP assign = undefined eval AbsurdP assign = undefined tautology :: (Eq a) => Prop a -> Tautology Int tautology term = undefined |
---|

To get you started I have defined a number of functions (**alphaRename** and **sub**)
and partially defined several others (**assignments**, **eval**, and **tautology**).
It's your job to complete the partially defined functions.

A function is
partially defined if it has the token **undefined** in its body.
The token **undefined** is a perfectly fine Haskell expression
and the stub file will compile just as you download it. It won't, of course,
compute any answers until you replace every undefined with working code.

Let's study the fully defined functions, this study should help you complete the partially defined ones. The first fully defined function is alphaRename.

alphaRename :: Eq a => Prop a -> (Prop Int,[(a,Int)]) alphaRename term = (sub pairs term,pairs) where vs = letters term pairs = zip vs [0..]

sub :: (Eq t) => [(t, b)] -> Prop t -> Prop b sub pairs (AndP x y) = AndP (sub pairs x) (sub pairs y) sub pairs (OrP x y) = OrP (sub pairs x) (sub pairs y) sub pairs (ImpliesP x y) = ImpliesP (sub pairs x) (sub pairs y) sub pairs (NotP x) = NotP (sub pairs x) sub pairs TruthP = TruthP sub pairs AbsurdP = AbsurdP sub pairs (LetterP x) = case lookup x pairs of Nothing -> error "Unknown LetterP" Just n -> LetterP n

- Replace all of the
**undefined**tokens with working code. - Define several examples
**ex1**,**ex2**, etc. Each example will be of type**Prop String**. Some examples should be tautologys and some should not. Test each one. - Make an example with 10 different propositional variables. Why does it take so long to test?

- Be sure your name is listed as a comment
in your solution, you have named your solution
P1.hs - Drop it in the ProbSet1 folder in the class drop box
- Be prepared to talk about your solution in class.

Back to the Course Schedule.