An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911484267724800 |
|---|---|
| author | Nederpelt, Rob Guidi, Ferruccio |
| author_facet | Nederpelt, Rob Guidi, Ferruccio |
| contents | Terms in the lambda-calculus can be represented as planar trees decorated with symbols for abstraction and application, and having variables as leaves. In this paper, we concentrate on the branches of such trees, rather than on the trees themselves. We reformulate several well-known notions of beta-reduction in this view. In a natural manner, this reconsideration eventually leads to a new form of beta-reduction, being expanding in the sense that the reduction of term t1 to term t2 entails that the tree of t1 is a subtree of the tree of t2. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_04017 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus Nederpelt, Rob Guidi, Ferruccio Logic in Computer Science F.4.1 Terms in the lambda-calculus can be represented as planar trees decorated with symbols for abstraction and application, and having variables as leaves. In this paper, we concentrate on the branches of such trees, rather than on the trees themselves. We reformulate several well-known notions of beta-reduction in this view. In a natural manner, this reconsideration eventually leads to a new form of beta-reduction, being expanding in the sense that the reduction of term t1 to term t2 entails that the tree of t1 is a subtree of the tree of t2. |
| title | An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2603.04017 |