From 54a58c704eebec24c4e1e745d4a27733ca2c5905 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:30:02 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20eveno=20+=20oddo=20=E2=80=94=20Peano=20pa?= =?UTF-8?q?rity=20predicates?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit eveno: zero, or (s (s m)) when m is even. oddo: one, or (s (s m)) when m is odd. Both run forward (predicate test on a Peano number) and backward (enumerate even / odd numbers). The two are mutually exclusive — no number satisfies both. 12 new tests, 359/359 cumulative. --- lib/minikanren/peano.sx | 16 ++++++++++ lib/minikanren/tests/parity.sx | 58 ++++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 4 +++ 3 files changed, 78 insertions(+) create mode 100644 lib/minikanren/tests/parity.sx 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 ...) ...)))`.