Normalization, canonicity, and decidable checking

For this lesson, use simply typed lambda calculus with function types, binary products, unit, and Booleans. Terms have variable and binder annotations where required; reduction consists of beta reduction, pair projections, Boolean case computation, and their closure inside terms. There is no general fixed-point operator, no extra opaque constants, and no added equations or eta laws. This standard total fragment has preservation, confluence, and strong normalization. These are metatheorems about its well-typed syntax, proved by methods such as reducibility rather than by testing examples.

Strong normalization says that every reduction sequence starting from a well-typed term is finite. Weak normalization would assert only that at least one terminating sequence exists. Confluence says that different reduction choices can be joined. Together they give a unique normal form up to renaming bound variables. Boolean canonicity adds a shape statement: a closed normal term of Boolean type is true or false. An open term may instead be blocked by a variable, so the closedness requirement is essential.

In this simply typed syntax, checking a fully supplied annotated term follows its finite syntax tree and compares the explicitly formed simple types. Types do not contain term indices, so that checking task does not itself require evaluating arbitrary programs inside types. Separately, judgmental equality generated by the stated computation rules is decidable by normalizing both well-typed terms and comparing the normal forms up to bound-variable renaming. Finite terminating normalization makes that comparison an algorithm, while confluence makes it complete for this conversion relation.

Dependent theories introduce additional conversion obligations because types may contain terms. Proving decidable checking there requires specifying the universe hierarchy, identity rules, inductive types, annotations, and equality algorithm of that theory. This lesson does not transfer its simply typed theorem to every such extension. Nor does decidable checking mean an algorithm can discover a proof of every true mathematical statement: checking a proposed finite certificate and solving unrestricted proof search are different problems, especially once arithmetic or stronger axioms enter the language.

An unrestricted fixed-point operator permits a term that repeatedly unfolds to itself, so the strong-normalization conclusion fails. An opaque postulated Boolean constant gives a different example: it may be a closed normal Boolean term that is neither constructor, even without introducing an infinite reduction. Such a constant need not be inconsistent, but the original constructor-canonicity statement no longer describes the enlarged syntax. Termination and canonicity therefore fail for different reasons and should be audited separately.

Postulating univalence in ordinary intensional type theory similarly does not automatically add executable transport rules. Cubical type theories supply additional computational structure and require their own proofs. Huber's cited canonicity result concerns natural-number terms in the specified cubical calculus with only dimension-name variables in the context. That theorem is not, by itself, a normalization or decidable-checking theorem for every cubical extension. Reporting the actual calculus and conclusion is more informative than claiming that one foundational label guarantees every desirable computational property.