Occurs check

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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[Bearbeiten]

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[Bearbeiten]

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[Bearbeiten]

Literatur[Bearbeiten]

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