mk: phase 7 — table-1 + table-3, Ackermann canary
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
Two more arities of the naive memoization wrapper: table-1: predicate (1-arg) tabling. Cache entry is :ok / :no. Demonstrated with a tabled membero-as-predicate. table-3: 3-arg (i1 i2 output) tabling. Cache key joins the two inputs; cache value is the output value list. Canonical demo: tabled Ackermann. (ack-o 0 0 q) -> 1 (ack-o 2 3 q) -> 9 (ack-o 3 3 q) -> 61 A(3,3) executes A(2,..) many times, A(1,..) more, A(0,..) most. With table-3 each (m, n) pair is computed once. 6 new tests, 644/644 cumulative.
This commit is contained in:
@@ -89,3 +89,69 @@
|
||||
(mk-tab-replay-vals vals output s)))))
|
||||
(:else (mk-tab-replay-vals cached output s))))))
|
||||
(:else ((rel-fn input output) s))))))))
|
||||
|
||||
;; --- table-1: 1-arg relation (one input, no output to cache) ---
|
||||
;; The relation is a predicate `(p input)` that succeeds or fails.
|
||||
;; Cache stores either :ok or :no.
|
||||
|
||||
(define
|
||||
table-1
|
||||
(fn
|
||||
(name rel-fn)
|
||||
(fn
|
||||
(input)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((winput (mk-walk* input s)))
|
||||
(cond
|
||||
((mk-tab-ground-term? winput)
|
||||
(let
|
||||
((key (str name "@1@" winput)))
|
||||
(let
|
||||
((cached (mk-tab-lookup key)))
|
||||
(cond
|
||||
((= cached :miss)
|
||||
(let
|
||||
((stream ((rel-fn input) s)))
|
||||
(let
|
||||
((peek (stream-take 1 stream)))
|
||||
(cond
|
||||
((empty? peek)
|
||||
(begin (mk-tab-store! key :no) mzero))
|
||||
(:else (begin (mk-tab-store! key :ok) stream))))))
|
||||
((= cached :ok) (unit s))
|
||||
((= cached :no) mzero)
|
||||
(:else mzero)))))
|
||||
(:else ((rel-fn input) s))))))))
|
||||
|
||||
;; --- table-3: 3-arg relation (input1 input2 output) ---
|
||||
;; Cache keyed by (input1, input2). Output values cached as a list.
|
||||
|
||||
(define
|
||||
table-3
|
||||
(fn
|
||||
(name rel-fn)
|
||||
(fn
|
||||
(i1 i2 output)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((wi1 (mk-walk* i1 s)) (wi2 (mk-walk* i2 s)))
|
||||
(cond
|
||||
((and (mk-tab-ground-term? wi1) (mk-tab-ground-term? wi2))
|
||||
(let
|
||||
((key (str name "@3@" wi1 "/" wi2)))
|
||||
(let
|
||||
((cached (mk-tab-lookup key)))
|
||||
(cond
|
||||
((= cached :miss)
|
||||
(let
|
||||
((all-substs (stream-take -1 ((rel-fn i1 i2 output) s))))
|
||||
(let
|
||||
((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
|
||||
(begin
|
||||
(mk-tab-store! key vals)
|
||||
(mk-tab-replay-vals vals output s)))))
|
||||
(:else (mk-tab-replay-vals cached output s))))))
|
||||
(:else ((rel-fn i1 i2 output) s))))))))
|
||||
|
||||
55
lib/minikanren/tests/tabling-more.sx
Normal file
55
lib/minikanren/tests/tabling-more.sx
Normal file
@@ -0,0 +1,55 @@
|
||||
;; lib/minikanren/tests/tabling-more.sx — table-1 + table-3.
|
||||
|
||||
;; --- table-1 (predicate caching) ---
|
||||
|
||||
(define
|
||||
tab-in-list
|
||||
(table-1
|
||||
"in-list"
|
||||
(fn
|
||||
(x)
|
||||
(membero
|
||||
x
|
||||
(list 1 2 3 4 5)))))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"table-1-hit"
|
||||
(run* q (tab-in-list 3))
|
||||
(list (make-symbol "_.0")))
|
||||
(mk-test "table-1-miss-no" (run* q (tab-in-list 99)) (list))
|
||||
(mk-test
|
||||
"table-1-replay"
|
||||
(run* q (tab-in-list 3))
|
||||
(list (make-symbol "_.0")))
|
||||
|
||||
;; --- table-3 (Ackermann) ---
|
||||
|
||||
(define
|
||||
ack-o
|
||||
(table-3
|
||||
"ack"
|
||||
(fn
|
||||
(m n result)
|
||||
(conde
|
||||
((== m 0) (pluso-i n 1 result))
|
||||
((fresh (m-1) (lto-i 0 m) (== n 0) (minuso-i m 1 m-1) (ack-o m-1 1 result)))
|
||||
((fresh (m-1 n-1 inner) (lto-i 0 m) (lto-i 0 n) (minuso-i m 1 m-1) (minuso-i n 1 n-1) (ack-o m n-1 inner) (ack-o m-1 inner result)))))))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"ack-0-0"
|
||||
(run* q (ack-o 0 0 q))
|
||||
(list 1))
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"ack-2-3"
|
||||
(run* q (ack-o 2 3 q))
|
||||
(list 9))
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"ack-3-3"
|
||||
(run* q (ack-o 3 3 q))
|
||||
(list 61))
|
||||
|
||||
(mk-tests-run!)
|
||||
Reference in New Issue
Block a user