Occurs check

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).

Wikimedia Foundation.

Игры ⚽ Нужно сделать НИР?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Occurs check — In computer science, the occurs check is a part of algorithms for syntactic unification. It causes unification of a logic variable V and a structure S to fail if S contains V. In theorem proving, unification without the occurs check can lead to… …   Wikipedia

  • Check It Out! with Dr. Steve Brule — Title screen Genre Comedy Created by John C. Reil …   Wikipedia

  • Check valve — Tilting disc inconel check valve …   Wikipedia

  • Check weigher — Example checkweigher. Product passes on the conveyor belt where it is weighed A checkweigher is an automatic machine for checking the weight of packaged commodities. It is normally found at the offgoing end of a production process and is used to… …   Wikipedia

  • Machine Check Exception — A Machine Check Exception (MCE) is a type of computer hardware error that occurs when a computer s central processing unit detects a hardware problem. Microsoft Windows displays the error using the blue screen of death containing the error… …   Wikipedia

  • Cyclic redundancy check — A cyclic redundancy check (CRC) is an error detecting code designed to detect accidental changes to raw computer data, and is commonly used in digital networks and storage devices such as hard disk drives. Blocks of data entering these systems… …   Wikipedia

  • Cross-check — This article is about a type of move in chess. Cross checking is also a penalty in ice hockey. In chess, a cross check is a tactic in which a check played in response to a check, especially when the original check is blocked by a piece that… …   Wikipedia

  • Bug check — A bug check (also known as a system crash, stop error, or kernel error) is when the Windows operating system halts the moment it reaches a condition where it cannot operate safely. A bug check can be deliberately caused from a kernel mode driver… …   Wikipedia

  • SCSI check condition — In computer terminology, a Check Condition occurs when a SCSI device needs to report an error. SCSI communication takes place between an initiator and a target. The initiator sends a command to the target which then responds. SCSI commands are… …   Wikipedia

  • Multidimensional parity-check code — A multidimensional parity check code (MDPC) is a simple type of error correcting code that operates by arranging the message into a multidimensional grid, and calculating a parity digit for each row and column. In general, an n dimensional parity …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”