Due in class on Monday October 10th.
This assignment will serve as an introduction to programming in Standard ML. There are a total of 20 points on this assignment.
Rules for collaboration: You may discuss the problem sets with other students to increase your understanding of the material. However, what you write down and turn in should be your own work.
This problem set is due at midnight on the due date.
1. Implement propositional intuitionistic logic formulas:
eg:
datatype form =
PropF of string
| TrueF
| ...
| AndF of form * form
2. [10 points] Proofs of theorems in intuitionistic logic can be represented using the following ML datatype:
datatype form = ... (* your definition from question 1 *)
datatype proof =
Hyp of form
| TrueI
| AndI of proof * proof
| AndE1 of proof
| AndE2 of proof
| ImpI of form * proof
| ImpE of proof * proof
Your job is to implement a proof checker for intuitionistic logic. You may build on the following definitions. If there are any errors in the following definitions you will obviously have to fix them. If you do not find them convenient, implement your own. If you would like an extra challenge, come up with a more efficient way to represent and manipulate contexts (balanced trees, hash tables, ...).
(* Contexts for proof-checking *)
type context = form list
fun emptyctxt () = [ ]
fun insertctxt ctxt f = f :: ctxt
fun lookupctxt ctxt f =
case ctxt of
[ ] => false
| f1::rest => (f = f1) orelse (lookupctxt f rest)
exception BadProof
(* return true if pf is a valid proof *)
fun check (pf:proof) : bool =
(let _ = aux [] pf in true end) handle BadProof => false
(* helper function for proof checking;
return formula proved by proof or raise BadProof *)
and checkaux (ctxt:context) (pf:proof) : form =
case pf of
Hyp f => if lookupctxt ctxt f then f else (raise BadProof)
| ...
3. Optional, ungraded exercise. if you would like more practice programming in ML, try the following exercises. They will not be graded but if you want feedback, you can show them to either Aquinas or myself. A little extra work with ML now might help you on future assignments.
(("N is even") /\ ("N is multiple of 5")) /\ (("N is a multiple of 3") /\ ("N is multiple of 7"))
print:
"N is even" /\ "N is multiple of 5" /\ "N is a multiple of 3" /\ "N is multiple of 7"
- treat => as left associative. Instead of:
("N is multiple of 5" => ("N is a multiple of 3" => "N is multiple of 7"))
print:
"N is multiple of 5" => "N is a multiple of 3" => "N is multiple of 7"
but still print this formula with parens:
("N is multiple of 5" => "N is a multiple of 3") => "N is multiple of 7"
- give /\ higher precedence than => and only insert parentheses where necessary. Instead of:
(("N is multiple of 5" /\ "N is a multiple of 3") => "N is multiple of 7")
print:
"N is multiple of 5" /\ "N is a multiple of 3" => "N is multiple of 7"
- Suggestion:
- Associate each formula type with an integer precedence (2 for /\ and 1 for =>)
- Implement printform2 by introducing a helper function (printaux (prec,f)) to print formula f. When the top-most connective in f has lower precedence level than prec, print parentheses.
type 'a option = NONE | SOME of 'a
- If the prover can determine that there is no possible proof of some formula (it isn't a valid formula) then that prover should return NONE.
- If the prover can find a proof pf then the prover should return (SOME pf).