5  Unification

When we say that a goal matches with a clause-head, we mean that the predicate and argument positions line up. Before making this comparison, Schelog dereferences all already bound logic variables. The resulting structures are then compared to see if they are recursively identical. Thus, 1 unifies with 1, and (list 1 2) with '(1 2); but 1 and 2 do not unify, and neither do '(1 2) and '(1 3).

In general, there could be quite a few uninstantiated logic variables in the compared objects. Unification will then endeavor to find the most natural way of binding these variables so that we arrive at structurally identical objects. Thus, (list x 1), where x is an unbound logic variable, unifies with '(0 1), producing the binding [x 0].

Unification is thus a goal, and Schelog makes the unification predicate available to the user as %=. Eg,

(%which (x)
  (%= (list x 1) '(0 1))
=>([x 0])

Schelog also provides the predicate %/=, the negation of %=. (%/= X Y) succeeds if and only if X does not unify with Y.

Unification goals constitute the basic subgoals that all Schelog goals devolve to. A goal succeeds because all the eventual unification subgoals that it decomposes to in at least one of its subgoal-branching succeeded. It fails because every possible subgoal-branching was thwarted by the failure of a crucial unification subgoal.

Going back to the example in sec 4, the goal (%computer‑literate 'Penelope) succeeds because (a) it unified with (%computer‑literate person); and then (b) with the binding [person Penelope] in place, (%knows person 'TeX) unified with (%knows 'Penelope 'TeX) and (%knows person 'Prolog) unified with (%knows 'Penelope 'Prolog).

In contrast, the goal (%computer‑literate 'Telemachus) fails because, with [person Telemachus], the subgoals (%knows person 'Scheme) and (%knows person 'Prolog) have no facts they can unify with.

5.1  The Occurs Check

A robust unification algorithm uses the occurs check, which ensures that a logic variable isn’t bound to a structure that contains itself. Not performing the check can cause the unification to go into an infinite loop in some cases. On the other hand, performing the occurs check greatly increases the time taken by unification, even in cases that wouldn’t require the check.

Schelog uses the global variable *schelog‑use‑occurs‑check?* to decide whether to use the occurs check. By default, this variable is #f, ie, Schelog disables the occurs check. To enable the check,

(set! *schelog-use-occurs-check?* #t)