From 726f3dfb116ec9265041e642000612831633fe3c Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 23:39:40 -0300 Subject: mutual recursion admitted under lexicographic measures --- docs/vm.org | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'docs/vm.org') diff --git a/docs/vm.org b/docs/vm.org index 8d1215a..87c0ca0 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -36,12 +36,15 @@ A program only becomes a world if everything in it is admitted: attribute domain. This is integrity control at load time, the same membership check it always is. A Natural is an Integer and an Integer is a Rational, literally. -- a recursive rule must exhibit a structurally decreasing argument: - some label whose call argument sits strictly inside the head - argument, like =T= inside =#(H | T)=. The label is kept as the - rule's witness. No witness, no world. -- mutual recursion between relations is rejected for now. Self - recursion with a witness is the admitted form. +- recursion must exhibit a lexicographic structural decrease. + Admission groups rule defined relations into strongly connected + components of the call graph and searches for an ordered list of + labels such that every call inside the component strictly shrinks + at some position, all earlier positions staying equal. Self + recursion is the one label case, like =T= inside =#(H | T)=; + mutual recursion like Even and Odd passing a shrinking list back + and forth is admitted the same way. The measure is stamped on the + recursive rules as their witness. No measure, no world. - every referenced relation must exist, either builtin or declared. This is rung one of the evidence ladder in decision 10. Bounded -- cgit v1.2.3