New Proofs of Important Theorems of Untyped Extensional λ Calculus

Research paper by A. A. Lyaletsky

Indexed on: 30 Jul '14Published on: 30 Jul '14Published in: Cybernetics and Systems Analysis


This paper contains new proofs of the following two theorems of the untyped extensional λ-calculus: the Curry theorem stating that any λ-term has a βη-normal form if and only if it has a β-normal form and the normalization theorem for βη-reduction. The proposed approach is based on the following well-known results: the postponement theorem of η-reduction and the strong normalization property of η-reduction that allow one to naturally extend some propositions from the usual λ-calculus to the extensional case.