Assignment #2

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.

• iii) Play with programming a proof-search (theorem proving) engine.  in other words, implement a function:
  • prove : context * form -> bool
  • return true if a proof exists (the formula is valid according to the inference rules) or false otherwise.
  • instead of programming a general-purpose prover from the get-go, try starting with a small subset of the logic.  For instance, try proving  G |- F where
    • G is a list of basic propositions (Prop s) only
    • and F only involves True, False, /\ and basic propositions
• iv) As an alternative, try to implement a prover that actually constructs a proof object.  After you construct the proof object, you can try your proof checker on it to make sure that your prover did not make a mistake (at least when it says the theorem is true -- to do this, you will want to change your proof checker so that it returns not just true or false, but the actual formula that has been proven).
  • prove : context * form -> proof 
  • prove takes a collection of assumptions (a context) and a formula to try to prove and produces a "proof option".  An option type is either SOME of a value of some type 'a or NONE:

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