From 186171fec3d87424b0709ce00fadbbf4f6137161 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:07:33 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20pythagorean=20triples=20search=20?= =?UTF-8?q?=E2=80=94=20intarith=20showcase?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Finds all (a, b, c) with a, b, c in [1..10], a <= b, a^2 + b^2 = c^2. Result: ((3 4 5) (6 8 10)) — the two smallest Pythagorean triples within the domain. Demonstrates the enumerate-then-filter pattern: (ino a dom) (ino b dom) (ino c dom) — generate (lteo-i a b) — symmetry break (*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) — squares (pluso-i a-sq b-sq sum) (== sum c-sq) — Pythagorean equation 288/288 cumulative. --- lib/minikanren/tests/pythag.sx | 36 ++++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 5 +++++ 2 files changed, 41 insertions(+) create mode 100644 lib/minikanren/tests/pythag.sx diff --git a/lib/minikanren/tests/pythag.sx b/lib/minikanren/tests/pythag.sx new file mode 100644 index 00000000..c8015ea6 --- /dev/null +++ b/lib/minikanren/tests/pythag.sx @@ -0,0 +1,36 @@ +;; lib/minikanren/tests/pythag.sx — Pythagorean triple search. +;; +;; Uses ino + intarith goals to find triples (a, b, c) with +;; a, b, c ∈ [1..N], a ≤ b, a² + b² = c². With intarith escapes +;; the search runs at host-arithmetic speed. + +(define + digits-1-10 + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + +(mk-test + "pythag-triples-1-to-10" + (let + ((triples (run* q (fresh (a b c a-sq b-sq sum c-sq) (ino a digits-1-10) (ino b digits-1-10) (ino c digits-1-10) (lteo-i a b) (*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) (pluso-i a-sq b-sq sum) (== sum c-sq) (== q (list a b c)))))) + (and + (= (len triples) 2) + (and + (some + (fn (t) (= t (list 3 4 5))) + triples) + (some + (fn (t) (= t (list 6 8 10))) + triples)))) + true) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 8e58641c..50510316 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,11 @@ _(none yet)_ _Newest first._ +- **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 + enumerate-then-filter pattern with intarith escape into host arithmetic. + 1 new test, 288/288 cumulative. - **2026-05-08** — **intarith.sx — fast ground-only integer arithmetic**: pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic via `project`. They are not relational like Peano `pluso` (require args