diff --git a/lib/minikanren/peano.sx b/lib/minikanren/peano.sx index 9865cf72..cdbec76e 100644 --- a/lib/minikanren/peano.sx +++ b/lib/minikanren/peano.sx @@ -26,6 +26,22 @@ (define lto (fn (a b) (fresh (sa) (succ-of a sa) (lteo sa b)))) +(define + eveno + (fn + (n) + (conde + ((== n :z)) + ((fresh (m) (== n (list :s (list :s m))) (eveno m)))))) + +(define + oddo + (fn + (n) + (conde + ((== n (list :s :z))) + ((fresh (m) (== n (list :s (list :s m))) (oddo m)))))) + (define *o (fn diff --git a/lib/minikanren/tests/parity.sx b/lib/minikanren/tests/parity.sx new file mode 100644 index 00000000..fc445558 --- /dev/null +++ b/lib/minikanren/tests/parity.sx @@ -0,0 +1,58 @@ +;; lib/minikanren/tests/parity.sx — eveno + oddo Peano predicates. + +(define + mk-nat + (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1)))))) + +(mk-test "eveno-zero" (run* q (eveno :z)) (list (make-symbol "_.0"))) +(mk-test + "eveno-2" + (run* q (eveno (mk-nat 2))) + (list (make-symbol "_.0"))) +(mk-test + "eveno-4" + (run* q (eveno (mk-nat 4))) + (list (make-symbol "_.0"))) +(mk-test "eveno-1-fails" (run* q (eveno (mk-nat 1))) (list)) +(mk-test "eveno-3-fails" (run* q (eveno (mk-nat 3))) (list)) + +(mk-test + "oddo-1" + (run* q (oddo (mk-nat 1))) + (list (make-symbol "_.0"))) +(mk-test + "oddo-3" + (run* q (oddo (mk-nat 3))) + (list (make-symbol "_.0"))) +(mk-test "oddo-zero-fails" (run* q (oddo :z)) (list)) +(mk-test "oddo-2-fails" (run* q (oddo (mk-nat 2))) (list)) + +;; Enumerate small evens. +(mk-test + "eveno-enumerates" + (run 4 q (eveno q)) + (list + (mk-nat 0) + (mk-nat 2) + (mk-nat 4) + (mk-nat 6))) + +;; Enumerate small odds. +(mk-test + "oddo-enumerates" + (run 4 q (oddo q)) + (list + (mk-nat 1) + (mk-nat 3) + (mk-nat 5) + (mk-nat 7))) + +;; A number is even XOR odd (no overlap). +(mk-test + "even-odd-no-overlap" + (run* + q + (mk-conj (eveno (mk-nat 4)) (oddo (mk-nat 4)))) + (list)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 56caa71c..9834c5c4 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,10 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **eveno / oddo Peano predicates**: classic miniKanren parity + relations. eveno: 0 or successor-of-successor of even; oddo: 1 or + successor-of-successor of odd. Both run forward (test) and backward + (enumerate). 12 new tests, 359/359 cumulative. - **2026-05-08** — **defrel — Prolog-style relation definition macro**: `(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...)` expands to `(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...)))`.