pub fn structural_columns(ctx: &Context, body: &Term) -> Vec<usize>Expand description
THE ι-SPECIFICATION — which argument makes a Fix unroll.
The ORDERED argument positions of the lexicographic measure this guard admitted for body
(the λ-abstraction under a Fix), with column 0 — the Giménez structural argument — first.
Empty when body has no inductive-typed binder at all, i.e. when the guard would refuse it.
This exists because a REDUCER has to agree with the guard, and the specification of ι for a fixpoint is:
(fix f. λx₀ … λxₙ. e) a₀ … aₙunrolls exactly when the argument at the STRUCTURAL position —structural_columns(ctx, body)[0]— is in constructor form.
Not “when a₀ is”, which is a different rule and a strictly smaller one: the guard reads the
structural column off the body’s own match, so fix f. λm. λn. match n with … — Lean’s
Nat.add, which recurses on its SECOND argument — is admitted with column 0 at position 1. A
reducer that insists on position 0 leaves that definition STUCK for every non-constructor
first argument, so n + 0 = n is not rfl here where it is rfl in Lean, and normalize
hands back a term that still has a δι-redex in it. Not “when SOME argument is”, either: that
unrolls on a non-structural constructor and makes progress the guard never promised.
The two kernels must each implement that rule from this specification — reduction.rs over
named terms, recheck.rs over de Bruijn levels — and NOT by calling one another or by sharing
a reduction routine. What is shared here is only the guard’s own answer to “which column”,
which the guard alone is the authority on: a reducer that guesses it is a reducer that
computes a function the guard did not check.