Superdevelopments for Weak Reduction

TL;DR

This paper investigates superdevelopments in the weak lambda calculus, introducing new reduction techniques and proving their equivalence, thereby advancing understanding of reduction processes in this constrained computational model.

Contribution

It introduces labeled and simultaneous reduction formulations for superdevelopments in the weak lambda calculus and proves their equivalence, extending the theory of reduction in this setting.

Findings

Labeled and simultaneous reduction formulations are equivalent.

Superdevelopments allow reduction of residual and newly created redexes.

New redex creation mechanisms are identified in the weak lambda calculus.

Abstract

We study superdevelopments in the weak lambda calculus of Cagman and Hindley, a confluent variant of the standard weak lambda calculus in which reduction below lambdas is forbidden. In contrast to developments, a superdevelopment from a term M allows not only residuals of redexes in M to be reduced but also some newly created ones. In the lambda calculus there are three ways new redexes may be created; in the weak lambda calculus a new form of redex creation is possible. We present labeled and simultaneous reduction formulations of superdevelopments for the weak lambda calculus and prove them equivalent.