Occurs check

Der Occurs check bezeichnet in der Informatik einen Teil des Unifikationsalgorithmus. Er verhindert, dass eine Variable durch einen Term ersetzt wird, der diese Variable enthält. Anwendung findet er bspw. bei der Typprüfung in funktionalen Programmiersprachen, um die Konstruktion unendlicher Datentypen zu verhindern, sowie in logischen Programmiersprachen.

Beispiel

Im folgenden Beispiel seien $x$, $y$ und $z$ Variablen, und $f$ ein 2-stelliges Funktionssymbol. Die Variable $y$ und der Term $t_{1}=f(x,y)$ sollen unifiziert werden. Aufgrund des Occurs checks schlägt die Unifizierung fehl, da $y$ in $t_{1}$ als Variable auftritt. Die Unifizierung von $y$ mit $t_{2}=f(x,z)$ wäre hingegen erfolgreich.

Prolog

In der Sprache Prolog ist der Occur check bei der Überprüfung von Regel-Definitionen aus Performanzgründen normalerweise abgeschaltet, was die Gefahr einer Endlosschleife bei der Auswertung in sich birgt. In einigen Implementierungen von Prolog kann sie aber bei Bedarf aktiviert werden.

Die Komplexität einer Unifikation liegt ohne occurs check bei:

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

und mit occurs check bei:

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

Siehe auch

• Unifikation (Logik)
• Prädikatenlogik
• Maschinengestütztes Beweisen

Literatur

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