- 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.
Inhaltsverzeichnis
Beispiel
Im folgenden Beispiel seien x, y und z Variablen, und f ein 2-stelliges Funktionssymbol. Die Variable y und der Term t1 = f(x,y) sollen unifiziert werden. Aufgrund des Occurs checks schlägt die Unifizierung fehl, da y in t1 als Variable auftritt. Die Unifizierung von y mit t2 = 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
Literatur
- Franz Baader, Wayne Snyder: Ch.8 - Unification theory In: Handbook of Automated Reasoning, 2001, S. 441–524 (Unification theory; 660 KB).
Kategorie:- Programmiersprachelement
Wikimedia Foundation.
