Continuous normalization for the lambda-calculus and Gödel's T

DOI10.1016/J.APAL.2004.10.003MaRDI QIDQ1772771zbMATH OpenOpenAlexFDO

Authors Klaus Aehlig, Felix Joachimski

Publication date 21 April 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2004.10.003

zbMATH Keywords

\(\lambda\)-calculus\(\omega\)-ruleBöhm treesContinuous normalizationCut elimination and \(\beta\)-reductionsGödel's TLength of reduction sequenceSize of normal form

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Review text

Continuous normalization of derivations, introduced by the reviewer and developed by W. Buchholz, is used here in the situation where non-well founded (proof) figures make more sense than for logical formulas. Untyped lambda calculus has a lot of uses for infinite trees, for example Böhm trees. The authors develop continuous normalization for typed and untyped \(\lambda\)-calculus, as well as for Gödel's T and obtain some interesting new results as well as new proofs of known results. An extensive and sometimes unexplained use of co-recursive and co-inductive notation makes definitions and proofs shorter but more difficult to read.

Recommendations

• scientific article; zbMATH DE number 1948154
• Non-determinism, non-termination and the strong normalization of System T
• New Computational Paradigms
• Strong normalisation for applied lambda calculi
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)

Cites work

• A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
• Analyzing Gödel's T Via Expanded Head Reduction Trees
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Confluence of the coinductive \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed -calculus
• Finite investigations of transfinite derivations
• Finite notations for infinite terms
• scientific article; zbMATH DE number 1615235 (Why is no real title available?)
• scientific article; zbMATH DE number 3933067 (Why is no real title available?)
• scientific article; zbMATH DE number 3497842 (Why is no real title available?)
• scientific article; zbMATH DE number 3508467 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1948154 (Why is no real title available?)
• scientific article; zbMATH DE number 1797606 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Notation systems for infinitary derivations
• Perpetual reductions in -calculus
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Universal coalgebra: A theory of systems
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(6)

• scientific article; zbMATH DE number 4068861 (Why is no real title available?)
• A simple ordinal recursive normalization of Gödel's T
• scientific article; zbMATH DE number 1948154 (Why is no real title available?)
• Analyzing Gödel's T Via Expanded Head Reduction Trees
• Typed Lambda Calculi and Applications
• On the computational complexity of cut-reduction

This page was built for publication: Continuous normalization for the lambda-calculus and Gödel's T

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1772771)