;;; -*- Mode:Text; -*-
;;; ************************************************************************
;;; FLAIR PROJECT
;;; ************************************************************************
;;; Filename:   unify.pseudo
;;; ========================================================================
;;; The UNIFICATION ALGORITHM.
;;; It is derived from Chang+Lee: Symbolic Logic etc. pp77-78
;;;-------------------------------------------------------------------------

FUNCTION Unify WITH PARAMETERS form1, form2, and assign RETURNS MGU, 
        where form1 and form2 are the forms that we want to unify, and assign
        is initially nil.

        1. Use the Find-Difference function described below to determine
           the first elements where form1 and form2 differ and one of 
           the elements is a variable. Call difference-set the value
           returned by Find-Difference. This value will be either the atom
           Fail, if the two forms cannot be unified; or null, if the two
           forms are identical; or a pair of the form (Variable Expression).

        2. If Find-Difference returned the atom Fail, Unify also returns Fail
           and we cannot unify the two forms.

        3. If Find-Difference returned nil, then Unify will return assign as MGU.

        4. Otherwise, we replace each occurrence of Variable by
           Expression in form1 and form2; we compose the given assignment assign
           with the assigment that maps Variable into Expression, and
           we repeat the process for the new form1, form2, and assign.


FUNCTION Find-Difference WITH PARAMETERS form1 and form2 RETURNS pair,
        where form1 and form2 are e-expressions.

        1. If form1 and form2 are the same variable, return nil.

        2. Otherwise, if either form1 or form2 is a variable, and it 
           does not appear anywhere in the other form, then return the 
           pair (Variable Other-Form), otherwise return Fail.

        3. Otherwise, if either form1 or form2 is an atom then
           if they are the same atom then return nil otherwise
           return Fail.

        4. Otherwise both form1 and form2 are lists.
           Apply the Find-Difference function to corresponding elements
           of the two lists until either a call returns a non-null value
           or the two lists are simultaneously exhausted, or some elements
           are left over in one list.
           In the first case, that non-null value is returned; in the second,
           nil is returned; in the third, Fail is returned.

;;;-------------------------------------------------------------------------