Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Rob Nederpelt, Ferruccio Guidi

TL;DR

This paper reformulates several well-known notions of beta-reduction in this view, and concludes that the reduction of term t1 to term t2 entails that the tree of t1 is a subtree of the tree of t2.

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.

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

TL;DR

This paper reformulates several well-known notions of beta-reduction in this view, and concludes that the reduction of term t1 to term t2 entails that the tree of t1 is a subtree of the tree of t2.

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.
Paper Structure (17 sections, 12 theorems, 1 equation, 4 figures)

This paper contains 17 sections, 12 theorems, 1 equation, 4 figures.

Table of Contents

  1. Preliminary remarks
  2. Introduction
  3. About the tree structure of lambda terms
  4. Lambda trees and paths
  5. beta-reduction
  6. A short history of updating in namefree beta-reduction
  7. The usual beta-reduction in the path-approach
  8. Comparing beta-reduction in namecarrying and namefree lambda-calculus
  9. Alternative beta-reductions
  10. Balanced beta-reduction in namefree lambda-calculus
  11. Focused beta-reduction in namefree lambda-calculus
  12. Erasing reduction
  13. Theorems
  14. A new, lossfree beta-reduction
  15. Expanding beta-reduction
  16. ...and 2 more sections

Key Result

Lemma 1.5

Along different paths in a $\lambda$-tree, one finds different strings of labels.

Figures (4)

  • Figure 1: Namefree lambda trees; traditional and adapted
  • Figure 2: The binding of a variable; traditional and adapted
  • Figure 3: A picture of namefree $\beta$-reduction with updating
  • Figure 4: A picture of namefree, expanding $\beta$-reduction

Theorems & Definitions (36)

  • Example 1.1
  • Definition 1.4
  • Lemma 1.5
  • Definition 1.6
  • Definition 1.7
  • Definition 1.8
  • Definition 1.9
  • Lemma 1.10
  • Definition 2.1
  • Definition 2.2
  • ...and 26 more