Cybernetics And Systems Analysis logo
Editorial Board Announcements Abstracts Authors Contents
Cybernetics And Systems Analysis
International Theoretical Science Journal
UDC 510.584
A.A. Lyaletsky

NEW PROOFS OF IMPORTANT THEOREMS OF UNTYPED EXTENSIONAL λ-CALCULUS

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.



FULL TEXT

Лялецкий Александр Александрович,
кандидат физ.-мат. наук, младший научный сотрудник Киевского национального университета имени Тараса Шевченко,
e-mail: foraal@mail.ru.

© 2017 Kibernetika.org. All rights reserved.