Continuous normalization for the lambda-calculus and Gödel's T (Q1772771): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Removed claim: reviewed by (P1447): Item:Q454365 |
||
Property / reviewed by | |||
Property / reviewed by: Grigori Mints / rank | |||
Revision as of 12:35, 15 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Continuous normalization for the lambda-calculus and Gödel's T |
scientific article |
Statements
Continuous normalization for the lambda-calculus and Gödel's T (English)
0 references
21 April 2005
0 references
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.
0 references
Continuous normalization
0 references
\(\lambda\)-calculus
0 references
Böhm trees
0 references
Length of reduction sequence
0 references
Size of normal form
0 references
Cut elimination and \(\beta\)-reductions
0 references
\(\omega\)-rule
0 references
Gödel's T
0 references