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