Fundamental theorems of extensional untyped $\lambda$-calculus revisited

Abstract

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.

Keywords

• extensional untyped $\lambda$-calculus
• $\beta\eta$-reduction
• postponement of $\eta$-reduction
• $\eta$-Postponement theorem
• $\beta\eta$-Nor-mal form theorem
• Normalization theorem for $\beta\eta$-reduction