This module contains the termination checker for the intermediate language. The goal is to to find one argument for every recursive function whose size is reduced in every recursive call. If such arguments exist we know that the function will terminate and can be translated to Coq. The termination checker defined in this module is very limited compared to Coq's termination checker. Even if we don't recognize the decreasing arguments, Coq might still be able to tell that the function is decreasing on one of its arguments. However, we cannot rely on Coq's termination entirely, since we need to know the decreasing arguments for the transformation of recursive functions into a recursive helper function and a non-recursive main function (see also FreeC.Backend.Coq.Converter.FuncDecl.Rec.WithHelpers)

Guessing Decreasing Arguments

Given set of mutually recursive function declarations F, the termination checker tries to find a combination of arguments such that each function in the set decreases on the corresponding argument. Since we have to know the decreasing argument of all functions in the set in order to test whether a function decreases on one of its argument, we first enumerate (or guess) all possible combinations and then check whether the combination of decreasing arguments is valid.

Checking Decreasing Arguments

A function f ∈ F declared by

f x₁ … xᵢ … xₙ = e

decreases on its i-th argument if for every recursive call to functions g ∈ F on the right-hand side e of f

g e₁ … eⱼ … eₘ

where j is the decreasing argument guessed for g the expression eⱼ is recognized as structurally smaller than xᵢ.

Checking for Structurally Smaller Expressions

To test whether an expression is structurally smaller than the decreasing argument, we assign every expression a depth within the structure of the decreasing argument as described below. There is a special depth value ⊥ with the property ⊥ + 1 = ⊥ that is assigned to expressions that are not known to be subterms of the decreasing argument.

1. The decreasing argument itself is at depth 0.
2. The variables x₁, …, xₙ that are bound by an alternative case e of { … ; C x₁ … xₙ -> e' ; … } of a case-expression whose scrutinee e is at depth d are at depth d + 1 within the right- hand side e of the alternative.
3. The variables x₁, …, xₙ that are bound by a let-binding let { x₁ = e₁ ; … ; xₙ = eₙ } in e whose right-hand sides e₁, …, eₙ are at depths d₁, …, dₙ are at the same depths within the in- expression e as well as in the right-hand sides e₁, …, eₙ.
4. All other variables and non-variable expressions are at depth ⊥.

An expression is structurally smaller than the decreasing argument if its depth is greater than the depth of the decreasing argument, i.e., >0. The definition above ensures that

• variables that are introduced by case-expression alternatives are structurally smaller than the scrutinee of the case-expression and
• variables that are introduced by let-bindings are structually equal to their right-hand side.

Bypassing the Termination Checker

Coq's termination checker uses the same idea as described above but is much more sophisticated. If the user knows that their function declaration is decreasing on one of its arguments, they can annotate the decreasing argument using a custom pragma (see also DecArgPragma). If there is such an annotation guessDecArgs will not consider any other argument for the annotated function declaration and checkDecArgs always accepts the guessed argument as a decreasing argument.