From f4ab7f2534336445b8bf07f089c9f09e16dea4c3 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Thu, 7 May 2026 21:49:38 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20phase=204B=20=E2=80=94=20reverseo=20+=20l?=
 =?UTF-8?q?engtho,=2010=20new=20tests?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

reverseo: standard recursive definition via appendo. Forward works in
run*; backward (input fresh, output ground) works in run 1 but run*
diverges trying to enumerate the unique answer (canonical TRS issue
with naive reverseo).

lengtho: Peano encoding (:z / (:s :z) / (:s (:s :z)) ...) so it works
relationally in both directions without arithmetic-as-relation. Forward
returns the Peano length; backward enumerates lists of a given length.

162/162 cumulative.
---
 lib/minikanren/relations.sx       | 16 ++++++++++
 lib/minikanren/tests/relations.sx | 52 +++++++++++++++++++++++++++++++
 plans/minikanren-on-sx.md         | 15 ++++++---
 3 files changed, 79 insertions(+), 4 deletions(-)

diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx
index b9f38732..10f5a289 100644
--- a/lib/minikanren/relations.sx
+++ b/lib/minikanren/relations.sx
@@ -49,3 +49,19 @@
     (conde
       ((fresh (d) (conso x d l)))
       ((fresh (a d) (conso a d l) (membero x d))))))
+
+(define
+  reverseo
+  (fn
+    (l r)
+    (conde
+      ((nullo l) (nullo r))
+      ((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r))))))
+
+(define
+  lengtho
+  (fn
+    (l n)
+    (conde
+      ((nullo l) (== n :z))
+      ((fresh (a d n-1) (conso a d l) (== n (list :s n-1)) (lengtho d n-1))))))
diff --git a/lib/minikanren/tests/relations.sx b/lib/minikanren/tests/relations.sx
index ae3475c9..40cc5fc8 100644
--- a/lib/minikanren/tests/relations.sx
+++ b/lib/minikanren/tests/relations.sx
@@ -172,4 +172,56 @@
   (run* q (membero q (list "a" "b" "c")))
   (list "a" "b" "c"))
 
+;; --- reverseo ---
+
+(mk-test
+  "reverseo-forward"
+  (run* q (reverseo (list 1 2 3) q))
+  (list (list 3 2 1)))
+
+(mk-test "reverseo-empty" (run* q (reverseo (list) q)) (list (list)))
+
+(mk-test
+  "reverseo-singleton"
+  (run* q (reverseo (list 42) q))
+  (list (list 42)))
+
+(mk-test
+  "reverseo-five"
+  (run*
+    q
+    (reverseo (list 1 2 3 4 5) q))
+  (list (list 5 4 3 2 1)))
+
+(mk-test
+  "reverseo-backward-one"
+  (run 1 q (reverseo q (list 1 2 3)))
+  (list (list 3 2 1)))
+
+(mk-test
+  "reverseo-round-trip"
+  (run*
+    q
+    (fresh (mid) (reverseo (list "a" "b" "c") mid) (reverseo mid q)))
+  (list (list "a" "b" "c")))
+
+;; --- lengtho (Peano-style) ---
+
+(mk-test "lengtho-empty-is-z" (run* q (lengtho (list) q)) (list :z))
+
+(mk-test
+  "lengtho-of-3"
+  (run* q (lengtho (list "a" "b" "c") q))
+  (list (list :s (list :s (list :s :z)))))
+
+(mk-test
+  "lengtho-empty-from-zero"
+  (run 1 q (lengtho q :z))
+  (list (list)))
+
+(mk-test
+  "lengtho-enumerates-of-length-2"
+  (run 1 q (lengtho q (list :s (list :s :z))))
+  (list (list (make-symbol "_.0") (make-symbol "_.1"))))
+
 (mk-tests-run!)
diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index ff9b67e0..f60651fc 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -109,10 +109,13 @@ Key semantic mappings:
 - [x] `nullo` `l` — l is empty
 - [x] `pairo` `p` — p is a (non-empty) cons-cell / list
 - [x] `caro` / `cdro` / `conso` / `firsto` / `resto`
-- [ ] `reverseo` `l` `r` — reverse of list
-- [ ] `flatteno` `l` `f` — flatten nested lists
-- [ ] `permuteo` `l` `p` — permutation of list
-- [ ] `lengtho` `l` `n` — length as a relation (Peano or integer)
+- [x] `reverseo` `l` `r` — reverse of list. Forward is fast; backward is `run 1`-clean,
+      `run*` diverges due to interleaved unbounded list search (canonical TRS issue).
+- [ ] `flatteno` `l` `f` — flatten nested lists (deferred — needs atom predicate)
+- [ ] `permuteo` `l` `p` — permutation of list (deferred to Phase 5 with `matche`)
+- [x] `lengtho` `l` `n` — length as a relation, Peano-encoded:
+      `:z` / `(:s :z)` / `(:s (:s :z))` ... matches TRS. Forward is direct;
+      backward enumerates lists of a given length.
 - [x] Tests: run each relation forwards and backwards (so far 25 in
       `tests/relations.sx`; reverseo/flatteno/permuteo/lengtho deferred)
 
@@ -152,6 +155,10 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-07** — **Phase 4 piece B — reverseo + lengtho**: reverseo runs forward
+  cleanly and `run 1`-cleanly backward; lengtho uses Peano-encoded lengths so it
+  works as a true relation in both directions (tests use the encoding directly).
+  10 new tests, 162/162 cumulative.
 - **2026-05-07** — **Phase 4 piece A — appendo canary green**: cons-cell support
   in `unify.sx` + `(:s head tail)` lazy stream refactor in `stream.sx` + hygienic
   `Zzz` (gensym'd subst-name) wrapping each `conde` clause + `lib/minikanren/