mk: phase 7 — naive ground-arg tabling, Fibonacci canary green
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 58s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 58s
`table-2` wraps a 2-arg (input, output) relation. On a ground input walk, looks up the (string-encoded) cache key; on miss, runs the relation, drains the answer stream, extracts walk*-output values from each subst, stores them, and replays. On hit, replays the cached values directly — no recomputation. Cache lifetime: a single global mk-tab-cache (mutated via set!). mk-tab-clear! resets between independent queries. Canonical demo: tabled fib(25) = 75025 in ~5 seconds; the same naive fib-o times out at 60s. Memoization collapses the exponential redundant recomputation in the binary recursion. Limitations (deferred to future SLG work): cyclic recursive calls with the same ground key still diverge — naive memoization populates the cache only AFTER computation completes, so a recursive call inside its own computation can't see the in-progress entry. The brief's "tabled patho on cyclic graphs" use case requires producer/consumer scheduling and is left for a future iteration. 12 new tests, fib(0..20) + ground-term predicate + cache-replay verification. 638/638 cumulative.
This commit is contained in:
91
lib/minikanren/tabling.sx
Normal file
91
lib/minikanren/tabling.sx
Normal file
@@ -0,0 +1,91 @@
|
||||
;; lib/minikanren/tabling.sx — Phase 7 piece A: naive memoization.
|
||||
;;
|
||||
;; A `table-2` wrapper for 2-arg relations (input, output). Caches by
|
||||
;; ground input (walked at call time). On hit, replays the cached output
|
||||
;; values; on miss, runs the relation, collects all output values from
|
||||
;; the answer stream, stores, then replays.
|
||||
;;
|
||||
;; Limitations of naive memoization (vs proper SLG / producer-consumer
|
||||
;; tabling):
|
||||
;; - Each call must terminate before its result enters the cache —
|
||||
;; so cyclic recursive calls with the SAME ground input would still
|
||||
;; diverge (not addressed here).
|
||||
;; - Caching by full ground walk only; partially-ground args fall
|
||||
;; through to the underlying relation.
|
||||
;;
|
||||
;; Despite the limitations, naive memoization is enough for the
|
||||
;; canonical demo: Fibonacci goes from exponential to linear because
|
||||
;; each fib(k) result is computed at most once.
|
||||
;;
|
||||
;; Cache lifetime: a single global mk-tab-cache. Use `(mk-tab-clear!)`
|
||||
;; between independent queries.
|
||||
|
||||
(define mk-tab-cache {})
|
||||
|
||||
(define mk-tab-clear! (fn () (set! mk-tab-cache {})))
|
||||
|
||||
(define
|
||||
mk-tab-lookup
|
||||
(fn
|
||||
(key)
|
||||
(cond
|
||||
((has-key? mk-tab-cache key) (get mk-tab-cache key))
|
||||
(:else :miss))))
|
||||
|
||||
(define
|
||||
mk-tab-store!
|
||||
(fn (key vals) (set! mk-tab-cache (assoc mk-tab-cache key vals))))
|
||||
|
||||
(define
|
||||
mk-tab-ground-term?
|
||||
(fn
|
||||
(t)
|
||||
(cond
|
||||
((is-var? t) false)
|
||||
((mk-cons-cell? t)
|
||||
(and
|
||||
(mk-tab-ground-term? (mk-cons-head t))
|
||||
(mk-tab-ground-term? (mk-cons-tail t))))
|
||||
((mk-list-pair? t) (every? mk-tab-ground-term? t))
|
||||
(:else true))))
|
||||
|
||||
(define
|
||||
mk-tab-replay-vals
|
||||
(fn
|
||||
(vals output s)
|
||||
(cond
|
||||
((empty? vals) mzero)
|
||||
(:else
|
||||
(let
|
||||
((sp (mk-unify output (first vals) s)))
|
||||
(let
|
||||
((this-stream (cond ((= sp nil) mzero) (:else (unit sp)))))
|
||||
(mk-mplus this-stream (mk-tab-replay-vals (rest vals) output s))))))))
|
||||
|
||||
(define
|
||||
table-2
|
||||
(fn
|
||||
(name rel-fn)
|
||||
(fn
|
||||
(input output)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((winput (mk-walk* input s)))
|
||||
(cond
|
||||
((mk-tab-ground-term? winput)
|
||||
(let
|
||||
((key (str name "@" winput)))
|
||||
(let
|
||||
((cached (mk-tab-lookup key)))
|
||||
(cond
|
||||
((= cached :miss)
|
||||
(let
|
||||
((all-substs (stream-take -1 ((rel-fn input 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 input output) s))))))))
|
||||
60
lib/minikanren/tests/tabling.sx
Normal file
60
lib/minikanren/tests/tabling.sx
Normal file
@@ -0,0 +1,60 @@
|
||||
;; lib/minikanren/tests/tabling.sx — Phase 7 piece A: naive memoization.
|
||||
|
||||
;; --- Fibonacci canary: tabled vs naive --
|
||||
|
||||
(define
|
||||
tab-fib-o
|
||||
(table-2
|
||||
"fib"
|
||||
(fn
|
||||
(n result)
|
||||
(conde
|
||||
((== n 0) (== result 0))
|
||||
((== n 1) (== result 1))
|
||||
((fresh (n-1 n-2 r-1 r-2) (lto-i 1 n) (minuso-i n 1 n-1) (minuso-i n 2 n-2) (tab-fib-o n-1 r-1) (tab-fib-o n-2 r-2) (pluso-i r-1 r-2 result)))))))
|
||||
|
||||
(mk-tab-clear!)
|
||||
|
||||
(mk-test "tab-fib-zero" (run* q (tab-fib-o 0 q)) (list 0))
|
||||
(mk-tab-clear!)
|
||||
(mk-test "tab-fib-one" (run* q (tab-fib-o 1 q)) (list 1))
|
||||
(mk-tab-clear!)
|
||||
(mk-test "tab-fib-two" (run* q (tab-fib-o 2 q)) (list 1))
|
||||
(mk-tab-clear!)
|
||||
(mk-test "tab-fib-five" (run* q (tab-fib-o 5 q)) (list 5))
|
||||
(mk-tab-clear!)
|
||||
(mk-test "tab-fib-ten" (run* q (tab-fib-o 10 q)) (list 55))
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"tab-fib-twenty"
|
||||
(run* q (tab-fib-o 20 q))
|
||||
(list 6765))
|
||||
|
||||
;; --- ground-term predicate ---
|
||||
|
||||
(mk-test "tab-ground-term-num" (mk-tab-ground-term? 5) true)
|
||||
(mk-test "tab-ground-term-str" (mk-tab-ground-term? "hi") true)
|
||||
(mk-test
|
||||
"tab-ground-term-list"
|
||||
(mk-tab-ground-term? (list 1 2 3))
|
||||
true)
|
||||
(mk-test "tab-ground-term-var" (mk-tab-ground-term? (mk-var "x")) false)
|
||||
(mk-test
|
||||
"tab-ground-term-nested"
|
||||
(mk-tab-ground-term?
|
||||
(list 1 (list 2 (mk-var "y")) 3))
|
||||
false)
|
||||
|
||||
;; --- caching reduces work — count cache hits via repeated query ---
|
||||
|
||||
(mk-test
|
||||
"tab-cache-replay"
|
||||
(begin
|
||||
(mk-tab-clear!)
|
||||
(let
|
||||
((first (run* q (tab-fib-o 10 q)))
|
||||
(second (run* q (tab-fib-o 10 q))))
|
||||
(and (= first (list 55)) (= second (list 55)))))
|
||||
true)
|
||||
|
||||
(mk-tests-run!)
|
||||
@@ -180,10 +180,19 @@ Key semantic mappings:
|
||||
- [ ] Tests: send-more-money, N-queens with CLP(FD), map coloring, cryptarithmetic
|
||||
|
||||
### Phase 7 — tabling (memoization of relations)
|
||||
- [ ] `tabled` annotation: memoize calls to a relation using a hash table
|
||||
- [ ] Prevents infinite loops in recursive relations like `patho` on cyclic graphs
|
||||
- [ ] Producer/consumer scheduling for tabled relations (variant of SLG resolution)
|
||||
- [ ] Tests: cyclic graph reachability, mutual recursion, Fibonacci via tabling
|
||||
- [x] `table-2` wrapper: ground-arg memoization for 2-arg relations.
|
||||
Cache keyed by walked input; on miss runs underlying relation,
|
||||
collects all output values from the answer stream, stores, and
|
||||
replays. Subsequent calls with the same ground input replay the
|
||||
cached values (no recomputation).
|
||||
- [x] Fibonacci canary green: tabled `fib(25) = 75025` in seconds;
|
||||
naive `fib(25)` times out at 60s. Memoization turns exponential
|
||||
recursion into linear.
|
||||
- [ ] Producer/consumer SLG scheduling — required to handle recursive
|
||||
tabled calls with the SAME ground key (e.g. cyclic `patho` with a
|
||||
shared key); naive memoization deferred to a future iteration.
|
||||
- [ ] Tests: cyclic graph reachability via tabled patho (deferred —
|
||||
requires SLG); mutual recursion (deferred).
|
||||
|
||||
## Blockers
|
||||
|
||||
|
||||
Reference in New Issue
Block a user