Vektoren

Vektoren, Listen und partielle Listen unifizieren schon als Sequenzen miteinander. (== [a b] (lcons 1 r)) funktioniert. Was fehlt, ist alles, was einen Vektor zum Vektor macht:

• Die einzige teilweise bekannte Sequenz ist ein bekannter Anfang plus ein unbekannter Rest, (1 2 . _0). Über das Ende einer Sequenz unbekannter Länge lässt sich nichts wissen.
• Antworten, die aus partiellen Listen gebaut werden, kommen als Listen zurück, nicht als Vektoren.
• Es gibt keine Relationen für Positionen (nth), Länge (count), das Ende (peek, pop), Ausschnitte (subvec) oder Konkatenation, die Vektoren kennen. Upstreams conjo ist ein Constraint, der wartet, bis zwei seiner Argumente ground sind.

Ein teilweise bekannter Vektor ist ein bekannter Anfang, eine unbekannte Mitte und ein bekanntes Ende. In Antworten wird er so ausgegeben:

(lvec [a b] | _0 | [y z])

Die Mitte ist eine ungebundene Variable. Sie steht für einen Vektor beliebiger Länge, auch null. Eine partielle Liste (a b . t) ist der Spezialfall mit leerem Ende.

Warum ein Ende: Clojure-Vektoren wachsen hinten. conj, peek und pop wirken auf das letzte Element. Mit nur Anfang und Rest müsste jede dieser Operationen über die unbekannte Länge suchen. Mit einem Ende geht es direkt:

(conjo v x out)   ;; out is [f | m | b x]: no search
(peeko v x)       ;; the last of b, if b isn't empty

Ist b leer, hat peeko zwei Fälle: Die Mitte ist nicht leer (dann ist m = [| m' | x], eine allgemeine Antwort), oder sie ist leer und x ist das letzte Element des Anfangs. Endlich viele Zweige, nie eine unbeschränkte Suche.

Das ist dieselbe Idee wie Prologs Differenzlisten, die das Ende einer Liste erreichbar machen, erweitert auf beide Enden.

Unifikation von [f1 | m1 | b1] mit [f2 | m2 | b2]:

1. Die Anfänge Element für Element unifizieren, so weit beide reichen. Dasselbe für die Enden, von hinten.
2. Was übrig bleibt: Höchstens eine Seite hat noch einen Anfang übrig, und höchstens eine hat noch ein Ende übrig.
3. Hat eine Seite nichts übrig, ist ihre Mitte die andere Seite: eine einzige Bindung.
4. Sonst gilt m1 ++ B = F ++ m2: Die beiden Mitten überlappen auf unbekannte Weise. Es gibt höchstens |F| + 1 Fälle: m1 deckt ganz F ab (eine allgemeine Antwort mit frischer Mitte), oder endet innerhalb von F an einer Stelle, an der der Rest von F in B passt.

Mit zwei verschiedenen Mitten ist Fall 4 endlich. Er nutzt deshalb denselben Mechanismus wie die Map-Unifikation mit unbekannten Keys: ausprobieren, festlegen, wenn genau ein Fall übrig bleibt, sonst offen halten, und erst vor dem Reifizieren aufzählen.

Mit derselben Mitte auf beiden Seiten ist er es nicht. [| x | 1] = [2 | x |], also x ++ [1] = [2] ++ x, hat keine Lösung, aber jede Länge besteht den Längencheck (|x| + 1 auf beiden Seiten), also endet das Aufzählen nie. Das ist eine echte Wortgleichung. Die Relation kann jede Antwort auflisten, aber sie kann nicht immer in endlicher Zeit scheitern. (Teil 5 hat die Theorie.)

Das volle Problem, beliebig viele unbekannte Stücke aneinandergehängt, ist das Lösen von Wortgleichungen. Das ist entscheidbar, aber sehr schwer. Deshalb hat der Term genau einen unbekannten Teil. Die Konkatenation zweier offener Vektoren (concato) ist eine Relation, die wartet, kein Term.

Jeder offene Vektor hat eine Länge, und über Längen wird exakt geschlossen, bevor irgendetwas aufgezählt wird. Eine Länge ist eine Konstante plus eine Summe der Längen unbekannter Mitten. concato stellt |out| = |a| + |b| auf, die Unifikation zweier Vektoren setzt ihre Längen gleich, und diese linearen Gleichungen werden durch Elimination gelöst, jede Länge mindestens 0. Unmögliche Längensysteme scheitern dann sofort: x ++ [1] = [1] ++ x ++ [2] scheitert an |x| + 1 ≠ |x| + 2, ohne eine einzige Länge auszuprobieren. (Teil 5 erklärt, warum Längen diese Behandlung bekommen.)

Warum nicht der FD-Solver von core.logic? Er engt Intervalle Schritt für Schritt ein. Längen haben keine obere Schranke, und bei |x| + 1 = |x| + 2 mit Längen bis 10.000 läuft der Stack über, bevor er den Widerspruch bemerkt. FD-Variablen funktionieren trotzdem mit counto: Eine Längenrelation wartet, bis eine FD-Variable gelabelt ist, und das FD-Labeling zählt dann nur ihre Domäne auf.

Ist eine Länge oder Position am Ende noch unbekannt, zählen die Relationen auf:

(run 3 [i v] (ntho v i :x))
;;=> ([0 (lvec [:x] | _0 | [])]
;;    [1 (lvec [_0 :x] | _1 | [])]
;;    [2 (lvec [_0 _1 :x] | _2 | [])])

Die Mitte bleibt in jeder Antwort offen: Nichts bindet ihre Länge an etwas. Auf einem offenen Vektor sind das unendlich viele Antworten, genau wie membero schon auf einer partiellen Liste. Mit einer endlichen FD-Domäne wird nur diese Domäne aufgezählt:

(run* [v n] (fd/in n (fd/interval 1 2)) (counto v n) (ntho v 0 :a))
;;=> ([[:a] 1] [[:a _0] 2])

Eine bekannte Länge schließt den Vektor und füllt die Mitte mit frischen Variablen:

(run* [q] (fresh [v] (ntho v 0 :a) (ntho v 2 :c) (counto v 3) (== q v)))
;;=> ([:a _0 :c])

Und Längen, die nicht zusammenpassen können, scheitern vor jedem Aufzählen. Hier gilt |a| = |x| + 1 = |b|, aber auch |a| = |b| + 1:

(run* [q] (fresh [x a b]
            (concato x [1] a) (concato [1] x b) (concato b [2] a)
            (== q 1)))
;;=> ()

(run* [a b] (concato a b [1 2 3]))
;;=> ([[] [1 2 3]] [[1] [2 3]] [[1 2] [3]] [[1 2 3] []])

(run* [v] (assoco v 1 :x [1 :x 3]))
;;=> ([1 _0 3])        ;; v had anything at index 1

geto und assoco funktionieren auf Maps und Vektoren, wie get und assoc in Clojure. Pfade durch verschachtelte Daten funktionieren also:

(run* [x] (fresh [u e]
            (geto {:users [{:name "a"} {:name "b"}]} :users u)
            (geto u 1 e)
            (geto e :name x)))
;;=> ("b")

Ist noch nicht bekannt, ob etwas eine Map oder ein Vektor ist, und der Key ist ein Index, dann wartet die Relation und probiert beides, bevor die Antwort herauskommt:

(run* [m] (geto m 0 1))
;;=> ((lmap {0 1} | _0) (lvec [1] | _0 | []))

Diese Kette von geto ist get-in, also bekommt sie einen Namen. (get-ino m ks v) sagt: (get-in m ks) ist v, durch jede Mischung aus Maps und Vektoren, und der Pfad ist einfach ein weiteres Argument. Ein paar Daten:

(def db {:users [{:name "ada" :age 36} {:name "bob" :age 40}]
         :admin {:name "ada" :age 36}})

Vorwärts ist es get-in. Mit unbekanntem Pfad findet es, wo ein Wert steht:

(run* [x] (get-ino db [:users 1 :name] x))   ;;=> ("bob")
(run* [p] (get-ino db p "ada"))              ;;=> ((:admin :name) (:users 0 :name))

Ein Teil des Pfads kann unbekannt sein, und der Wert kann unbekannte Teile haben:

(run* [i n] (get-ino db [:users i :name] n))
;;=> ([0 "ada"] [1 "bob"])

(run* [p a] (get-ino db p {:name "ada" :age a}))
;;=> ([(:admin) 36] [(:users 0) 36])         ;; jede Map, die ada ist, und wo

Ein Map-Literal unifiziert exakt: {:name "ada" :age a} findet Maps mit genau diesen zwei Keys und keinen anderen. Für mindestens bestimmte Keys nimmt matcho ein Muster: Eine Map darin passt auf eine Map mit mindestens ihren Keys, ein Set auf ein Set mit mindestens seinen Elementen, ein Vektor auf eine Folge seiner Länge, alles verschachtelt. Mit get-ino ist das eine kleine Abfragesprache:

(run* [p n] (fresh [u] (get-ino db p u) (matcho u {:age 40 :name n})))
;;=> ([(:users 1) "bob"])                    ;; alles mit Alter 40, egal welche Keys sonst

(run* [p] (fresh [u] (get-ino db p u) (matcho u {:name "ada"})))
;;=> ((:admin) (:users 0))

(run* [a b] (matcho db {:users [{:name a} {:name b}]}))
;;=> (["ada" "bob"])

matcho läuft auch rückwärts: Mit unbekanntem x antwortet (matcho x {:a {:b 1}}) mit (lmap {:a (lmap {:b 1} | _0)} | _1), der offenen Map, die das Muster beschreibt. Das Muster selbst sind Clojure-Daten, gelesen, wenn das Goal gebaut wird; eine Logikvariable darin steht also für einen Wert, nicht für ein Teilmuster. Es verallgemeinert featurec, das wartet, bis die Map bekannt ist, statt sie zu bauen, und in verschachtelte Maps schaut, aber nicht in Vektoren oder Sets.

Mit unbekannten Daten sagt es, wie die Daten aussehen müssen, und legt nicht fest, ob :users eine Map mit Key 0 oder ein Vektor ist:

(run 2 [d] (get-ino d [:users 0 :name] "bob"))
;;=> ((lmap {:users (lmap {0 (lmap {:name "bob"} | _0)} | _1)} | _2)
;;    (lmap {:users (lvec [(lmap {:name "bob"} | _0)] | _1 | [])} | _2))

assoc-ino ist assoc-in. Rückwärts findet es aus den Daten vorher und nachher den Pfad, der sich geändert hat, und aus dem Ergebnis allein jeden Wert, von dem assoc-in ausgegangen sein könnte:

(run* [out] (assoc-ino db [:users 1 :age] 41 out))
;;=> ({:admin {:name "ada", :age 36}, :users [{:name "ada", :age 36} {:name "bob", :age 41}]})

(run* [p] (assoc-ino db p 37 (assoc-in db [:admin :age] 37)))
;;=> ((:admin :age))

(run* [m] (assoc-ino m [:a :b] 1 {:a {:b 1}}))
;;=> (nil {} {:a nil} {:a {}} {:a {:b _0}})

Das letzte ist Clojures assoc-in rückwärts gelesen: nil gilt als leere Map, und fehlende Ebenen werden angelegt, also ergeben alle fünf Startwerte {:a {:b 1}}.

(= [1 2] '(1 2)) ist in Clojure wahr, und core.logic unifiziert die beiden schon. Das bleibt so. Antworten, die die Vektor-Relationen bauen, kommen als Vektoren zurück.

• Unbekannte Art. conj, peek und pop wirken bei Vektoren und Listen an verschiedenen Enden, und count einer unbekannten Map hat keine endliche Antwort. Deshalb warten conjo, peeko, popo und counto auf einer Collection, deren Art noch unbekannt ist, und erscheinen in der Antwort als Constraints, z. B. (_0 :- (clojure.core.logic/counto _0 3)).
• Unendlich viele Antworten. ntho mit unbekanntem Index oder counto mit unbekannter Länge hat auf einem offenen Vektor unendlich viele Antworten. Dafür run n nehmen. Positionen werden fair aufgezählt: Antwort k deckt Position k in der Mitte ab und jede Position im Ende, die eine Mitte passender Länge zulässt.
• Wortgleichungen. Eine Mitte mit Elementen drumherum, gleichgesetzt mit sich selbst mit anderen Elementen drumherum, x ++ [1] = [2] ++ x, wird über die Länge von x aufgezählt. Das findet jede Antwort, aber wenn es keine gibt, hört es nicht auf.

Weiter: Literatur und Parität mit miniKanren.

Generiert von Claude im Auftrag von Benjamin Schwerdtner.