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:

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


    datatype form =

       PropF of string

    | TrueF

    | ...

    | AndF of form * form

  • ii) [8 points] Implement an ML function to print formulas. 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 ")"


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


  • i) Add formulas for False and Disjunction to the datatype and extend your proof checker accordingly.
  • ii) 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"))


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


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


    "N is multiple of 5" /\ "N is a multiple of 3" => "N is multiple of 7"