From 136cacbd3f66cfa46af2bb868074a3046ad1326a Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 11:54:24 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20iterate-no=20=E2=80=94=20apply=20a=20rela?=
 =?UTF-8?q?tion=20n=20times?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

(iterate-no rel n x result) holds when applying the 2-arg relation rel
n times (Peano n) starting from x produces result. Base case: zero
iterations means result equals x. Recursive case: rel x mid, then
iterate-no n-1 from mid.

Generalises common chains:
  succ iteration:  (iterate-no succ-rel n :z q) -> n in Peano
  list growth:     (iterate-no cons-rel n () q) -> n-element list

4 new tests, 426/426 cumulative.
---
 lib/minikanren/relations.sx        |  8 +++++++
 lib/minikanren/tests/iterate-no.sx | 38 ++++++++++++++++++++++++++++++
 plans/minikanren-on-sx.md          |  1 +
 3 files changed, 47 insertions(+)
 create mode 100644 lib/minikanren/tests/iterate-no.sx

diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx
index ca2abf09..1afee3c5 100644
--- a/lib/minikanren/relations.sx
+++ b/lib/minikanren/relations.sx
@@ -182,6 +182,14 @@
       ((nullo l1) (nullo l2))
       ((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (rel a a-prime) (mapo rel d d-prime))))))
 
+(define
+  iterate-no
+  (fn
+    (rel n x result)
+    (conde
+      ((== n :z) (== result x))
+      ((fresh (n-1 mid) (== n (list :s n-1)) (rel x mid) (iterate-no rel n-1 mid result))))))
+
 (define
   everyo
   (fn
diff --git a/lib/minikanren/tests/iterate-no.sx b/lib/minikanren/tests/iterate-no.sx
new file mode 100644
index 00000000..56405e52
--- /dev/null
+++ b/lib/minikanren/tests/iterate-no.sx
@@ -0,0 +1,38 @@
+;; lib/minikanren/tests/iterate-no.sx — iterated relation application.
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+(mk-test
+  "iterate-no-zero"
+  (run*
+    q
+    (iterate-no
+      (fn (a b) (== b (list :wrap a)))
+      (mk-nat 0)
+      :seed q))
+  (list :seed))
+
+(mk-test
+  "iterate-no-three-wraps"
+  (run*
+    q
+    (iterate-no (fn (a b) (== b (list :wrap a))) (mk-nat 3) :x q))
+  (list (list :wrap (list :wrap (list :wrap :x)))))
+
+(mk-test
+  "iterate-no-succ-three-times"
+  (run*
+    q
+    (iterate-no (fn (a b) (== b (list :s a))) (mk-nat 3) :z q))
+  (list (mk-nat 3)))
+
+(mk-test
+  "iterate-no-with-list-cons"
+  (run*
+    q
+    (iterate-no (fn (a b) (conso :a a b)) (mk-nat 4) (list) q))
+  (list (list :a :a :a :a)))
+
+(mk-tests-run!)
diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index 5307dc9c..2307e5c2 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -173,6 +173,7 @@ _(none yet)_
 
 _Newest first._
 
+- **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.
 - **2026-05-08** — **even-i / odd-i (intarith)**: ground-only parity goals via project. Composes with membero for filtered enumeration:  -> . 5 new tests, 416/416 cumulative.
 - **2026-05-08** — **selecto**: classic miniKanren "choose an element + rest". Direct base (l = (x . rest)) plus skip-head recurse. Enumerates all (element, rest) splits in run*; runs forward, backward, mid-pipeline. 6 new tests, 411/411 cumulative.