A Note on Shortest Developments

TL;DR

This paper introduces a duality-based approach to prove the finiteness of shortest developments in lambda calculus, providing effective strategies and formulas, simplifying prior work and highlighting differences with beta-reduction.

Contribution

It presents a novel duality principle that extends de Vrijer's finite developments theorem to shortest developments, simplifying existing proofs and strategies.

Findings

Establishes finiteness of some shortest developments

Provides an effective reduction strategy for shortest developments

Simplifies previous proofs by Khasidashvili

Abstract

De Vrijer has presented a proof of the finite developments theorem which, in addition to showing that all developments are finite, gives an effective reduction strategy computing longest developments as well as a simple formula computing their length. We show that by applying a rather simple and intuitive principle of duality to de Vrijer's approach one arrives at a proof that some developments are finite which in addition yields an effective reduction strategy computing shortest developments as well as a simple formula computing their length. The duality fails for general beta-reduction. Our results simplify previous work by Khasidashvili.