Ich habe eine interessante Frage, aber ich bin nicht sicher genau, wie Begriff es ...Wie finde ich die optimale Verarbeitungsreihenfolge?
das Lambda-Kalkül Betrachten. Für einen gegebenen Lambda-Ausdruck gibt es mehrere mögliche Reduktionsordnungen. Aber einige davon enden nicht, andere tun es.
Im Lambda-Kalkül stellt sich heraus, dass es eine bestimmte Reduktionsordnung gibt, die immer mit einer irreduziblen Lösung endet, wenn eine existiert. Es heißt normale Ordnung.
Ich habe einen einfachen Logiklöser geschrieben. Aber die Schwierigkeit ist, dass die Reihenfolge, in der die Constraints verarbeitet werden, einen großen Einfluss darauf hat, ob sie Lösungen findet oder nicht. Im Grunde frage ich mich, ob für meine Logik-Programmiersprache etwas wie eine normale Reihenfolge existiert. (Oder ob es unmöglich ist, für eine bloße Maschine determinis dieses Problem zu lösen.)
Also das ist, was ich bin nach. Vermutlich hängt die Antwort entscheidend davon ab, was genau der "einfache Logiklöser" ist. Also werde ich versuchen, kurz beschreiben es.
Mein Programm ist eng mit dem System von Kombinatoren in Kapitel 9 von The Fun of Programming (Jeremy Gibbons & Oege de Moor). Die Sprache hat die folgende Struktur:
Die Eingabe in den Löser ist ein einzelne Prädikat. Prädikate können Variablen beinhalten. Die Ausgabe des Solver ist 0 oder mehr Lösungen. Eine Lösung ist eine Menge von Variablenzuweisungen, die das Prädikat wahr werden lassen.
Variablen halten Ausdrücke. Ein Ausdruck ist eine Ganzzahl, ein Variablenname oder ein Tupel von Teilausdrücken.
Es gibt ein Gleichheitsprädikat, das Ausdrücke (nicht Prädikate) auf Gleichheit vergleicht. Es ist erfüllt, wenn die Substitution jeder (gebundenen) Variablen durch ihren Wert die beiden Ausdrücke identisch macht. (Insbesondere ist jede Variable gleich, gebunden oder nicht). Dieses Prädikat wird durch Vereinheitlichung gelöst.
Es gibt auch Operatoren für AND und OR, die in der offensichtlichen Weise arbeiten. Es gibt keinen NOT-Operator.
Es gibt einen Operator "exists", der im Wesentlichen lokale Variablen erstellt.
Die Einrichtung zu definieren benannte Prädikate ermöglicht rekursive Schleifen.
Einer der „interessanten Dinge“ über Logikprogrammierung ist, dass wenn Sie ein benannte Prädikat schreiben, es in der Regel arbeitet fowards und rückwärts (und manchmal sogar seitwärts). Kanonisches Beispiel: Ein Prädikat zur Verknüpfung zweier Listen kann auch dazu verwendet werden, eine Liste in alle möglichen Paare aufzuteilen.
Aber manchmal führt die Ausführung eines Prädikats rückwärts zu einer unendlichen Suche, es sei denn, Sie ordnen die Reihenfolge der Terme neu an. (ZB tauschen Sie LHS und RHS eines AND oder OR OR etwas aus.) Ich frage mich, ob es eine automatisierte Möglichkeit gibt, die beste Reihenfolge für die Ausführung der Prädikate zu finden, um eine sofortige Beendigung in allen Fällen zu gewährleisten, in denen die Lösungsmenge genau ist endlich.
Irgendwelche Vorschläge?
Es wahrscheinlich helfen wird, wenn Sie ein paar Beispiele für Programme in Ihrer Sprache zu veröffentlichen, und zeigen, wie verschiedene Strategien zur Reduzierung führen zu verschiedene Ergebnisse. –
@ n.m. Gute Idee. Ich werde versuchen, ein minimales Beispiel zu finden ... – MathematicalOrchid
Siehe auch [Presburger Arithmetik] (http://en.wikipedia.org/wiki/Presburger_arithmetic) falls Sie es vorher nicht gesehen haben - die Gültigkeit ist entscheidbar , und es erlaubt und, oder, nicht, für alle, und Induktion (obwohl vielleicht die Induktion nicht so mächtig ist wie die Rekursion, die Sie beschreiben). –