提交: 0f322cea91c2fa1e671ada0a2ab8fda1477c7e44 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修訂: 0f322cea91c2fa1e671ada0a2ab8fda1477c7e44 (tree)
• 時間: 2023-01-28 14:30:24
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Search backwards through eval° and cammy°.

I figured it out for eval°, but I do not at all understand why cammy° is
improved by this. Nonetheless, I was able to replace cammy-synth° and
the entire pile of hacks. As a bonus, previous tests which timed out are
now successfully finding valid expressions; djinn is cleverer!

Change Summary

• modified: movelist/cammy-djinn.scm
• modified: movelist/cammyo.scm
• modified: movelist/rels.scm
• modified: todo.txt

差異

--- a/movelist/cammy-djinn.scm
+++ b/movelist/cammy-djinn.scm
@@ -10,7 +10,7 @@
     (begin (display (car xs)) (newline) (print-each (cdr xs)))))
 
 (define (djinn x s t)
-  (print-each (run x (q) (cammy-synth° q s t))))
+  (print-each (run x (q) (cammy° q s t))))
 
 (match (map (lambda (s) (read (open-input-string s)))
             (command-line-arguments))

--- a/movelist/cammyo.scm
+++ b/movelist/cammyo.scm
@@ -1,4 +1,4 @@
-(module cammyo (cammy° cammy-prim° cammy-synth° eval°)
+(module cammyo (cammy° cammy-prim° eval°)
   (import scheme)
   (import (chicken pretty-print))
   (import (mini-kanren))
@@ -80,97 +80,13 @@
       ; Categories
       ((== expr 'id) (== s t))
       ((fresh (f g) (== expr `(comp ,f ,g))
-              (fresh (y) (cammy° f s y) (cammy° g y t))))
+              ; XXX: Why backwards? Should be same rationale as in eval°, but
+              ; why does it work on types and not just elements?
+              (fresh (y) (cammy° g y t) (cammy° f s y))))
       ))
 
-  ; Syntactic composition enforcing normal form. This is just a synthesis helper.
-  ; Cammy × Cammy <-> Cammy
-  (define (comp-s° f g fg) (=/= f 'id) (=/= g 'id) (== fg `(comp ,f ,g)))
-
-  ; Cammy expressions which are theorems of BCI combinator calculus.
-  ; Cammy <-> Ty × Ty × Comb
-  (define (bci° expr s t comb)
-    (conde
-      ((== expr 'id) (== s t) (== comb 'I))
-      ((fresh (f g u cf cg) (== expr `(comp ,f ,g)) (== comb `((B ,cg) ,cf))
-              (bci° f s u cf) (bci° g u t cg)))
-      ))
-
-  ; Like cammy°, but suitable for type-directed term synthesis. All expressions
-  ; are normalized, and logical clauses are ordered to try some expert strategies.
-  ; Cammy <-> Ty × Ty
-  (define (cammy-synth° expr s t)
-    ; s, t, u, v are types
-    ; f, g are Cammy expressions
-    (fresh (f g u v)
-      ; (project (expr s t) (begin (pp `(synth? ,expr : ,s -> ,t)) succeed))
-      (conde
-        ; Try primitives first.
-        ((cammy-prim° expr s t))
-        ; Is it a BCI theorem?
-        ((fresh (comb) (bci° expr s t comb)))
-        ; Is it any arrow into 1?
-        ((== t '1)
-         ; NB: ignore : X -> 1, but only when X ≠ 1, because otherwise it's
-         ; the unique arrow, id : 1 -> 1
-         (conde
-           ((== s '1) (== expr 'id))
-           ((=/= s '1) (== expr 'ignore))))
-        ; Is it an NT?
-        ((== `(pair ,s ,s) t) (== expr 'dup))
-        ((== s `(pair ,t ,u)) (== expr 'fst))
-        ((== s `(pair ,u ,t)) (== expr 'snd))
-        ((== s `(pair ,u ,v)) (== t `(pair ,v ,u)) (== expr 'swap))
-        ((== s `(pair (hom ,u ,t) ,u)) (== expr 'app))
-        ((== `(sum ,s ,u) t) (== expr 'left))
-        ((== `(sum ,u ,s) t) (== expr 'right))
-        ; Is it a tuple lookup?
-        ((== s `(pair ,u ,v))
-         (conde
-           ((comp-s° 'fst f expr) (cammy-synth° f u t))
-           ((comp-s° 'snd f expr) (cammy-synth° f v t))))
-        ; Is it a case analysis?
-        ((== s `(sum ,u ,v)) (cammy-synth° f u t) (cammy-synth° g v t) (== expr `(case ,f ,g)))
-        ; Is it a tagging or return value?
-        ((== t `(sum ,u ,v))
-         (conde
-           ((comp-s° f 'left expr) (cammy-synth° f s u))
-           ((comp-s° f 'right expr) (cammy-synth° f s v))))
-        ; Is it a graph?
-        ; NB: Want to disallow (pair id id)
-        ((== `(pair ,s ,u) t) (=/= f 'id) (cammy-synth° f s u) (== expr `(pair id ,f)))
-        ((== `(pair ,u ,s) t) (=/= f 'id) (cammy-synth° f s u) (== expr `(pair ,f id)))
-        ; Is it a curry?
-        ((== t `(hom ,u ,v)) (cammy-synth° f `(pair ,s ,u) v) (== expr `(curry ,f)))
-        ; Is it an application?
-        ((cammy-synth° f s `(hom ,u ,t)) (cammy-synth° g s u) (comp-s° `(pair ,f ,g) 'app expr))
-        ; Is it a pair-builder?
-        ((== `(pair ,u ,v) t) (cammy-synth° f s u) (cammy-synth° g s v) (== expr `(pair ,f ,g)))
-        ; Does it result in a list?
-        ((== t `(list ,u))
-         (conde
-           ((== s '1) (== expr 'nil))
-           ((== s `(pair ,u (list ,u))) (== expr 'cons))))
-        ; Is it primitive recursive?
-        ((== s 'N) (cammy-synth° f '1 t) (=/= g 'id) (cammy-synth° g t t) (== expr `(pr ,f ,g)))
-        ; Is it a composition?
-        ; ((comp-s° f g expr) (cammy-synth° f s u) (cammy-synth° g u t))
-        )
-      ; (project (expr s t) (begin (pp `(found: ,expr : ,s -> ,t)) succeed))
-      ))
-
-  (define (not° x y)
-    (conde
-      ((== x #t) (== y #f))
-      ((== x #f) (== y #t))))
-
-  (define (conj° x y z)
-    (conde
-      ((== x #t) (== y #t) (== z #t))
-      ((== x #t) (== y #f) (== z #f))
-      ((== x #f) (== y #t) (== z #f))
-      ((== x #f) (== y #f) (== z #f))))
-
+  ; Recursion helper for primitive recursion.
+  ; Cammy × Cammy × Val <-> Val
   (define (pr° x f i o)
     (conde
       ((zeroo i) (eval° x 'star o))
@@ -181,8 +97,13 @@
   (define (eval° expr i o)
     (conde
       ((== expr 'id) (== i o))
-      ((fresh (f g u) (== expr `(comp ,f ,g))
-              (eval° f i u) (eval° g u o)))
+      ((fresh (f g) (== expr `(comp ,f ,g))
+              ; NB: Search backwards through compositions.
+              ; Cammy expressions are functional; when inputs are ground,
+              ; outputs will also be ground, so going backwards doesn't hurt.
+              ; Contrariwise, some outputs don't correspond to any input, so
+              ; refutations also need to search backwards.
+              (fresh (u) (eval° g u o) (eval° f i u))))
       ((== expr 'ignore) (== o 'star))
       ((== expr 'fst) (caro i o))
       ((== expr 'snd) (cdro i o))

--- a/movelist/rels.scm
+++ b/movelist/rels.scm
@@ -1,6 +1,7 @@
 ; Extra relations for typical Scheme-flavored miniKanren.
-(module rels (succ° nth° concat°)
+(module rels (concat° succ° nth° not° conj°)
   (import scheme)
+  (import (chicken pretty-print))
   (import (mini-kanren))
 
   ; Flatten an arbitrary number of lists into one list by repeated appending.
@@ -18,7 +19,7 @@
 
   ; The successor function.
   ; Nat <-> Nat
-  (define (succ° n m) (addero 1 '() n m))
+  (define (succ° n m) (+o (build-num 1) n m))
 
   ; The n'th element of a list.
   ; Nat × X <-> [X]
@@ -26,4 +27,20 @@
     (conde
       ((zeroo n) (caro xs x))
       ((fresh (m rest) (succ° m n) (cdro xs rest) (nth° m x rest)))))
+
+  ; Boolean NOT.
+  ; Bool <-> Bool
+  (define (not° x y)
+    (conde
+      ((== x #t) (== y #f))
+      ((== x #f) (== y #t))))
+
+  ; Boolean AND.
+  ; Bool × Bool <-> Bool
+  (define (conj° x y z)
+    (conde
+      ((== x #t) (== y #t) (== z #t))
+      ((== x #t) (== y #f) (== z #f))
+      ((== x #f) (== y #t) (== z #f))
+      ((== x #f) (== y #f) (== z #f))))
 )

--- a/todo.txt
+++ b/todo.txt
@@ -343,16 +343,8 @@
       be applications of non-core templates
 * Sunday
   * Let's do a Pantagruel spec!
-    * But not right now!
-    * Also Janet apps using JPM don't build on NixOS?
-  * Let's rewrite Honey with FastAPI!
-    * And use PyPy!
-    * But not right now!
-* New REPL
-  * Not sure if there's much need for commands
-    * Making new dippers, maybe?
-    * Realized that ":" is not the best command-starter
-      * Technically ")" would be the best choice since it can't start a legal term
+    * Janet apps using JPM don't build on NixOS?
+    * JPM got added to nixpkgs a few months ago, let's try again
 * Let's destroy the Python glue
   * Indeed, let's destroy most of the glue
   * Use CHICKEN Scheme for the basic REPL
@@ -361,7 +353,9 @@
   * Call jelly for optimizing
   * Call RPython binaries for fast rendering
     * Need to provide way to dump CAM bytecode; maybe new executable?
+      * Let's just use an envvar
   * Maybe Honey was a mistake
+    * And now it's gone
 * Slogans?
   * Cammy is compositional
   * Cammy is chimeric