Occurs check
Template:Short description In computer science, the occurs check is a part of algorithms for syntactic unification. It causes unification of a variable V and a structure S to fail if S contains V.
Application in theorem proving
In theorem proving, unification without the occurs check can lead to unsound inference. For example, the Prolog goal <math>X = f(X)</math> will succeed, binding X to a cyclic structure which has no counterpart in the Herbrand universe. As another example,<ref>Template:Cite book; here: p.143</ref> without occurs-check, a resolution proof can be found for the non-theorem<ref>Informally, and taking <math>p(x,y)</math> to mean e.g. "x loves y", the formula reads "If everybody loves somebody, then a single person must exist that is loved by everyone."</ref> <math>(\forall x \exists y. p(x,y)) \rightarrow (\exists y \forall x. p(x,y))</math>: the negation of that formula has the conjunctive normal form <math>p(X,f(X)) \land \lnot p(g(Y),Y)</math>, with <math>f</math> and <math>g</math> denoting the Skolem function for the first and second existential quantifier, respectively. Without occurs check, the literals <math>p(X,f(X))</math> and <math>p(g(Y),Y)</math> are unifiable, producing the refuting empty clause.
Rational tree unification
Prolog implementations usually omit the occurs check for reasons of efficiency, which can lead to circular data structures and looping. By not performing the occurs check, the worst case complexity of unifying a term <math>t_1</math> with term <math>t_2</math> is reduced in many cases from <math>O(\text{size}(t_1)+\text{size}(t_2))</math> to <math>O(\text{min}(\text{size}(t_1),\text{size}(t_2)))</math>; in the frequent case of variable-term unification, runtime shrinks to <math>O(1)</math>. Template:Refn
Implementations, based on Colmerauer's Prolog II, <ref>Template:Cite book</ref> <ref>Template:Cite journal</ref> <ref>Template:Cite journal</ref> <ref>Template:Cite journal</ref> use rational tree unification to avoid looping. However it is difficult to keep the complexity time linear in the presence of cyclic terms. Examples where Colmerauers algorithm becomes quadratic <ref>Template:Cite conference</ref> can be readily constructed.
Jaffar’s 1984 work proposed a refinement based on union–find techniques,<ref>Template:Citation</ref> effectively reducing the worst-case complexity to near-linear time. Modern systems — including SWI-Prolog, SICStus Prolog, Scryer Prolog, and Ciao Prolog — appear to implement variants of this approach.
See image for an example run of the unification algorithm given in Unification (computer science)#A unification algorithm, trying to solve the goal <math>cons(x,y) \stackrel{?}{=} cons(1,cons(x,cons(2,y)))</math>, however without the occurs check rule (named "check" there); applying rule "eliminate" instead leads to a cyclic graph (i.e. an infinite term) in the last step.
Sound unification
ISO Prolog implementations have the built-in predicate unify_with_occurs_check/2 for sound unification but are free to use unsound or even looping algorithms when unification is invoked otherwise, provided the algorithm works correctly for all cases that are "not subject to occurs-check" (NSTO).<ref>7.3.4 Normal unification in Prolog of ISO/IEC 13211-1:1995.</ref> The built-in acyclic_term/1 serves to check the finiteness of terms.
Implementations offering sound unification for all unifications are Qu-Prolog and Strawberry Prolog and (optionally, via a runtime flag): XSB, SWI-Prolog, CxProlog, Tau Prolog, Trealla Prolog and Scryer Prolog. A variety <ref>Template:Cite journal</ref><ref>Template:Cite conference</ref> of optimizations can render sound unification feasible for common cases.