Continuous normalization for the lambda-calculus and Gödel's T (Q1772771): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/j.apal.2004.10.003 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2024515723 / rank | |||
Normal rank | |||
Revision as of 02:34, 20 March 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
