From eb69039935c91eda42ed2c94645985a0a4011089 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:59:41 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20swap-firsto=20=E2=80=94=20swap=20first=20?= =?UTF-8?q?two=20list=20elements?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four conso calls express the (a b . rest) -> (b a . rest) rewrite as a purely relational constraint. Self-inverse on length-2+ lists; runs forward (swap given input) and backward (recover original from the swapped form). Fails on lists shorter than 2. 6 new tests, 437/437 cumulative. --- lib/minikanren/relations.sx | 11 ++++++++++ lib/minikanren/tests/swap-firsto.sx | 32 +++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 1 + 3 files changed, 44 insertions(+) create mode 100644 lib/minikanren/tests/swap-firsto.sx diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index ce49586c..73bfd532 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -198,6 +198,17 @@ ((nullo l1) (nullo l2) (nullo pairs)) ((fresh (a1 d1 a2 d2 d-pairs) (conso a1 d1 l1) (conso a2 d2 l2) (conso (list a1 a2) d-pairs pairs) (pairlisto d1 d2 d-pairs)))))) +(define + swap-firsto + (fn + (l result) + (fresh + (a b rest mid-l mid-r) + (conso a mid-l l) + (conso b rest mid-l) + (conso b mid-r result) + (conso a rest mid-r)))) + (define everyo (fn diff --git a/lib/minikanren/tests/swap-firsto.sx b/lib/minikanren/tests/swap-firsto.sx new file mode 100644 index 00000000..773a57c2 --- /dev/null +++ b/lib/minikanren/tests/swap-firsto.sx @@ -0,0 +1,32 @@ +;; lib/minikanren/tests/swap-firsto.sx — swap first two elements. + +(mk-test + "swap-firsto-pair" + (run* q (swap-firsto (list 1 2) q)) + (list (list 2 1))) + +(mk-test + "swap-firsto-with-tail" + (run* q (swap-firsto (list 1 2 3 4) q)) + (list (list 2 1 3 4))) + +(mk-test + "swap-firsto-singleton-fails" + (run* q (swap-firsto (list 1) q)) + (list)) + +(mk-test "swap-firsto-empty-fails" (run* q (swap-firsto (list) q)) (list)) + +(mk-test + "swap-firsto-self-inverse" + (run* + q + (fresh (mid) (swap-firsto (list :a :b :c :d) mid) (swap-firsto mid q))) + (list (list :a :b :c :d))) + +(mk-test + "swap-firsto-backward" + (run* q (swap-firsto q (list :y :x :z))) + (list (list :x :y :z))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 9b096dd9..f77aa993 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **swap-firsto**: swap the first two elements of a list. Built via four conso constraints. Self-inverse on length-2+ lists; runs forward and backward. 6 new tests, 437/437 cumulative. - **2026-05-08** — **pairlisto**: relational zip — pairs is the zipped list of (l1[i] l2[i]). Runs forward, recovers l1 given l2 and pairs, recovers l2 given l1 and pairs. 5 new tests, 431/431 cumulative. - **2026-05-08** — **iterate-no**: relational iterated application. Applies a 2-arg relation n times (Peano n) starting from x to produce result. Generalises succ-iteration / list-cons-iteration / etc. 4 new tests, 426/426 cumulative. - **2026-05-08** — **rev-acco / rev-2o**: accumulator-style reversal — faster than appendo-driven reverseo for forward queries because no quadratic appendos. Trade-off: rev-acco is asymmetric (cannot run cleanly backward in run*). 6 new tests, 422/422 cumulative.