imported>Matthäus Wander: link

2023-08-19T14:40:38Z

link

Neue Seite

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

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

== Prolog ==
In der Sprache [[Prolog (Programmiersprache)|Prolog]] ist der Occur check bei der Überprüfung von Regel-Definitionen aus [[Performance (Informatik)|Performanzgründen]] normalerweise abgeschaltet, was die Gefahr einer [[Endlosschleife (Programmierung)|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:
: <code>O(min(Größe(Term1), Größe(Term2)))</code>
und mit ''occurs check'' bei:
: <code>O(max(Größe(Term1), Größe(Term2)))</code>

== 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 ([http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf Unification theory]; 660 kB).

[[Kategorie:Programmiersprachelement]]

Occurs check - Versionsgeschichte

imported>Matthäus Wander: link