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
A rewriting system is terminating if we cannot perform a never-ending computation.
Let $(X,\rightarrow)$ be an abstract rewriting system. Then $\rightarrow$ is terminating, strongly normalizing or noetherian iff there doesn’t exist any infinite reduction $x_{1} \rightarrow x_{2} \rightarrow ... \rightarrow x_{n} \rightarrow ...$
The cut elimination of second order linear logic? is strongly normalizable, see Pagani & Tortora de Falco (2009) where they prove it using notably Girard’s reducibility candidates.
It is possible that only one term is strongly normalizable but not the entire rewriting system: see normal form.
On strong normalization of second order linear logic:
Last revised on December 13, 2022 at 10:43:05. See the history of this page for a list of all contributions to it.