Fundamental theorems of extensional untyped $\lambda$-calculus revisited
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...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Institute of Mathematics and Computer Science of the Academy of Sciences of Moldova
2015-10-01
|
| Series: | Computer Science Journal of Moldova |
| Subjects: | |
| Online Access: | http://www.math.md/files/csjm/v23-n2/v23-n2-(pp153-164).pdf |
| id |
doaj-89feb1f36e6b45b7a9fab38ced6c7395 |
|---|---|
| record_format |
Article |
| spelling |
doaj-89feb1f36e6b45b7a9fab38ced6c73952020-11-25T01:47:57ZengInstitute of Mathematics and Computer Science of the Academy of Sciences of MoldovaComputer Science Journal of Moldova1561-40422015-10-01232(68)153164Fundamental theorems of extensional untyped $\lambda$-calculus revisitedAlexandre Lyaletsky0Taras Shevchenko National University of Kyiv (Faculty of Cybernetics)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.http://www.math.md/files/csjm/v23-n2/v23-n2-(pp153-164).pdfextensional untyped $\lambda$-calculus$\beta\eta$-reductionpostponement of $\eta$-reduction$\eta$-Postponement theorem$\beta\eta$-Nor-mal form theoremNormalization theorem for $\beta\eta$-reduction |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Alexandre Lyaletsky |
| spellingShingle |
Alexandre Lyaletsky Fundamental theorems of extensional untyped $\lambda$-calculus revisited Computer Science Journal of Moldova 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 |
| author_facet |
Alexandre Lyaletsky |
| author_sort |
Alexandre Lyaletsky |
| title |
Fundamental theorems of extensional untyped $\lambda$-calculus revisited |
| title_short |
Fundamental theorems of extensional untyped $\lambda$-calculus revisited |
| title_full |
Fundamental theorems of extensional untyped $\lambda$-calculus revisited |
| title_fullStr |
Fundamental theorems of extensional untyped $\lambda$-calculus revisited |
| title_full_unstemmed |
Fundamental theorems of extensional untyped $\lambda$-calculus revisited |
| title_sort |
fundamental theorems of extensional untyped $\lambda$-calculus revisited |
| publisher |
Institute of Mathematics and Computer Science of the Academy of Sciences of Moldova |
| series |
Computer Science Journal of Moldova |
| issn |
1561-4042 |
| publishDate |
2015-10-01 |
| description |
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. |
| topic |
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 |
| url |
http://www.math.md/files/csjm/v23-n2/v23-n2-(pp153-164).pdf |
| work_keys_str_mv |
AT alexandrelyaletsky fundamentaltheoremsofextensionaluntypedlambdacalculusrevisited |
| _version_ |
1725013851646197760 |