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 |