Förekommer kontroll

Inom datavetenskap är kontrollen av inträffar en del av algoritmer för syntaktisk enande . Det gör att föreningen av en variabel V och en struktur S misslyckas om S innehåller V .

Tillämpning i satsbevisande

I satsbevisande kan förening utan att inträffar-kontrollen leda till osunda slutsatser . Till exempel Prolog- målet $X=f(X)$ att lyckas, binda X till en cyklisk struktur som inte har någon motsvarighet i Herbrands universum . Som ett annat exempel, utan inträffar-kontroll, kan ett upplösningsbevis hittas för icke-satsen ${\displaystyle (\forall x\exists yp(x,y))\rightarrow (\exists y\forall xp(x,y))} : negationen$ av den formeln har den konjunktiva normalformen ${\displaystyle p(X,f(X))\land \lnot p(g(Y),Y)} ,$ med $f$ och $g$ betecknar Skolem-funktionen för den första respektive andra existentiella kvantifieraren; bokstaverna $p(X,f(X))$$p(g(Y),Y)$ p är unifierbara utan inträffar kontroll, producerar den motbevisande tomma klausulen.

Cykel genom utelämnad sker kontroll

Rationell trädförening

Prolog-implementationer utelämnar vanligtvis kontrollen av inträffar av effektivitetsskäl, vilket kan leda till cirkulära datastrukturer och looping. Genom att inte utföra kontrollen inträffar, reduceras i många fall den värsta komplexiteten av att förena en term $t_{1}$ med term ${\displaystyle t_{2}} från$$O({\text{size}}(t_{1})+{\text{size}}(t_{2}))$ till $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})) )$ ; i det speciella, frekventa fallet med variabla termer, krymper körtiden till $O(1)$ .

Moderna implementeringar, baserade på Colmerauers Prolog II, använder rationell trädförening för att undvika looping. Det är dock svårt att hålla komplexitetens tid linjär i närvaro av cykliska termer. Exempel där Colmerauers algoritm blir kvadratisk kan lätt konstrueras, men förfiningsförslag finns.

$cons(x,y){\stackrel {?}{=}}cons(1,cons( x,cons(2,y)))$ ett exempel på en enhetsalgoritm som ges i Unification (datavetenskap)#A unification algorithm , trying to solve the goal , dock utan regeln "checks" (som heter "check" där); att tillämpa regeln "eliminera" leder istället till en cyklisk graf (dvs en oändlig term) i det sista steget.

Ljudförening

ISO Prolog-implementeringar har det inbyggda predikatet unify_with_occurs_check/2 för ljudsammanslutning, men är fria att använda osunda eller till och med loopingalgoritmer när sammanslagningen åberopas på annat sätt, förutsatt att algoritmen fungerar korrekt för alla fall som "inte är föremål för förekomstkontroll" ( NSTO). Den inbyggda acykliska_term/1 tjänar till att kontrollera termernas ändlighet.

Implementationer som erbjuder ljudsammanslutning för alla sammanslagningar är Qu-Prolog och Strawberry Prolog och (valfritt, via en runtime-flagga): XSB , SWI-Prolog , Tau Prolog och Scryer Prolog . En mängd olika optimeringar kan göra ljudsammanslutning möjlig för vanliga fall.

Se även

WP Weijland (1990). "Semantik för logikprogram utan förekomstkontroll" . Teoretisk datavetenskap . 71 : 155–174. doi : 10.1016/0304-3975(90)90194-m .