diff --git a/lib/minikanren/intarith.sx b/lib/minikanren/intarith.sx index 108caf86..f5351ece 100644 --- a/lib/minikanren/intarith.sx +++ b/lib/minikanren/intarith.sx @@ -77,3 +77,19 @@ ((nullo l)) ((fresh (a) (== l (list a)))) ((fresh (a b rest mid) (conso a mid l) (conso b rest mid) (lteo-i a b) (sortedo mid)))))) + +(define + mino + (fn + (l m) + (conde + ((fresh (a) (== l (list a)) (== m a))) + ((fresh (a d rest-min) (conso a d l) (mino d rest-min) (conde ((lteo-i a rest-min) (== m a)) ((lto-i rest-min a) (== m rest-min)))))))) + +(define + maxo + (fn + (l m) + (conde + ((fresh (a) (== l (list a)) (== m a))) + ((fresh (a d rest-max) (conso a d l) (maxo d rest-max) (conde ((lteo-i rest-max a) (== m a)) ((lto-i a rest-max) (== m rest-max)))))))) diff --git a/lib/minikanren/tests/minmax.sx b/lib/minikanren/tests/minmax.sx new file mode 100644 index 00000000..76ea3dd5 --- /dev/null +++ b/lib/minikanren/tests/minmax.sx @@ -0,0 +1,49 @@ +;; lib/minikanren/tests/minmax.sx — mino + maxo via intarith. + +(mk-test + "mino-singleton" + (run* q (mino (list 7) q)) + (list 7)) +(mk-test + "mino-of-3" + (run* q (mino (list 5 1 3) q)) + (list 1)) +(mk-test + "mino-of-5" + (run* + q + (mino (list 5 1 3 2 4) q)) + (list 1)) +(mk-test + "mino-with-dups" + (run* q (mino (list 3 3 3) q)) + (list 3)) +(mk-test "mino-empty-fails" (run* q (mino (list) q)) (list)) + +(mk-test + "maxo-singleton" + (run* q (maxo (list 7) q)) + (list 7)) +(mk-test + "maxo-of-5" + (run* + q + (maxo (list 5 1 3 2 4) q)) + (list 5)) +(mk-test + "maxo-of-negs" + (run* q (maxo (list -5 -1 -3) q)) + (list -1)) + +(mk-test + "min-and-max-of-list" + (run* + q + (fresh + (mn mx) + (mino (list 5 1 3 2 4) mn) + (maxo (list 5 1 3 2 4) mx) + (== q (list mn mx)))) + (list (list 1 5))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 3a05e6c6..6f0c9ca4 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,7 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **mino + maxo (intarith)**: find the minimum/maximum of a non-empty list of ground integers. Two conde clauses each: singleton (return the element) / multi (compare head against recursive min/max of tail). 9 new tests, 472/472 cumulative. - **2026-05-08** — **sortedo (intarith)**: list is non-decreasing under integer ordering. Three conde clauses: empty / singleton / pair-and-recurse. Uses lteo-i for the adjacent-pair check (ground integers). 7 new tests, 463/463 cumulative. - **2026-05-08** — **subseto**: every element of l1 is a member of l2. Recurses on l1, checking each element via membero. Allows duplicates in l1 (each independently in l2). 7 new tests, 456/456 cumulative. - **2026-05-08** — **cycle-free path search**: mitigation for the cyclic-graph divergence — thread a accumulator through the recursion, gate each step with nafc + membero on visited. Terminates on graphs with cycles; no Phase-7 tabling required for the simple case. 3 new tests, 449/449 cumulative.