Prolog Language
monotoni~~POS=TRUNC

Resonemang om monotoniska predikat

Monotoniska predikat kan felsöks genom att tillämpa deklarativt resonemang.

I ren Prolog kan ett programmeringsfel leda till ett eller alla av följande fenomen:

1. predikatet lyckas felaktigt i ett fall där det skulle misslyckas
2. predikatet misslyckas felaktigt i ett fall där det borde lyckas
3. predikatet slingrar oväntat där det bara borde ge en begränsad uppsättning svar.

Tänk som exempel på hur vi kan felsöka ärende (2) genom deklarativt resonemang: Vi kan systematiskt ta bort mål för predikatets klausuler och se om frågan fortfarande misslyckas. I monotonisk kod kan borttagande av mål högst göra det resulterande programmet mer generellt . Därför kan vi fastställa fel genom att se vilka av målen som leder till det oväntade misslyckandet.

Exempel på monotoniska predikat

Exempel på monotoniska predikat är:

• enhet med (=)/2 eller unify_with_occurs_check/2
• dif/2 , uttrycker ojämlikhet mellan villkor
• CLP (FD) begränsningar som (#=)/2 och (#>)/2 med ett monotoniskt exekveringsläge.

Prolog förutsäger att endast monotoniska mål är själva monotoniska.

Monotoniska predikat möjliggör förklarande resonemang:

1. Att lägga till en begränsning (dvs. ett mål) till en fråga kan i högsta grad minska , aldrig utöka, uppsättningen lösningar.
2. Att ta bort ett mål med sådana predikat kan på det mesta förlänga , aldrig minska, uppsättningen lösningar.

Icke-monotoniska predikat

Här är exempel på predikat som inte är monotoniska:

• metallogiska predikat som var/1 , integer/1 etc.
• term jämförelse predicates som (@<)/2 och (@>=)/2
• predikater som använder !/0 , (\+)/1 och andra konstruktioner som bryter monotoniciteten
• all-lösningar findall/3 som findall/3 och setof/3 .

Om dessa predikat används kan tillägg av mål leda till fler lösningar, vilket strider mot den viktiga deklarativa egenskapen känd från logiken att att lägga till begränsningar kan som mest reducera , aldrig utvidga, lösningen.

Som en konsekvens bryts också andra egenskaper som vi förlitar oss för deklarativ felsökning och andra resonemang. Till exempel bryter icke-monotoniska predikater det grundläggande begreppet kommutativitet för konjunktion som är känd från första ordningens logik. Följande exempel illustrerar detta:

?- var(X), X = a.
X = a.

?- X = a, var(X).
false.

All-lösningar predikat som findall/3 bryter också monotonicity: Att lägga till klausuler kan leda till misslyckanden i mål som tidigare hade hållits . Detta strider också mot montonicity som är känt från första ordningens logik, där tillägg av fakta som högst kan öka , aldrig minskar uppsättningen konsekvenser.

Monotoniska alternativ för icke-monotoniska konstruktioner

Här är exempel på hur du använder monotoniska predikat istället för orena, icke-monotoniska konstruktioner i dina program:

• dif/2 är avsett att användas istället för icke-monotoniska konstruktioner som (\=)/2
• aritmetiska begränsningar (CLP (FD), CLP (Q) och andra) är avsedda att användas istället för modifierade aritmetiska predikat
• !/0 leder nästan alltid till icke-monotoniska program och bör undvikas helt.
• inställningsfel kan tas upp i situationer där du inte kan fatta ett bra beslut vid denna tidpunkt.

Kombinera monotonicitet med effektivitet

Det hävdas ibland att vi för effektivitetsskäl måste acceptera användningen av icke-monotoniska konstruktioner i verkliga Prolog-program.

Det finns inga bevis för detta. Ny forskning tyder på att den rena monotonundersättningen av Prolog kanske inte bara är tillräcklig för att uttrycka de flesta verkliga program, utan också acceptabelt effektiv i praktiken. En konstruktion som nyligen har upptäckts och uppmuntrar denna uppfattning är if_/3 : Den kombinerar monotonicitet med en minskning av valpunkter. Se Indexering diff / 2 .

Till exempel kod för formuläret:

pred(L, Ls) :-
    condition(L),
    then(Ls).
pred(L, Ls) :-
    \+ condition(L),
    else(Ls).

Kan skrivas med if_/3 som:

pred(L, Ls) :-
    if_(condition(L),
        then(Ls),
        else(Ls)).

och kombinerar monotonicitet med determinism.