mutual recursion admitted under lexicographic measures

1 files changed, 9 insertions, 6 deletions

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