Expand description
Termination checking for fixpoints.
This module implements the syntactic guard condition that ensures
all recursive functions terminate. Without this check, the type system
would be unsound - we could “prove” False by writing fix f. f.
The algorithm (following Coq):
- Identify the “structural parameter” - the first inductive-typed argument
- Track variables that are “structurally smaller” than the structural parameter
- Verify all recursive calls use a smaller argument
A variable k is smaller than n if it was bound by matching on n:
match n with Succ k => ... means k < n structurally.
Functions§
- check_
termination - Check that a Fix term satisfies the syntactic guard condition.