From cfb43a3cdfd0193e8807f17971527ef326ccfebf Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:09:48 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20samelengtho=20=E2=80=94=20equal-length=20?= =?UTF-8?q?relation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Recurses positionally, dropping a head from each list each step. Both arguments can be unbound, giving the natural enumeration: (run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2)))) -> (((), ()) empty/empty ((_.0), (_.1)) pair of 1-element lists ((_.0 _.1), (_.2 _.3))) pair of 2-element lists 5 new tests, 293/293 cumulative. --- lib/minikanren/relations.sx | 8 ++++++ lib/minikanren/tests/list-relations.sx | 39 +++++++++++++++++++++++++- plans/minikanren-on-sx.md | 5 ++++ 3 files changed, 51 insertions(+), 1 deletion(-) diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index 1fcddd6d..200c3128 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -124,3 +124,11 @@ (conde ((== n :z) (fresh (d) (conso elem d l))) ((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (nth-o n-1 d elem)))))) + +(define + samelengtho + (fn + (l1 l2) + (conde + ((nullo l1) (nullo l2)) + ((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (samelengtho d d-prime)))))) diff --git a/lib/minikanren/tests/list-relations.sx b/lib/minikanren/tests/list-relations.sx index 9c36ff8e..0a9582d3 100644 --- a/lib/minikanren/tests/list-relations.sx +++ b/lib/minikanren/tests/list-relations.sx @@ -1,4 +1,4 @@ -;; lib/minikanren/tests/list-relations.sx — rembero, assoco, nth-o. +;; lib/minikanren/tests/list-relations.sx — rembero, assoco, nth-o, samelengtho. ;; --- rembero (remove first occurrence) --- @@ -86,4 +86,41 @@ q)) (list)) +;; --- samelengtho --- + +(mk-test + "samelengtho-equal" + (run* + q + (samelengtho (list 1 2 3) (list :a :b :c))) + (list (make-symbol "_.0"))) + +(mk-test + "samelengtho-different-fails" + (run* q (samelengtho (list 1 2) (list :a :b :c))) + (list)) + +(mk-test + "samelengtho-empty-equal" + (run* q (samelengtho (list) (list))) + (list (make-symbol "_.0"))) + +(mk-test + "samelengtho-builds-vars" + (run 1 q (samelengtho (list 1 2 3) q)) + (list (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2")))) + +(mk-test + "samelengtho-enumerates-pairs" + (run + 3 + q + (fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2)))) + (list + (list (list) (list)) + (list (list (make-symbol "_.0")) (list (make-symbol "_.1"))) + (list + (list (make-symbol "_.0") (make-symbol "_.1")) + (list (make-symbol "_.2") (make-symbol "_.3"))))) + (mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 50510316..c1d668a2 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,11 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **samelengtho**: classic miniKanren relation that + succeeds when two lists have equal length. Symmetric — works to enumerate + both lists fresh: `(run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q + (list l1 l2))))` produces empty/empty, then 1-elem pairs, then 2-elem. + 5 new tests, 293/293 cumulative. - **2026-05-08** — **Pythagorean triples (intarith showcase)**: search for (a, b, c) ∈ [1..10]³, a ≤ b, a² + b² = c² via `ino + lteo-i + *o-i + pluso-i + ==`. Finds exactly `(3 4 5)` and `(6 8 10)`. Demonstrates the