Die Unifikation ist ein Vorgang, bei dem das Zusammenpassen eines gewöhnlichen Atoms aus dem Ziel mit der Bedingung einer Hornklausel geprüft wird. Im Erfolgsfall werden dabei Variablen an Werte gebunden.

Der Trait unifiable markiert unifizierbare Terme oder Formeln.

(deftrait unifiable ())

Die Methode unify-copies erzeugt Kopien der übergebenen Argumente und unifiziert diese.

(defmethod unify-copies ((this unifiable) (that unifiable) context context-lock namespace-1 namespace-2)
  t
  (unify
    (copy this context context-lock namespace-1)
    (copy that context context-lock namespace-2)
    (list (new variable (quote *GUARD*) nil))))

Für unifizierbare Instanzen, für die es keine speziellere Methode gibt, schlägt die Unifikation fehl.

(defmethod unify ((this unifiable) (that unifiable) substitution) t
  (undo substitution))

(defproc undo (substitution)
  (dolist (value substitution nil)
    (unset-value value)))

Zwei Listen werden unifiziert, indem die einzelnen Elemente paarweise unifiziert werden.

(defproc unify-lists (elements-1 elements-2 substitution)
  (if
    elements-1
    (if
      elements-2
      (aand
        (unify (first elements-1) (first elements-2) substitution)
        (unify-lists (rest elements-1) (rest elements-2) it))
      (undo substitution))
    (if
      elements-2
      (undo substitution)
      substitution)))

Die folgenden Methoden spezifizieren die Unifikation für verschiedene Arten von Termen (siehe Term).

Termlisten werden unifiziert, indem deren Elemente unifiziert werden.

(defmethod unify ((this term-list) (that term-list) substitution)
  t
  (unify-lists
    (. this elements)
    (. that elements)
    substitution))

Strukturen werden unifiziert, indem deren Köpfe und deren Rümpfe unifiziert werden.

(defmethod unify ((this structure) (that structure) substitution)
  t
  (aand
    (unify (. this head) (. that head) substitution)
    (unify (. this tail) (. that tail) it)))

Zwei Konstanten sind unifizierbar, wenn sie den gleichen Wert haben.

(defmethod unify ((this constant) (that constant) substitution)
  t
  (if
    (= (. this value) (. that value))
    substitution
    (undo substitution)))

Eine Variable kann mit einem Term unifiziert werden, indem entweder der Wert der Variablen mit dem Term unifiziert wird (Variablen mit Wert) oder der Term zum Wert der Variablen wird (Variablen ohne Wert vor der Unifikation). Dabei darf der Term die Variable nicht enthalten.

(defmethod unify ((this term) (that variable) substitution) t
  (unify that this substitution))

(defmethod unify ((this variable) (that term) substitution) t
  (aif
    (get-value this)
    (unify it that substitution)
    (if
      (occurs? this that)
      (undo substitution)
      (progn
        (set-value this that)
        (cons this substitution)))))

(defmethod unify ((this term) (that variable) substitution)
  t
  (unify that this substitution))

(defmethod unify ((this variable) (that term) substitution)
  t
  (aif
    (get-value this)
    (unify it that substitution)
    (if
      (occurs? this that)
      (undo substitution)
      (progn
        (set-value this that)
        (cons this substitution)))))

(defmethod occurs? ((this variable) (that constant))
  t
  nil)

(defmethod occurs? ((this variable) (that variable))
  t
  (if
    (= this that)
    t
    (aand
      (get-value that)
      (occurs? this it))))
    
(defmethod occurs? ((this variable) (that structure))
  t
  (with-slots-read-only (head tail) that
    (or
      (occurs? this head)
      (occurs? this tail))))

(defmethod occurs? ((this variable) (that term-list))
  t
  (some?
    (lambda (term) (occurs? this term))
    (. that elements)))
    
(defmethod unify ((this variable) (that variable) substitution)
  t
  (if
    (and
      (= (. this name) (. that name))
      (= (. this namespace) (. that namespace)))
    substitution
    (aif
      (get-value this)
      (unify it that substitution)
      (progn
        (set-value this that)
        (cons this substitution)))))

Zwei Atome (siehe Formel) werden unifiziert, indem deren Strukturen unifiziert werden.

(defmethod unify ((this ordinary-atom) (that ordinary-atom) substitution)
  t
  (unify
    (. this structure)
    (. that structure)
    substitution))

Weil bei der Unifikation Variablen an Werte gebunden werden, geschieht die Unifikation nur auf Kopien der ursprünglichen Formeln. Die Kopien der Formeln enthalten für Variablen mit Wert den Wert und Kopien von Variablen ohne Wert.

(deftrait copyable ())

(defproc make-context ()
  (make-hash-table))

(defmethod copy ((this copyable) context context-lock default-namespace)
  t
  (let
    ((class (class-of this))
     (pairs (slot-values this)))
    (let
      ((that (allocate-instance class)))
      (progn
        (dolist (pair pairs)
          (assign
            that
            (first pair)
            (copy (second pair) context context-lock default-namespace)))
        (if
          (frozen? this)
          (freeze that)
          that)))))

(defmethod copy (this context context-lock default-namespace)
  (list? this)
  (map-with
    (lambda (element) (copy element context context-lock default-namespace))
    this))

(defmethod copy (this context context-lock default-namespace)
  (not (or (list? this) (is-a? this copyable)))
  this)

(defmethod copy ((this constant) context context-lock default-namespace)
  t
  this)

(defmethod copy ((this variable) context context-lock default-namespace)
  t
  (with-slots-read-only (name value) this
    (if
      value
      (copy value context context-lock default-namespace)
      (let
        ((namespace
          (or
            (. this namespace)
            default-namespace
            (throw (quote error) "no namespace"))))
        (let
          ((key (list name namespace)))
          (progn
            (acquire-lock context-lock)
            (aif
              (get-hash-table-value context key)
              (progn
                (release-lock context-lock)
                (if
                  (get-value it)
                  (copy (get-value it) context context-lock default-namespace)
                  it))
              (prog1
                (put-hash-table-value
                  context
                  key
                  (new variable name (or namespace default-namespace)))
                (release-lock context-lock)))))))))

(defmethod copy ((this negative-literal) context context-lock default-namespace)
  t
  (with-slots-read-only (atom program) this
    (let
      ((that (new negative-literal (copy atom context context-lock default-namespace))))
      (progn
        (.= that program program)
        (freeze that)))))

(defmethod copy ((this ordinary-atom) context context-lock default-namespace)
  t
  (with-slots-read-only (structure matching-clauses matching-clause-count) this
    (let
      ((that (new ordinary-atom (copy structure context context-lock default-namespace))))
      (progn
        (.= that matching-clauses matching-clauses)
        (.= that matching-clause-count matching-clause-count)
        (freeze that)))))

(defmethod copy ((this test-atom) context context-lock default-namespace)
  t
  (with-slots-read-only (variables function) this
    (new test-atom
      (copy variables context context-lock default-namespace)
      function)))

(defmethod copy ((this assignment-atom) context context-lock default-namespace)
  t
  (with-slots-read-only (left-hand-side variables function) this
    (new assignment-atom
      (copy left-hand-side context context-lock default-namespace)
      (copy variables context context-lock default-namespace)
      function)))