Occurs check: Difference between revisions

Content deleted Content added

Inline

Revision as of 11:15, 17 June 2020

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 $X=f(X)$ will succeed, binding X to a cyclic structure which has no counterpart in the Herbrand universe. As another example, ^[1] without occurs-check, a resolution proof can be found for the non-theorem ^[2] $(\forall x\exists y.p(x,y))\rightarrow (\exists y\forall x.p(x,y))$ : the negation of that formula has the conjunctive normal form $p(X,f(X))\land \lnot p(g(Y),Y)$ , with $f$ and $g$ denoting the Skolem function for the first and second existential quantifier, respectively; the literals $p(X,f(X))$ and $p(g(Y),Y)$ are unifiable without occurs check, producing the refuting empty clause.

Prolog implementation

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 $t_{1}$ with term $t_{2}$ is reduced in many cases from $O({\text{size}}(t_{1})+{\text{size}}(t_{2}))$ to $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$ ; in the particular, frequent case of variable-term unifications, runtime shrinks to $O(1)$ . ^{[nb 1]}

A naive omission of the occurs check leads to the creation of cyclic structures and may cause unification to loop forever. Modern implementations, based on Colmerauer's Prolog II, ^[4] ^[5] ^[6] ^[7] use rational tree unification to avoid looping. See image for an example run of the unification algorithm given in Unification (computer science)#A unification algorithm, trying to solve the goal $cons(x,y){\stackrel {?}{=}}cons(1,cons(x,cons(2,y)))$ , 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.

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).^[8]

Implementations offering sound unification for all unifications are Qu-Prolog and Strawberry Prolog and (optionally, via a runtime flag): XSB, SWI-Prolog and Tau Prolog.

Notes

^ Some Prolog manuals state that the complexity of unification without occurs check is $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$ (in all cases).^[3] This is incorrect, as it would imply comparing arbitrary ground terms in constant time (by unifying $eq(t_{1},t_{2})$ with $eq(X,X)$ ).

References

^ David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley.; here: p.143
^ Informally, and taking $p(x,y)$ 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."
^ F. Pereira; D. Warren; D. Bowen; L. Byrd; L. Pereira (1983). C-Prolog's User's Manual Version 1.2 (Technical report). SRI International. Retrieved 21 June 2013.
^ A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (eds.). Prolog and Infinite Trees. Academic Press.
^ M.H. van Emden; J.W. Lloyd (1984). "A Logical Reconstruction of Prolog II". J. Logic Programming. 2: 143–149.
^ Joxan Jaffar; Peter J. Stuckey (1986). "Semantics of Infinite Tree Logic Programming". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.
^ B. Courcelle (1983). "Fundamental Properties of Infinite Trees" (PDF). Theoretical Computer Science. 25: 95–169. doi:10.1016/0304-3975(83)90059-2. Archived from the original (PDF) on 2014-04-21. Retrieved 2013-06-21. {{cite journal}}: Cite has empty unknown parameter: |month= (help)
^ 7.3.4 Normal unification in Prolog of ISO/IEC 13211-1:1995.

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.

[4] Some Prolog manuals state that the complexity of unification without occurs check is $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$ (in all cases).^[3] This is incorrect, as it would imply comparing arbitrary ground terms in constant time (by unifying $eq(t_{1},t_{2})$ with $eq(X,X)$ ).

[1] David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley.; here: p.143

[2] Informally, and taking $p(x,y)$ 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."

[3] F. Pereira; D. Warren; D. Bowen; L. Byrd; L. Pereira (1983). C-Prolog's User's Manual Version 1.2 (Technical report). SRI International. Retrieved 21 June 2013.

[5] A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (eds.). Prolog and Infinite Trees. Academic Press.

[6] M.H. van Emden; J.W. Lloyd (1984). "A Logical Reconstruction of Prolog II". J. Logic Programming. 2: 143–149.

[7] Joxan Jaffar; Peter J. Stuckey (1986). "Semantics of Infinite Tree Logic Programming". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.

[8] B. Courcelle (1983). "Fundamental Properties of Infinite Trees" (PDF). Theoretical Computer Science. 25: 95–169. doi:10.1016/0304-3975(83)90059-2. Archived from the original (PDF) on 2014-04-21. Retrieved 2013-06-21. {{cite journal}}: Cite has empty unknown parameter: |month= (help)

[9] 7.3.4 Normal unification in Prolog of ISO/IEC 13211-1:1995.

[1]

[2]

[nb 1]

[4]

[5]

[6]

[7]

[8]

[3]

@@ Line 16: / Line 16: @@
 ==Prolog implementation==
-By default, Prolog implementations usually omit the occurs check for reasons of efficiency, which can lead to circular data structures and looping.
+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
+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 particular, frequent case of variable-term unifications, runtime shrinks to <math>O(1)</math>.{{refn|group=nb|Some Prolog
+in the particular, frequent case of variable-term unifications, runtime shrinks to
+<math>O(1)</math>.
-manuals state that the complexity of unification without occurs check is
+{{refn|group=nb|Some Prolog manuals state that the complexity of unification without occurs check is
 <math>O(\text{min}(\text{size}(t_1),\text{size}(t_2)))</math> (in all cases).<ref>{{cite techreport|author1=F. Pereira |author2=D. Warren |author3=D. Bowen |author4=L. Byrd |author5=L. Pereira | title=C-Prolog's User's Manual Version 1.2| year=1983| institution=SRI International|URL=http://www.cs.duke.edu/csl/docs/cprolog.html| accessdate=21 June 2013}}</ref>
 This is incorrect, as it would imply comparing arbitrary ground terms in constant time (by unifying <math>eq(t_1,t_2)</math> with <math>eq(X,X)</math>).}}
@@ Line 36: / Line 39: @@
 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.
-ISO Prolog implementations have the built-in predicate unify_with_occurs_check/2
+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>
-for sound unification but are free to use unsound or even looping algorithms
+Implementations offering sound unification for all unifications are Qu-Prolog and [[Strawberry Prolog]] and (optionally, via a runtime flag): [[XSB]], [[SWI-Prolog]] and [http://tau-prolog.org/ Tau Prolog].
-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>
-Implementations offering sound unification
+==See also==
-for all unifications are
+{{cite journal| author=W.P. Weijland| title=Semantics for Logic Programs without Occur Check| journal=Theoretical Computer Science| year=1990| month=| volume=71| number=| pages=155–174| url=https://www.sciencedirect.com/science/article/pii/030439759090194M| doi=10.1016/0304-3975(90)90194-m}}
-Qu-Prolog and [[Strawberry Prolog]] and (optionally, via a runtime flag): [[XSB]], [[SWI-Prolog]] and [http://tau-prolog.org/ Tau Prolog].
 ==Notes==
@@ Line 47: / Line 50: @@
 ==References==
-* {{cite journal| author=W.P. Weijland| title=Semantics for Logic Programs without Occur Check| journal=Theoretical Computer Science| year=1990| month=| volume=71| number=| pages=155–174| url=http://oai.cwi.nl/oai/asset/2366/2366A.pdf| doi=10.1016/0304-3975(90)90194-m}}
 {{reflist}}
 {{FOLDOC}}