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.
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)