An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus
Abstract
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.
Fields of Study & Subjects
Logic
programming
and type systems
Advanced Algebra and Logic
Computability
AI Algorithms
Publication details
- Journal / source
- Electronic Proceedings in Theoretical Computer Science
- Volume
- 441
- Pages
- 197–212
- Publication date
- 3 March 2026
- Language
- EN