Continuous normalization for the lambda-calculus and Gödel's T (Q1772771): Difference between revisions

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.