Overview

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).

Learning Objectives

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.
  1. Design recipe for generic programs
  2. Design recipe for recursive programs

Getting Started

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
	

What to do

• 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?

What To Turn In

• 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.