An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus

TL;DR

This paper offers a novel perspective on beta-reduction in namefree lambda-calculus by representing terms as planar decorated trees and introducing an expanding form of reduction based on subtree relations.

Contribution

It reinterprets beta-reduction through tree structures and introduces a new expanding reduction form that emphasizes subtree relationships.

Findings

Reformulation of beta-reduction using planar tree representations

Introduction of an expanding beta-reduction concept

Establishment of subtree-based reduction properties

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.