Abstract. The paper contains new proofs of the following two theorems for the untyped extensional λ-calculus: the Curry theorem that any λ-term has a βη-normal form if and only if it has a βη-normal form, and the normalization theorem for βη-reduction. Our approach is based on the following well-known results: the postponement theorem of η-reduction and the strong normalization property of η-reduction, which allow one to extend, in a natural way, some propositions from the usual λ-calculus onto the extensional case.
Keywords: untyped extensional λ-calculus, postponement of η-reduction, theorem on βη-normal form, normalization theorem for βη-reduction.
Лялецкий Александр Александрович,
кандидат физ.-мат. наук, младший научный сотрудник
Киевского национального университета имени Тараса Шевченко,
e-mail: foraal@mail.ru.