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 --- lib/world.mli | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'lib/world.mli') diff --git a/lib/world.mli b/lib/world.mli index 51ee078..14f82d3 100644 --- a/lib/world.mli +++ b/lib/world.mli @@ -29,11 +29,13 @@ type rule = { rule_name : string; head : Pattern.t Label.Map.t; body : expr; - witness : Label.t option; - (** For a recursive rule, the label whose argument strictly - decreases. The VM requires it ground before unfolding, - which is what turns the admission proof into runtime - termination. [None] on non-recursive rules. *) + witness : Label.t list; + (** For a recursive rule, the lexicographic measure of its + call-graph component: at some position the recursive + argument strictly decreases, all earlier positions staying + equal. The VM requires every position ground before + unfolding, which is what turns the admission proof into + runtime termination. Empty on non-recursive rules. *) } (** The primitive host-checked domains. *) -- cgit v1.2.3