×

zbMATH — the first resource for mathematics

A note on shortest developments. (English) Zbl 1131.68039
Summary: 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.

MSC:
68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus
PDF BibTeX XML Cite
Full Text: DOI