ML Programming Assignment: Unification

Due Wednesday, November 8
Postponed to Friday 10 November


Your assignment is to implement in ML (SML or Caml) term substitutions, term matching and unification, as presented in the slides.

Substitutions, matching and unification operate on the following datatype:

datatype term =
  Var of string
| Symbol of string * (term list);


In Caml, the same datatype definition would be:

type term =
  Var of string
| Symbol of string * (term list);;
For example, the term
Succ(Zero)
would be represented as
Symbol("Succ", [Symbol("Zero",[])])
and
Pair(x, Nothing)
would be represented as
Symbol("Pair", [Var "x", Symbol("Nothing",[])]) in SML
and
Symbol("Pair", [Var "x"; Symbol("Nothing",[])]) in Caml.
You must implement the two functions matches and unify given during the lecture, and their type must be:
matches : term -> term -> substitution
unify : term -> term -> substitution
given an appropriate representation for substitutions.
Also, you must provide a function
compose : substitution -> substitution -> substitution
implementing the composition of substitutions, and
apply : substitution -> term -> term
which applies a substitution to a term.

If you have any question, please post it in the class mailing list.

For your information, my own implementation is 100 lines long (and includes multi-lines comments). Yours shouldn't be much longer...