Occurs Check

Occurs Check
†bersicht
Wiederholung: Wann sind zwei Terme unifizierbar?
Beispiel fŸr das Problem
Lšsung des Problems: Occurs Check
Verhalten von Prolog
Ziel
Verstehen, worin das Problem liegt
Occurs Check Ð 1
Wann sind zwei Terme unifizierbar?
Zwei Terme S und T sind unifizierbar, genau dann wenn:
S und T sind dasselbe Atom,
oder einer von ihnen ist eine freie Variable
(in diesem Fall wird die Variable gebunden),
oder S und T sind komplexe Terme, wobei
S und T haben denselben Funktor,
und S und T haben dieselbe Stelligkeit,
und die einzelnen Argumente sind jeweils paarweise unifizierbar.
Occurs Check Ð 2
A Problem Occurs É
Das Problem zeigt sich bei folgender Frage:
Sind die Terme X und f(X) miteinander unifizierbar?
Wenn ja, was ist das Ergebnis?
X
f(X)
Occurs Check Ð 3
A Problem Occurs É
X
f( X )
Occurs Check Ð 4
A Problem Occurs É
X
f( X )
X
f( X )
f(f( X ))
Occurs Check Ð 5
/f( X )
A Problem Occurs É
X
f( X )
X
/f( X )
X
/f( X )
f( X )
f(f( X ))
f(f( X ))
f(f(f( X )))
Occurs Check Ð 6
A Problem Occurs É
X
f( X )
X
/f( X )
X
/f( X )
X
/f( X )
X
/f( X )
f( X )
f(f( X ))
f(f( X ))
f(f(f( X )))
f(f(f( X )))
f(f(f(f( X ))))
Occurs Check Ð 7
Vermeiden des Problems
Eine Variable darf nicht an einen Term gebunden werden,
der dieselbe Variable enthŠlt.
Dieser Sicherheitstest heisst Occurs Check (ÈAuftauchtestÇ).
GemŠss mathematisch korrekter Definition der Unifikation wŠren
X und f(X) nicht miteinander unifizierbar.
f( X )
X
Occurs Check Ð 8
Was macht Prolog?
Wir kšnnen diese Anfrage natŸrlich an Prolog stellen.
Was ist das Ergebnis?
?- X = f(X).
X = f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
Occurs Check Ð 9
Was macht Prolog?
Prolog fŸhrt den Occurs Check offensichtlich nicht durch.
Der Test ist relativ aufwendig durchzufŸhren
Die meisten Prolog-Interpreter lassen ihn daher einfach weg
É denn in der Praxis kommt das Problem eher selten vor
Allerdings bieten viele Prolog-Implementationen ein besonderes
PrŠdikat fŸr die Unifikation mit Occurs Check an
Es wŠre auch mšglich, zyklische Strukturen zuzulassen.
andere Defintion der Unifikation
von einigen Prolog-Versionen unterstŸtzt
Occurs Check Ð 10

Download Report