Assignment #2

Due by midnight on Monday October 1st.  

For proofs:  Either hand in in class, email to Kenny (kzhu@cs.princeton.edu) or deliver to Kenny's office.  Please put "COS 441 A2" in the subject line of any email.

For code:  email to Kenny (kzhu@cs.princeton.edu) a file named firstlastnameA2.sml where "firstlastname" is your firstname followed by your last name.  eg:

davidwalkerA2.sml

Again, please put "COS 441 A2" in the subject line of any email.

There are 10 points to gain on this assignment.

Here is the definition of intuitionistic propositional logic with implication, conjunction and truth:

 

------------------ hyp

G1, F, G2 |- F

 

 

G,F1 |- F2                    G |- F1 => F2         G |- F1

-----------------  =>I         ---------------------------------- =>E        

G |- F1 => F2                               G |- F2

 

 

G |- F1     G |- F2                G |- F1 /\ F2                   G |- F1 /\ F2 

-----------------------  /\I         ------------------ /\E1          ------------------ /\E2        

G |- F1 /\ F2                           G |- F1                            G |- F2

 

 

-------------  True I             (no elimination rule for true)

G |- True

    

                                                                   G |- False

(no introduction rule for false)                     -------------  False E

                                                                      G |- F

 

 

1.  [2 Points] Prove the following judgements are valid:
    i)  . |- (A /\ (B /\ C)) => ((A /\ B) /\ C)        

    ii) C |- (C => B) => B

 

2.  [3 Points] Prove that this logic obeys the standard Weakening Lemma:

 

Weakening Lemma:  If G |- F  then G,F' |- F.

 

Intuitively, Weakening says that adding extra unnecessary "junk" to the context (such as F') does not prevent us from proving formulas true.  Your proof may use the Exchange Lemma:

 

Exchange Lemma:  If G1,F1,F2,G2 |- F then G1,F2,F1,G2 |- F.

 

You only need to show the cases of your proof for the rules (True I), (hyp), (=>I), (=>E).

 

3. Implement propositional intuitionistic logic formulas:

  • i) [2 points] Represent the syntax of the logical formulas, as defined by the BNF below, using an ML datatype. 

    F ::= s | True | False | F1 => F2 | F1 /\ F2

    • eg:

     

    datatype form =

       PropF of string

    | TrueF

    | ...

    | AndF of form * form

  • ii) [3 points] Implement an ML function to print formulas.

    printform : form -> unit 

    Your solution should insert double-quotes around propositions.  Your solution should insert parentheses everywhere to disambiguate the structure of the formula. eg: 

    ((("N is even") /\ ("N is multiple of 5")) => ("N is multiple of 10"))

    fun printform f =

      case f of

        PropF s => print "\""; print s; print "\""

     | ...

     | AndF (f1,f2) => print "("; printform f1; print "/\"; printform f2; print ")"

    •

     

    Optional, ungraded exercise.  if you would like more practice programming in ML, try the following exercise.  They will not be graded but if you want feedback, you can show them to either Kenny or myself.  A little extra work with ML now might help you on future assignments.

    Implement an improved printer that minimizes the number of parentheses.

  • print_form2 : form -> unit
    •

    A perfect solution will

  • not insert parentheses around atomic formulae (just double quotes).
  • not insert parentheses around a series of conjunctions (since conjunction is associative).  Instead of:
    •

    (("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"

     ("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"

     (("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"