The program UNIF is an implementation in AlgolW of the algorithm published as:
G. P. HUET, A unification algorithm for typed lambda-calculus, Theoretical Computer Science 1 (1975) 27-57.
As in the article, lambda terms are represented in head normal form: *x1x2...xn.h(e1,e2,... ep) (n >= 0, p >= 0) x1 x2 ... xn are different variables, h is a variable or a constant e1 e2 ... en are terms
- stands for lambda
variables are x y z u v w f g h optionally followed by an integer constants start with other letters. Every atom is given with its type. Atomic types are i and o Functional types are (t1, ..., tk - a) where a is an atomic type, standing for (t1 -> (t2 -> ... -> (tk -> a)...)) in the usual notation.
The program starts by asking for a list of pairs of terms to unify, and for each term asks fot the type of its atoms. When the list is finished (answer n to query "any more pairs?"), the program asks for an integer used as a bound to the number of nodes of the spanning tree. It then enumerates the tree of solutions, within this limit.
The following gives the complete transcript of a session, corresponding to exemple 3.5.3 in the paper. The nodes in the tree are named NULL for the root, RCCLxy.z for others.
=================================================================== PAIR NO 1 FIRST TERM ENTER YOUR TERM: x
ENTER TYPE OF ATOM :X (((i-i),i,i-i)-i)
SECOND TERM ENTER YOUR TERM: *u.u(*v.w,x(*u1v1w1.a(u1(v1),w1)),x(f))
ENTER TYPE OF ATOM :U ((i-i),i,i-i)-i)
ENTER TYPE OF ATOM :V i
ENTER TYPE OF ATOM :W i
ENTER TYPE OF ATOM : U1 (i-i)
ENTER TYPE OF ATOM : V1 i
ENTER TYPE OF ATOM : W1 i
ENTER TYPE OF ATOM : A (i,i-i)
ENTER TYPE OF ATOM : F ((i-i),i,i-i)
ANY MORE PAIRS ALLOWED ? n
HOW MANY NODES ALLOWED ? 10
RCCL08.1 FOLLOWS NULL