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