Reinheit der Prolog-Prädikate, die unreine Primitive verwenden

  

1. Ist das obige Prädikat plus / 3 wirklich rein?
  

Es hat ein seltsames Verhalten: Manchmal akzeptiert es arithmetische Ausdrücke und manchmal nicht; und dies, obwohl alle Argumente ausgewertet werden:

Ich wäre eher besorgt über die Ineffizienz von nat/1 für Fälle wie:

Es sieht also so aus, dass Ihre Definition rein ist. Diese Art der Programmierung macht es jedoch ziemlich schwierig, diese Eigenschaft zu garantieren. Eine minimale Änderung wird verheerende Auswirkungen haben.

  

2. Wie können Sie im Allgemeinen beweisen, dass eine bestimmte Beziehung eine logische Reinheit hat?
  

Der einfachste Weg ist die Konstruktion. Das heißt, nur reine monotone Bausteine ​​zu verwenden. Das heißt, Prolog ohne irgendwelche eingebauten und nur die Verbindung und Disjunktion von regulären Zielen verwendend. Jedes Programm, das auf diese Weise erstellt wird, wird auch rein und monoton sein. Dann führen Sie dieses Programm mit Prolog Flag-Check-Set auf true oder error .

Fügen Sie zu diesen reinen Einbauten wie (=)/2 und dif/2 hinzu.

Fügen Sie diesen Einfügungen, die versuchen, reine Beziehungen zu emulieren und Instanziierungsfehler zu erzeugen, wenn dies nicht möglich ist, Add-Ons hinzu. Denken Sie an (is)/2 und die arithmetischen Vergleichsprädikate. Einige von diesen sind ziemlich auf der Grenze wie call/N , was einige unreine Prädikate nennen könnte.

Fügen Sie library(clpfd) dem Flag clpfd_monotonic hinzu, das auf% co_de gesetzt ist %.

Viele Konstrukte sind für bestimmte Zwecke gut und rein, für andere aber unrein. Denken Sie an if-then-else, das für den arithmetischen Vergleich perfekt ist:

aber das funktioniert nicht zusammen mit einem reinen Ziel wie

Was bleibt, sind unreine Einbauten, die verwendet werden können, um Prädikate zu konstruieren, die sich rein verhalten; aber deren Definition als solche ist nicht mehr rein.

Betrachten Sie zum Beispiel wirklich grüne Schnitte. Diese sind extrem selten und noch seltener hier auf SO. Siehe dies und das .

Ein weiteres allgemeines Muster, um eine reine Beziehung zu liefern, sind Bedingungen wie:

Und um sich gegen Fälle zu schützen, die nicht sauber abgedeckt sind, können Fehler ausgelöst werden.

In Bezug auf die Frage "Ist das obige plus/3 wirklich rein?" Ich kann nur sagen: Ich habe keine Ahnung, welche Eigenschaften hier erhalten bleiben, weil der Code aufgrund all dieser extra logischen Prädikate so kompliziert und schwer zu folgen ist, dass es schwer ist zu sagen, was er eigentlich tut. Und ich muss in diesem Fall wirklich tun sagen, denn das ist weit entfernt von deklarativem Code, der beschreibt etwas, über das wir vergleichsweise leicht reden können. Alle Arten von Eigenschaften, die wir von deklarativem Code erwarten, können in diesem Fall zerstört werden.

Der beste Weg, um allgemein zu beweisen, dass eine Beziehung rein ist, besteht darin, sich auf die reine und monotone Teilmenge von Prolog zu beschränken. Aus diesem Grund ist diese Eigenschaft so wichtig, weil diese Untergruppe unter Komposition geschlossen ist. Sobald Sie diese Teilmenge verlassen, wird es sehr schnell sehr schwer, irgendwelche Eigenschaften über Ihre Programme zu beweisen, wie Ihr Beispiel schön zeigt.

Um zum Beispiel Ihre plus/3 monoton zu belegen, müssen Sie unter anderem zeigen, dass, wenn ?- plus(X, _, _), X = T für einen Begriff T fehlschlägt , ?- X = T, plus(X, _, _) nicht erfolgreich . Da es im Allgemeinen nicht entscheidbar ist, ob eine Anfrage fehlschlägt, loops oder erfolgreich ist und wir daher im Allgemeinen nicht einmal eine Seite dieser Implikation bestimmen können, geschweige denn beides, kann ich nur sagen: Viel Glück damit!