Unification algorithm in Racket

unification.rkt

#lang racket
;;;; Unification algorithm.
;;;; Racket implementation based on Chapter 11 of "Paradigms of Artificial
;;;; Intelligence Programming" by Peter Norvig.
;;;;
;;;; Example usage:
;;;;
;;;;  (unify '(1 ?x ?y)
;;;;         '(?y 2 ?y))
;;;;  ;; Returns: '((?x . 2) (?y . 1))
;;;;
;;;;  (unifier '(1 ?x ?y)
;;;;           '(?y 2 ?y))
;;;;  ;; Returns: '(1 2 1)
;;;;
;;;;  (parameterize ((*occurs-check* #t))
;;;;    (unifier '?x '(?x)))
;;;;  ;; Returns: '()
;;;;  ;; (i.e. FAIL)

(provide FAIL
         NO-BINDINGS
         *occurs-check*
         subst-bindings
         unify
         variable?)

;; Indicates unification failure.
(define FAIL '())
;; Indicates unification success with no variables.
(define NO-BINDINGS '((#t . #t)))
;; Whether or not to do the occurs check.
(define *occurs-check* (make-parameter #f))

;; Is x a variable? (Is x a symbol beginning with a question mark character?)
(define (variable? x)
  (and (symbol? x)
       (eq? (first (string->list (symbol->string x)))
            #\?)))

;; Returns a '(var . val) pair in the bindings list.
;; Returns #f if var is not in the bindings list.
(define (get-binding var bindings)
  (assoc var bindings))

;; Whether or not var exists in the bindings list.
(define (has-binding? var bindings)
  (if (get-binding var bindings)
      #t
      #f))

;; Get the value part of a single binding.
(define (binding-val binding)
  (cdr binding))

;; Get the value for a var from the bindings list.
(define (lookup var bindings)
  (binding-val (get-binding var bindings)))

;; Add a '(var . val) pair to the bindings list.
(define (extend-bindings var val bindings)
  (cons (cons var val)
        (if (equal? bindings NO-BINDINGS)
            '()
            bindings)))

;; See if x and y match with the given bindings.
;; Returns either an alist of bindings or FAIL.
(define (unify x y [bindings NO-BINDINGS])
  (cond [(eq? bindings FAIL) FAIL]
        [(equal? x y) bindings]
        [(variable? x)
         (unify-variable x y bindings)]
        [(variable? y)
         (unify-variable y x bindings)]
        [(and (pair? x) (pair? y))
         (unify (cdr x)
                (cdr y)
                (unify (car x) (car y) bindings))]
        [else FAIL]))

;; Unify var with x, using and possibly extending the given bindings.
(define (unify-variable var x bindings)
  (cond [(has-binding? var bindings)
         (unify x
                (lookup var bindings)
                bindings)]
        [(and (variable? x) (has-binding? x bindings))
         (unify var
                (lookup x bindings)
                bindings)]
        [(and (*occurs-check*) (occurs-check var x bindings))
         FAIL]
        [else (extend-bindings var x bindings)]))

;; Does var occur anywhere inside x?
(define (occurs-check var x bindings)
  (cond [(eq? var x) #t]
        [(and (variable? x) (has-binding? x bindings))
         (occurs-check var (lookup x bindings) bindings)]
        [(pair? x)
         (or (occurs-check var (car x) bindings)
             (occurs-check var (cdr x) bindings))]
        [else #f]))

;; Substitute the value of variables in bindings into x.
(define (subst-bindings bindings x)
  (cond [(eq? bindings FAIL) FAIL]
        [(equal? bindings NO-BINDINGS) x]
        [(and (variable? x) (has-binding? x bindings))
         (subst-bindings bindings
                         (lookup x bindings))]
        [(pair? x)
         (cons (subst-bindings bindings (car x))
               (subst-bindings bindings (cdr x)))]
        [else x]))

;; Return a value that unifies with both x and y (or fails).
(define (unifier x y)
  (subst-bindings (unify x y) x))