Ein relationaler Clojure-Interpreter

(eval-expo expr env val) gilt, wenn expr in env zu val auswertet; env ist eine Map von Symbolen auf Werte. (evalo expr val) startet mit prim-env, das die Primitive enthält.

• Zahlen, Strings, Keywords, true, false, nil und () werten zu sich selbst aus
• Symbole werden in der Umgebung nachgeschlagen
• quote, if (mit oder ohne Else)
• fn mit einer Arität und einem Body, let mit sequenziellen Bindungen
• Anwendung von fns und Primitiven, und von Keywords, Maps und Vektoren als fns, wie in Clojure
• Vektor-Literale, Map-Literale mit konstanten Keys, Set-Literale aus Konstanten
• Primitive: list, vector, get, assoc, conj, =

Shadowing folgt Clojure. quote und if sind Special Forms, also ändert ein Local namens if nicht, was (if ...) bedeutet. fn und let sind Makros, und ein Local mit diesem Namen verdeckt sie. Primitive sind Werte in der Umgebung, also werden auch sie verdeckt und lassen sich herumreichen.

Jede Antwort unten stammt aus einem echten Lauf. Zeiten: eine frische JVM je Abfrage, das Beste aus 3 bis 5 Läufen nach einem Aufwärmlauf.

(run* [v] (evalo '(let [x 1 y [x 2]] {:a y :b (get {:c 3} :c)}) v))
;;=> ({:a [1 2], :b 3})

(run* [v] (evalo '(:b {:a 1 :b 2}) v))     ;;=> (2)
(run* [v] (evalo '({:a 1} :a) v))          ;;=> (1)

Lass einen Teil der Umgebung unbekannt, und der Interpreter sagt, was er gewesen sein muss. Das sind die Map-Relationen aus Teil 1, die hier arbeiten, innerhalb eines Interpreters:

(run* [m] (eval-expo '(get m :a) (env-with {'m m}) 1))
;;=> ((lmap {:a 1} | _0))          ;; any map with 1 at :a

(run* [m] (eval-expo '(assoc m :b 2) (env-with {'m m}) {:a 1 :b 2}))
;;=> ({:a 1} {:a 1, :b _0})        ;; m had no :b, or some :b

(run* [x] (eval-expo '(if x :yes :no) (env-with {'x x}) :no))
;;=> (false nil)                   ;; Clojure's two false values

(run* [k1 k2]
  (keywordo k1) (keywordo k2)
  (eval-expo (list 'get (list 'get 'm k1) k2) (env-with {'m {:a {:b 1} :c 2}}) 1))
;;=> ([:a :b])                     ;; the key path to 1, in 2.5 ms

Lass den Ausdruck unbekannt, und er schreibt Programme:

(run 8 [q] (evalo q 6))
;;=> (6 (quote 6) (if () 6 _0) ((if _0 6 _1) :- (numbero _0))
;;    (if () (quote 6) _0) (let [] 6) ...)

(if () 6 _0) stimmt: In Clojure ist die leere Liste wahr.

Er kann auch eine fn aus Beispielen finden. Gesucht ist ein Body, sodass (fn [m] body) jede Eingabe auf ihre Ausgabe abbildet:

Die dritte Antwort ist eine Nachschlagetabelle der Beispiele: korrekt, und das billigste Programm, das es gibt. Barliman verbietet auf dieselbe Weise, die Beispiele ins Programm zu kopieren, mit absento. Mit vorgegebener Form des Aufrufs braucht die letzte 5 ms:

(run 1 [b]
  (fresh [x y z] (== b (list 'assoc x y z)))
  (eval-expo b (env-with {'m {:a 1}}) {:a 1 :b 2})
  (absento 1 b))      ;; no copying 1 from the answer into a quote
;;=> ((assoc m :b 2))

Eine Quine in Clojure-Syntax läuft vorwärts und wertet zu sich selbst aus:

(def quine '((fn [x] (list x (list 'quote x)))
             '(fn [x] (list x (list 'quote x)))))
(run* [v] (evalo quine v))   ;;=> (quine), in 2.4 ms

Bei der Suche nach einer fällt dieser Interpreter zurück:

Ohne "ein Aufruf" antwortet (evalo q q) sofort mit (): Die leere Liste wertet zu sich selbst aus, ebenso nil, Zahlen und Keywords.

Die Quine, die er mit vorgegebener Form findet, ist die klassische, in Clojure-Syntax, mit x als beliebigem Symbol außer dem Namen eines Primitivs oder &:

((fn [_0] (list _0 (list (quote quote) _0)))
 (quote (fn [_0] (list _0 (list (quote quote) _0)))))

Der Interpreter aus dem Quine-Paper, den faster-miniKanren in seinen Tests hat, kennt fünf Formen: quote, list, Symbole, Anwendung mit einem Argument und lambda mit einem Argument. Dieser hier hat viel mehr Wege, jeden Teilausdruck zu bauen: sechs Arten von Konstanten, if, let, beliebig viele Argumente, Vektor-, Map- und Set-Literale und Daten, die man aufrufen kann. Eine Suche nach einem Programm von der Größe einer Quine zahlt dafür an jedem Knoten. Die meisten der zusätzlichen Wege sind auch billige Wege zu schummeln: ({:k E} :k) ist E mit Extraschritten, und die Suche probiert auch die.

Beim Bauen kamen Lücken im Fork selbst ans Licht, alle inzwischen mit Tests behoben:

• Listen und Vektoren sind =, aber Code unterscheidet sie. (f x) ist ein Aufruf und [f x] ist ein Vektor. Die Typ-Constraints, die symbolo nutzt, kennen jetzt auch Liste, Vektor, Map und Set, und eine Variable, die eines davon bekommen hat, kann später weder eine Zahl noch die andere Art von Sequenz werden. Die Map- und Vektor-Relationen lesen die Art, also behandelt geto eine unbekannte Variable, von der bekannt ist, dass sie ein Vektor ist, als Vektor.
• keywordo, neben symbolo, numbero und stringo.

• Wartende Antworten, die nicht gelten konnten. geto auf einer unbekannten Map mit einem unbekannten Key wartet, weil eine offene Map nur bekannte Keys hält (Teil 2). Während es wartete, gab es Antworten ohne Lösung, und die Synthese-Suchen oben waren voll davon:

  • zwei wartende =geto=s auf denselben Key derselben Map mit verschiedenen Werten
  • eine Map, deren Wert an einem Key die Map selbst enthält
  • (absento 1 m) zusammen mit einem wartenden geto, das 1 in m legt

  Jeder dieser Fälle schlägt jetzt fehl. Ein wartendes geto wacht auch auf, wenn seine Map-Variable mit einer anderen Variable unifiziert wird, sodass zwei wartende =geto=s auf denselben Key sich treffen.

• Suchen, die nie endeten. Die erste Fassung dieses Posts hatte Bodies in 0,2–0,5 s, und weder die assoc-Beispiele noch die Quine mit Form ((fn [x] b) 'B) innerhalb von Minuten. Für die Zahlen oben hat sich der Interpreter kaum geändert. Die Relationen darunter hatten Fälle, die ewig liefen oder den Stack sprengten, wo sie hätten fehlschlagen oder handeln sollen, und die Suchen waren voll davon:

  • ein Element an unbekanntem Index eines offenen Vektors, das den Vektor enthalten müsste, oder etwas, das absento von ihm fernhält: jede Position wurde probiert, ewig
  • zwei Zugriffe auf denselben unbekannten Index mit verschiedenen Elementen
  • conjo auf einer Variable, die schon als Vektor bekannt ist, wartete, statt zu handeln, und Ketten davon sprengten den Stack
  • ein assoc an unbekanntem Index in ein bekanntes Ergebnis gab seine Antworten und endete dann nie
  • absento durchsuchte bei jedem Aufruf jeden Constraint im Store

  Jeder Fall schlägt jetzt sofort fehl oder handelt sofort, wie es die Map-Relationen schon taten. Jeder verletzte die Regel aus Teil 2, auch außerhalb des Interpreters.

• Die Quine-Suche ohne Form. (evalo q q) mit nur "q ist ein Aufruf" füllt einen 4-GB-Heap, bevor sie eine findet. Jede Variable unter einem quote trägt einen Constraint, der fn-Werte aus gequoteten Daten heraushält, und die Suche erzeugt Millionen davon. Die Interpreter von faster-miniKanren verdanken ihr Tempo außerdem einer kleinen Sprache und einer sorgfältig geordneten Suche; dieser hat noch keins von beidem.
• Antworten, die warten. Ein Programm, das ein noch nicht gewähltes Keyword auf unbekannte gequotete Daten anwendet, (_0 '_1), gibt eine Antwort mit einem wartenden geto, weil weder die Map noch der Key bekannt ist. Diese Antworten sind korrekt, als Bedingungen, aber es sind keine Programme, die man schreiben würde.
• Nicht in der Sprache: def, do, loop/recur, fns mit mehreren Aritäten und variadische fns, Destructuring, mehr als ein Ausdruck im Body, Map-Keys und Set-Elemente, die keine Konstanten sind, Chars und der Rest von clojure.core. Ein Ausdruck außerhalb dieser Teilmenge schlägt in jedem Modus fehl.
• Wo es von Clojure abweicht, schlägt es fehl, wo Clojure nil liefert: get mit einem Index, den ein Vektor nicht hat, oder mit einem Key auf einem Vektor, der weder Index noch Keyword ist, get auf einer Liste, assoc auf nil. = schlägt bei fns fehl, die Clojure über Identität vergleicht.

Generiert von Claude im Auftrag von Benjamin Schwerdtner.