Seite an Seite mit miniKanren

script/fmk_tests.py übersetzt die Testsuite von faster-miniKanren nach core.logic: 355 der 357 Tests (zwei berechnen ihre erwartete Antwort und lassen sich nicht übersetzen). Sie decken ==, =/=, symbolo, numbero, stringo, absento, Typinferenz und die Arithmetik aus The Reasoned Schemer ab. Die beiden Systeme drucken Antworten unterschiedlich, deshalb werden beide Seiten vor dem Vergleich normalisiert (_.0 und _0, =/= und !=, Variablennummerierung, Reihenfolge der Constraints).

Beim ersten Lauf stimmten 202 von 355 überein. Der Rest ging auf sieben Bugs und ein fehlendes Feature zurück.

Alle außer dem ersten geben falsche Antworten: entweder Antworten, die keine Lösungen sind, oder fehlende Lösungen. Alle sind behoben, und jeder hat seinen eigenen Regressionstest.

Das fehlende Feature war das Aufräumen der Antworten. faster-miniKanren lässt Constraints weg, die für die Antwort keine Rolle spielen können. Das ist jeder Constraint auf einer Variablen, die die Antwort nicht zeigt, x ≠ 5, wenn x ein Symbol ist, x ≠ y, wenn (absento x y) da ist, und so weiter. core.logic druckte sie alle. Jetzt vereinfacht es auf dieselbe Weise:

;; miniKanren
(run* (q) (fresh (x) (== q `(,x)) (symbolo x) (=/= x 'lambda)))
;;=> (((_.0) (=/= ((_.0 lambda))) (sym _.0)))

;; core.logic
(run* [q] (fresh [x] (== q [x]) (symbolo x) (!= x 'lambda)))
;;=> (([_0] :- (!= (_0 lambda)) (clojure.core.logic/symbolo _0)))

Jetzt stimmen 352 von 355 überein, und alle laufen mit lein test, in etwa drei Sekunden. Die drei abweichenden Tests werden übersprungen und sind im Skript dokumentiert:

• Suchreihenfolge: Einer ist run 12 auf einem unendlichen Stream, wo eine andere Suchreihenfolge andere erste zwölf liefert.
• Äquivalente Form: Einer druckt denselben Constraint in einer anderen Normalform: (!= (_0 _1) (_1 _2)), wo miniKanren ((_.0 _.1) (_.0 _.2)) schreibt.
• Redundanter Constraint: Einer zeigt einen zusätzlichen Constraint, den eine Ungleichung schon impliziert.

Programme, die nur Listen nutzen, lassen sich Zeile für Zeile übersetzen:

;; miniKanren
(defrel (appendo l s out)
  (conde
    [(== '() l) (== s out)]
    [(fresh (a d res)
       (== `(,a . ,d) l)
       (== `(,a . ,res) out)
       (appendo d s res))]))

(run* (x y) (appendo x y '(1 2 3)))
;;=> ((() (1 2 3)) ((1) (2 3)) ((1 2) (3)) ((1 2 3) ()))

;; core.logic, in a namespace that excludes core.logic's own appendo
(defrel appendo [l s out]
  (conde
    [(== '() l) (== s out)]
    [(fresh [a d res]
       (== (lcons a d) l)
       (== (lcons a res) out)
       (appendo d s res))]))

(run* [x y] (appendo x y '(1 2 3)))
;;=> ([() (1 2 3)] [(1) (2 3)] [(1 2) (3)] [(1 2 3) ()])

Der Rest dieses Posts handelt von Daten, die miniKanren als Listen kodieren muss.

miniKanren hat keine Maps. Die übliche Kodierung ist eine Assoziationsliste, wie in der Umgebung des relationalen Interpreters:

(defrel (lookupo k m v)
  (fresh (k2 v2 rest)
    (== `((,k2 . ,v2) . ,rest) m)
    (conde
      [(== k k2) (== v v2)]
      [(=/= k k2) (lookupo k rest v)])))

Einen Schlüssel nachschlagen funktioniert in beiden gleich, vorwärts und rückwärts:

(run* (k) (lookupo k '((a . 1) (b . 2)) 2))   ;;=> (b)

(run* [k] (geto {:a 1 :b 2} k 2))              ;;=> (:b)

Bei der Frage nach einer Map mit zwei Einträgen trennen sich die Wege. Eine Map hat unendlich viele Assoziationslisten: jede Reihenfolge, beliebige andere Schlüssel dazwischen. Also zählt miniKanren sie auf, ohne Ende:

(run 4 (m) (lookupo 'a m 1) (lookupo 'b m 2))
;;=> (((a . 1) (b . 2) . _.0)
;;    ((b . 2) (a . 1) . _.0)
;;    (((a . 1) (_.0 . _.1) (b . 2) . _.2) (=/= ((_.0 b))))
;;    (((a . 1) (_.0 . _.1) (_.2 . _.3) (b . 2) . _.4) (=/= ((_.0 b)) ((_.2 b)))))
;;   run* never returns

core.logic antwortet einmal, mit einer offenen Map, und hört auf:

(run* [m] (geto m :a 1) (geto m :b 2))
;;=> ((lmap {:b 2, :a 1} | _0))

Gleichheit ist der andere Unterschied. Zwei Assoziationslisten in verschiedener Reihenfolge unifizieren nicht, obwohl sie dieselbe Map bedeuten:

(run* (q) (== '((a . 1) (b . 2)) '((b . 2) (a . 1))))   ;;=> ()

(run* [q] (== {:a 1 :b 2} {:b 2 :a 1}))   ;;=> (_0)
(run* [x k] (== {:a x :b 2} {k 2 :a 1}))  ;;=> ([1 :b])

Bei Sets wiederholt sich das Muster. Mit Listen und membero ist jede Reihenfolge und jedes Auffüllen eine weitere Antwort:

(run 4 (s) (membero 1 s) (membero 2 s))
;;=> ((1 2 . _.0) (2 1 . _.0) (1 _.0 2 . _.1) (1 _.0 _.1 2 . _.2))

(run* [s] (containso s 1) (containso s 2))
;;=> ((lset #{1 2} | _0))

Set-Gleichheit und Mengenalgebra laufen in jede Richtung:

(run* [x y] (== #{x y} #{1 2}))           ;;=> ([1 2] [2 1])
(count (run* [a b] (uniono a b #{1 2})))  ;;=> 9, each element in a, b or both

appendo schaut nur auf Elemente. Wenn beide Listen unbekannt sind, erzeugt es Längen eine nach der anderen, und wenn die Antwort von Längen abhängt, merkt es das nie:

(run 1 (x) (appendo x '(1) x))
;;   no answer within 20 seconds: it tries ever longer x

(run 1 (x) (fresh (l r) (appendo x '(1) l) (appendo '(1) x r) (appendo r '(2) l)))
;;   no answer within 20 seconds

Die Vektoren des Forks lösen zuerst die Längen (Teil 4), also schlagen beide sofort fehl:

(run* [x] (concato x [1] x))
;;=> ()        ;; |x| + 1 ≠ |x|

(run* [x] (fresh [l r] (concato x [1] l) (concato [1] x r) (concato r [2] l)))
;;=> ()        ;; |x| + 1 ≠ |x| + 2

Wo es unendlich viele Antworten gibt, zählen beide sie auf: x ++ (1) = (1) ++ x ergibt (() (1) (1 1)) für run 3 in faster-miniKanren und ([] [1] [1 1]) im Fork.

Längenschließen macht nicht jede Wortgleichung endlich. Wenn die Längen übereinstimmen, wie bei x ++ [1] = [2] ++ x, zeigen erst die Elemente den Konflikt, und auch der Fork zählt ohne Ende auf (Teil 5).

Indizierung und Pfade haben kein direktes Gegenstück in miniKanren. Sie bräuchten Peano-Zahlen und eine Kette von Lookups:

(run* [i] (ntho [:a :b :a] i :a))                                  ;;=> (0 2)
(run* [p] (get-ino {:users [{:name "ada"} {:name "bob"}]} p "bob"))
;;=> ((:users 1 :name))

• Notation: _0 für _.0, != für =/=, symbolo für sym, und Antworten als (value :- constraints).
• Suchreihenfolge: conde, fresh und defrel verschränken anders, also kann run n andere erste n Antworten liefern. run* liefert dieselbe Menge.
• ClojureScript: Nichts davon läuft dort bisher; siehe Future Work.

Generiert von Claude im Auftrag von Benjamin Schwerdtner.