Kein nicht unterstütztes Verhalten

Mein core.logic-Fork, Teil 2 von 9. Übersicht · ← Relationale Maps für core.logic · Schnell machen →

Die erste Version relationaler Maps in diesem Fork funktionierte für die Queries, die ich im Kopf hatte. Als ich sie systematisch durchging, Modus für Modus, hatte sie Lücken: Kombinationen aus bekannten und unbekannten Argumenten, bei denen eine Relation aufgab, oder für einen Fall antwortete und die anderen stillschweigend fallen ließ.

In einer relationalen Bibliothek ist das kein kleines Problem. Der ganze Sinn einer Relation ist, dass man nicht wissen muss, in welche Richtung sie läuft. Wenn assoco rückwärts funktioniert, außer wenn, muss jeder Aufrufer die Ausnahme kennen, und dann ist es keine Relation mehr, sondern eine Funktion mit ein paar zusätzlichen Modi.

Also wurde die Regel: kein nicht unterstütztes Verhalten. Jede Relation ist in jedem Modus korrekt: Sie antwortet, scheitert, oder wartet und sagt, worauf sie wartet. Wenn das alles langsam machte, musste sich das Design ändern, nicht die Regel.

Es hat sich geändert. Dieser Post handelt von dem Design, das dabei herauskam.

Drei Arten von Map

Eine Map kann in einer Query drei Dinge sein, und sie auseinanderzuhalten ist der größte Teil des Designs.

Eine normale Map mit normalen Keys: {:a x :b 2}. Werte dürfen unbekannt sein, Keys sind feste Werte. Das ist der häufige Fall, und er muss so schnell bleiben wie upstream.
Eine normale Map mit unbekannten Keys: {k 1 :b 2}. Clojure erlaubt jeden Wert als Key, also kann ein Key in einer Query eine logische Variable sein oder ein Term, der eine enthält. So eine Map ist geschlossen: Sie hat genau diese Einträge.
Eine offene Map, (lmap {:a 1} | r): bekannte Einträge plus ein unbekannter Rest.

Die zentrale Invariante: Offene Maps haben nur ground Keys. Niemand schreibt offene Maps direkt; nur die Relationen der Bibliothek erzeugen sie, und sie legen nur feste Keys hinein. Unbekannte Keys gibt es nur in geschlossenen normalen Maps.

Diese eine Einschränkung beseitigt den schwierigsten Fall: Eine offene Map mit unbekannten Keys würde bedeuten, dass jeder unbekannte Key zu jedem Eintrag jedes Rests passen könnte, eine unbeschränkte Suche. Mit der Einschränkung sind offene Maps billig: Lookups sind Hash-Lookups, und der Rest wächst nur am Ende.

Der Rest jeder offenen Map trägt einen lacks-Constraint: Der Rest von (lmap {:a 1} | r) darf nie :a bekommen. Das hält „Einträge plus Rest“ zu einer disjunkten Vereinigung, und es gibt (lacks-keyo m :a) eine Bedeutung, noch bevor m bekannt ist.

Maps mit unbekannten Keys unifizieren

(== {k1 v k2 v} {:a 1 :b 1}) hat zwei Antworten: k1 = :a, k2 = :b und umgekehrt. Unifikation ist in core.logic eine Funktion von einer Substitution auf eine Substitution oder nil. Sie kann nicht zwei zurückgeben.

Die Optionen waren, die Verzweigung in die Suche zu verlagern (Unifikation zu einem Goal machen) oder Unifikation eine Funktion bleiben zu lassen und aufzuschieben. Ich habe beides gemacht, je nach Fall:

Das Matching als Goal auf einer sauberen Kopie des Zustands laufen lassen und nach zwei Antworten fragen.
Keine: Die Unifikation scheitert.
Eine: Darauf festlegen. Das ist der häufige Fall, {k 1 :b 2} gegen {:a 1 :b 2}, und er kostet überhaupt keine Suche: Es bleibt kein Choice Point zurück.
Zwei oder mehr: Die Unifikation ist wirklich mehrdeutig. Sie bleibt als ausstehender Constraint, der neu läuft, wenn eine seiner Variablen gebunden wird. Bevor eine Antwort reifiziert wird, wird jeder noch mehrdeutige Constraint erzwungen: Seine Alternativen werden als normale Suchzweige aufgezählt.

So bleiben deterministische Fälle deterministisch, und Mehrdeutigkeit wird nur dann zur Suche, wenn es sich nicht vermeiden lässt. Warten heißt auch, dass spätere Goals oft entscheiden, welche Zuordnung gilt, und die anderen Zweige nie erkundet werden.

Derselbe Mechanismus behandelt Relationen, die nicht weiterkommen. geto auf einer unbekannten Map mit einem unbekannten Key hat unendlich viele Antworten, also suspendiert es, bis die Map oder der Key bekannt wird. Passiert keins von beidem, erscheint es in der Antwort als Constraint.

Keys müssen verschieden bleiben

Eine Clojure-Map hat nie zwei gleiche Keys. In einer Query kann sie welche bekommen: Man baut {k1 1 k2 2}, während k1 und k2 ungebunden sind, und bindet dann beide an :a. Jetzt hat die „Map“ :a zweimal, was keine Clojure-Map kann, also muss dieser Zweig scheitern.

Die naheliegende Lösung, ein Constraint auf jeder Map mit unbekannten Keys, der bei jeder Bindung neu geprüft wird, war teuer: Jede Unifikation hätte fragen müssen, ob sie so eine Map berührt.

Der Trick: core.logic läuft ohnehin jeden Term ab, an den es eine Variable bindet, für den Occurs Check. Dieser Durchlauf merkt sich jetzt auch jede Map mit nicht-normalen Keys, an der er vorbeikommt, indem er einen Zähler erhöht, was auf dem häufigen Pfad fast nichts kostet. Hat sich der Zähler nach dem Binden bewegt, werden die Keys dieser Maps geprüft, und ein Constraint hält sie von da an verschieden.

In run-nc (ohne Occurs Check) findet der Durchlauf nicht statt. Dort werden Keys bei Maps geprüft, die mit einer anderen Map unifiziert oder an eine Relation übergeben werden, und Kollisionen in der Antwort werden beim Reifizieren erkannt: Die Map zurück in eine Clojure-Map zu überführen würde gleiche Keys zusammenlegen, also kommt die reifizierte Map kleiner heraus als der Term, und diese Antwort wird verworfen. Der Preis: Eine Map, die run-nc nur bindet und nie unifiziert, an keine Relation übergibt und nicht zurückgibt, wird nicht geprüft. Das passt zu dem, was run-nc ohnehin ist: ein Verzicht auf Prüfungen zugunsten der Geschwindigkeit, im Vertrauen darauf, dass es auf Termen benutzt wird, wo das sicher ist.

Kopierte Reste

Tabling und copy-term kopieren Terme mit frischen Variablen. Der Rest einer offenen Map, kopiert auf eine frische Variable, würde seinen lacks-Constraint verlieren und damit die Disjunktheit. Beide hängen die Constraints jetzt wieder an kopierte Reste an.

Was es kostet

Die Upstream-Benchmarks (zebra, nrev, n-queens, sudoku, dinesman, magic square, und appendo und membero mit Hunderten von Antworten) laufen im Rauschen von upstream. Ein Microbenchmark, der winzige Maps unifiziert, ist ein paar Prozent langsamer. Die Relationen selbst hatten eigene Probleme: Schnell machen.