An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus
Logic in Computer Science
2026-03-05 v1
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.
Cite
@article{arxiv.2603.04017,
title = {An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus},
author = {Rob Nederpelt and Ferruccio Guidi},
journal= {arXiv preprint arXiv:2603.04017},
year = {2026}
}
Comments
In Proceedings LTT 2026, arXiv:2603.02912. Dedicated to Stefano Berardi on the occasion of his 64th birthday in honor of his extensive and diverse research in theoretical computer science