A recursive normalizing one-step reduction strategy for the distributive lambda calculus

TL;DR

This paper introduces a recursive normalizing one-step reduction strategy for the micro lambda calculus, addressing a longstanding open question about its existence and effectiveness.

Contribution

It provides a positive answer to the open question by proposing a new reduction strategy that normalizes micro lambda calculus using recursive distribution of beta-redexes.

Findings

The strategy guarantees normalization for micro lambda calculus expressions.

It offers a new approach to implement beta-reduction recursively.

The method enhances understanding of reduction strategies in lambda calculus.

Abstract

We positively answer the question A.1.6 in J. Klop's "Ustica Notes": "Is there a recursive normalizing one-step reduction strategy for micro $\lambda$-calculus?" Micro $\lambda$-calculus refers to an implementation of the $\lambda$-calculus due to Revesz, implementing $\beta$-reduction by means of "micro steps" recursively distributing a $\beta$-redex $(\lambda x.M)\ N$ over its body $M$.