;;;
;;; Solution for A3 question #2
;;;
;;; By Philip W. L. Fong
;;;
;;
;; Composition of substitutions
;;
(defun substitution-bound-p (sub sym)
"Check if symbol SYM is bound in substitution SUB."
(not (eq sym (substitution-look-up sub sym))))
(defun compose-substitutions (s1 s2)
"Compose substitution s1 with s2."
(let ((s3 (mapcar #'(lambda (B)
(make-binding (binding-sym B)
(apply-substitution s2 (binding-exp B))))
s1))
(s4 (remove-if #'(lambda (B)
(substitution-bound-p s1 (binding-sym B)))
s2)))
(append s3 s4)))
;;
;; Unification
;;
(defun occurs-check-p (var exp)
"Return non-NIL if variable VAR occurs in expression EXP."
(cond
((null exp)
nil)
((consp exp)
(or (occurs-check-p var (first exp))
(occurs-check-p var (rest exp))))
(t
(eq var exp))))
(defun unify (equation-list)
"Return the substitution that solves the unification equations in the list
EQUATION-LIST, or return 'failure if the list of equations is not solvable."
(unify-aux nil equation-list))
(defun unify-aux (sub equation-list)
"Implementation of the Robinson's unification algorithm."
(if (null equation-list)
sub
(let ((t1 (equation-lhs (first equation-list)))
(t2 (equation-rhs (first equation-list)))
(rest-eqns (rest equation-list)))
(cond
;; Deletion
((eq t1 t2)
(unify-aux sub rest-eqns))
;; Binding + Occur-Check
((variable-p t1)
(if (occurs-check-p t1 t2)
'failure
(unify-aux
(compose-substitutions sub (make-unit-substitution t1 t2))
(apply-substitution (make-unit-substitution t1 t2)
rest-eqns))))
;; Orientation
((variable-p t2)
(unify-aux sub (cons (list t2 t1) rest-eqns)))
;; Decomposition + Disagreement
(t
(if (or (not (listp t1))
(not (listp t2))
(not (= (list-length t1) (list-length t2))))
'failure
(unify-aux sub (append (mapcar #'list t1 t2) rest-eqns))))))))