natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In a rewriting system, a term is said to be of normal form if it does not admit any further rewrites.
In type theory, a canonical form is a normal form, but the converse need not hold.
A term is weakly normalizing if there exists at least one particular sequence of rewrites that eventually yields a normal form. A rewrite has weak normalization if every term has this property.
A term is strongly normalizing if every sequence of rewrites eventually terminates with a normal form. If every term has this property, the rewrite system has strong normalization.
In the untyped lambda calculus the term is neither strongly nor weakly normalizing.
One method for obtaining normal forms, in the context of dependent type theory, is normalisation by evaluation?.
Last revised on May 9, 2023 at 13:19:44. See the history of this page for a list of all contributions to it.