Zoeken…


Redeneren over monotone predikaten

Monotone predikaten kunnen worden opgelost door declaratieve redenering toe te passen.

In pure Prolog kan een programmeerfout leiden tot een of alle van de volgende fenomenen:

  1. het predikaat slaagt niet in een geval waarin het zou moeten falen
  2. het predicaat faalt ten onrechte in een geval waarin het zou moeten slagen
  3. het predicaat loopt onverwacht in een lus waar het slechts een eindige reeks antwoorden zou moeten opleveren.

Als een voorbeeld, overweeg hoe we case (2) kunnen debuggen door een declaratieve redenering: we kunnen systematisch doelen van de clausules van het predicaat verwijderen en kijken of de query nog steeds mislukt. In monotone code kan het verwijderen van doelen hoogstens het resulterende programma algemener maken . Daarom kunnen we fouten opsporen door te kijken welke van de doelen tot de onverwachte mislukking leidt.

Voorbeelden van monotone predikaten

Voorbeelden van monotone predikaten zijn:

  • unificatie met (=)/2 of unify_with_occurs_check/2
  • dif/2 , waarmee ongelijkheid van termen wordt uitgedrukt
  • CLP (FD) beperkingen zoals (#=)/2 en (#>)/2 , met behulp van een monotone uitvoeringsmodus.

Prolog predicaten die alleen monotone doelen gebruiken, zijn zelf monotoon.

Monotone predikaten laten een verklarende redenering toe:

  1. Het toevoegen van een beperking (dat wil zeggen een doel) aan een query kan de reeks oplossingen hooguit verminderen , nooit uitbreiden.
  2. Het verwijderen van een doel van dergelijke predicaten kan de reeks oplossingen hoogstens uitbreiden , nooit verminderen.

Niet-monotone predikaten

Hier zijn voorbeelden van predikaten die niet monotoon zijn:

  • meta-logische predikaten zoals var/1 , integer/1 etc.
  • termvergelijking voorspelt zoals (@<)/2 en (@>=)/2
  • predicaten die !/0 , (\+)/1 en andere constructies die monotoniciteit breken
  • alle oplossingen predicaten zoals findall/3 en setof/3 .

Als deze predicaten worden gebruikt, kan het toevoegen van doelen leiden tot meer oplossingen, wat in strijd is met de belangrijke logische eigenschap die bekend is uit de logica dat het toevoegen van beperkingen de set oplossingen hoogstens kan verminderen , nooit uitbreiden.

Als gevolg hiervan zijn ook andere eigenschappen die we gebruiken voor declaratieve foutopsporing en andere redeneringen verbroken. Niet-monotone predikaten bijvoorbeeld breken de fundamentele notie van commutativiteit van conjunctie die bekend is uit de eerste-orde logica. Het volgende voorbeeld illustreert dit:

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

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

All-oplossingen predikaten zoals findall/3 breken ook de monotoniteit: het toevoegen van clausules kan leiden tot het falen van doelen die eerder waren gehouden . Dit gaat ook in tegen montonicity zoals bekend van de eerste-orde logica, waarbij het toevoegen van de feiten kunnen hooguit verhogen, nooit de set van de gevolgen daarvan te beperken.

Monotone alternatieven voor niet-monotone constructen

Hier zijn voorbeelden van het gebruik van monotone predicaten in plaats van onzuivere, niet-monotone constructies in uw programma's:

  • dif/2 is bedoeld om te worden gebruikt in plaats van niet-monotone constructies zoals (\=)/2
  • rekenkundige beperkingen (CLP (FD), CLP (Q) en andere) zijn bedoeld om te worden gebruikt in plaats van gemodificeerde rekenkundige predikaten
  • !/0 leidt bijna altijd tot niet-monotone programma's en moet volledig worden vermeden .
  • instantiëringsfouten kunnen optreden in situaties waarin u op dit moment geen goede beslissing kunt nemen.

Monotoniciteit combineren met efficiëntie

Er wordt wel eens beweerd dat we omwille van de efficiëntie het gebruik van niet-monotone constructen in echte Prolog-programma's moeten accepteren.

Hier is geen bewijs voor. Recent onderzoek geeft aan dat de pure monotone subset van Prolog niet alleen voldoende is om de meeste echte programma's tot uitdrukking te brengen, maar ook in de praktijk acceptabel efficiënt is. Een construct dat recent is ontdekt en deze visie aanmoedigt is if_/3 : het combineert monotoniciteit met een vermindering van keuzepunten. Zie Indexering dif / 2 .

Bijvoorbeeld code van het formulier:

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

Kan worden geschreven met if_/3 als:

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

en combineert monotoniciteit met determinisme.



Modified text is an extract of the original Stack Overflow Documentation
Licentie onder CC BY-SA 3.0
Niet aangesloten bij Stack Overflow