mk: iterate-no — apply a relation n times
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
(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.
This commit is contained in:
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user