pub enum Unreduced {
Cyclic,
BudgetSpent,
TooDeep,
}Expand description
Why a reduction stopped before reaching a normal form.
normalize hands back a bare Term, so “this is the normal form” and “this is as far as I
got” are THE SAME ANSWER — and the caller cannot tell them apart. That is not a precision
loss, it is a soundness channel: a conversion check that compares two abandoned reductions
and finds them equal has certified nothing.
A δ-cycle (a := b, b := a) proves no fuel constant can close the gap, because that
reduction has no normal form at all. Only an error channel can.
It is nevertheless CONSERVATIVE rather than unsound, and the reason is worth stating because
it is what a future change can break: reduce_step_opt is a FUNCTION of the term, so two
reductions holding the same term after the same number of steps hold it forever after and
therefore have the same normal form. A conversion check built on “normalise both sides, then
compare” can be INCOMPLETE when a budget runs out — never wrong. The same determinism makes
the cycle answer safe: normalize hands the INPUT back, and the only term that can be
mistaken for is itself. Collapsing every non-normalising term to one answer instead — a
shared Hole, say — would identify two unrelated cycles and let refl prove an equation
between two well-typed terms that are not equal.
Variants§
Cyclic
The reduction returned to a term it had already produced, so it cycles forever. The term has NO normal form.
BudgetSpent
The step budget ran out. The term may or may not have a normal form.
TooDeep
The term nests deeper than the kernel will descend, so the reducer never started.