Występuje sprawdź

W informatyce kontrola występowania jest częścią algorytmów unifikacji składni . Powoduje niepowodzenie unifikacji zmiennej V i struktury S , jeśli S zawiera V .

Zastosowanie w dowodzeniu twierdzeń

W dowodzeniu twierdzeń unifikacja bez sprawdzenia występowania może prowadzić do błędnego wnioskowania . Na przykład cel Prologu odniesie sukces, wiążąc X z $cykliczną$ odpowiednika we wszechświecie Jako inny przykład, bez sprawdzania występowania, można znaleźć dowód rozwiązania dla nie-twierdzenia ${\ Displaystyle (\ forall x \ istnieje yp (x, y)) \ rightarrow (\ istnieje y \ forall xp (x, y) )}$ : zaprzeczenie tego wzoru ma koniunkcyjną postać normalną ${\ Displaystyle p (X, f (X)} \ land \ lnot p (g (Y), Y)}$ , przy czym ${\ Displaystyle f}$ i ${\ Displaystyle g}$ oznaczają funkcję Skolema dla pierwszego i drugiego odpowiednio kwantyfikator egzystencjalny; ${\ Displaystyle p (X, f (X))}$ i $g (Y), Y)}$ ( są unifikowalne bez sprawdzania, co daje odrzucającą pustą klauzulę.

Cykl po pominięciu występuje sprawdzanie

Racjonalne Ujednolicenie Drzewa

Implementacje Prologu zwykle pomijają sprawdzanie występowania ze względu na wydajność, co może prowadzić do kołowych struktur danych i pętli. $rozmiar$${\ Displaystyle O ({\ tekst {rozmiar}} (t_ {1}) + {\ tekst {rozmiar}} (t_ {2})}}$ występowania, złożoność najgorszego przypadku ujednolicenia terminu terminem $przypadkach$ zmniejszana z do ${\ Displaystyle O ({\ tekst {min}} ({\ tekst {rozmiar}} (t_ {1}), {\ tekst {rozmiar} }(t_{2})))}$ ; w szczególnym, częstym przypadku unifikacji zmiennych terminów, czas wykonania kurczy się do ${\ Displaystyle O (1)}$ .

Nowoczesne implementacje, oparte na Prologu II Colmerauera, wykorzystują racjonalne ujednolicenie drzewa, aby uniknąć pętli. Jednak trudno jest utrzymać liniowość czasu złożoności w obecności terminów cyklicznych. Przykłady, w których algorytm Colmerauersa staje się kwadratowy, można łatwo skonstruować, ale istnieją propozycje udoskonalenia.

Zobacz obraz przykładowego przebiegu algorytmu unifikacji podanego w Unification (informatyka)#A algorytm unifikacji , próbujący rozwiązać cel ${\ displaystyle cons (x, y) {\ stackrel {?} {=}} cons (1, cons (x, cons (2, y)))} , jednak bez reguły sprawdzania występowania (nazwanej tam „$ check ” ) ; zamiast tego zastosowanie reguły „wyeliminuj” prowadzi do wykresu cyklicznego (tj. składnika nieskończonego) w ostatnim kroku.

Ujednolicenie dźwięku

Implementacje ISO Prolog mają wbudowany predykat unify_with_occurs_check/2 dla ujednolicenia dźwięku, ale mogą swobodnie używać wadliwych lub nawet zapętlonych algorytmów, gdy ujednolicenie jest wywoływane w inny sposób, pod warunkiem, że algorytm działa poprawnie we wszystkich przypadkach, które „nie podlegają kontroli występowania” ( NSTO). Wbudowany acycle_term/1 służy do sprawdzania skończoności terminów.

Implementacje oferujące ujednolicenie dźwięku dla wszystkich unifikacji to Qu-Prolog i Strawberry Prolog oraz (opcjonalnie za pomocą flagi wykonawczej): XSB , SWI-Prolog , Tau Prolog i Scryer Prolog . Różnorodne optymalizacje mogą sprawić, że ujednolicenie dźwięku będzie wykonalne w typowych przypadkach.

Zobacz też

WP Weijland (1990). „Semantyka programów logicznych bez sprawdzania występowania” . Informatyka teoretyczna . 71 : 155–174. doi : 10.1016/0304-3975(90)90194-m .