Occurs check

In computer science, the occurrence check describes part of the unification algorithm . It prevents a variable from being replaced by a term that contains that variable. It is used, for example, in type testing in functional programming languages to prevent the construction of infinite data types, as well as in logical programming languages .

example

In the following example , and are variables, and are a 2-digit function symbol. The variable and the term should be unified. Due to the occurrence check, the unification fails because in appears as a variable. The unification of with , however, would be successful. ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$ ${\displaystyle f}$ ${\displaystyle y}$ ${\displaystyle t_{1}=f(x,y)}$ ${\displaystyle y}$ ${\displaystyle t_{1}}$ ${\displaystyle y}$ ${\displaystyle t_{2}=f(x,z)}$

prolog

In the Prolog language , the occurrence check is normally switched off when checking rule definitions for reasons of performance , which harbors the risk of an endless loop in the evaluation. However, in some implementations of Prolog it can be activated if necessary.

The complexity of a unification is without occurs check :

O(min(Größe(Term1), Größe(Term2)))

and with occurs check at:

O(max(Größe(Term1), Größe(Term2)))

See also

• Unification (logic)
• Predicate logic
• Machine-Aided Proof

literature

• Franz Baader, Wayne Snyder: Ch.8 - Unification theory In: Handbook of Automated Reasoning , 2001, pp. 441-524 ( Unification theory ; 660 kB).