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 , und Variablen, und ein 2-stelliges Funktionssymbol. Die Variable und der Term sollen unifiziert werden. Aufgrund des Occurs checks schlägt die Unifizierung fehl, da in als Variable auftritt. Die Unifizierung von mit 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:
und mit occurs check bei:
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).