mk: phase 4B — reverseo + lengtho, 10 new tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s

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.
This commit is contained in:
2026-05-07 21:49:38 +00:00
parent cae87c1e2c
commit f4ab7f2534
3 changed files with 79 additions and 4 deletions

View File

@@ -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))))))