IMCS/Publications/CSJM/Issues/CSJM v.23, n.2 (68), 2015/

Fundamental theorems of extensional untyped lambda-calculus revisited

Authors: Alexandre Lyaletsky


This paper presents new proofs of three following fundamental theorems of the untyped extensional lambda-calculus: the eta-Postpo-nement theorem, the beta eta-Normal form theorem, and the Norma-lization theorem for beta eta-reduction. These proofs do not involve any special extensions of the standard language of lambda-terms but nevertheless are shorter and much more comprehensive than their known analogues.

Institution: Taras Shevchenko National University of Kyiv (Faculty of Cybernetics)
Phone: +38 067 4086768

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License


Adobe PDF document0.12 Mb