Sørensen, Morten Heine - A Note on Shortest Developments

lmcs:838 - Logical Methods in Computer Science, November 5, 2007, Volume 3, Issue 4
A Note on Shortest Developments

Authors: Sørensen, Morten Heine

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.


Source : oai:arXiv.org:0708.0200
DOI : 10.2168/LMCS-3(4:2)2007
Volume: Volume 3, Issue 4
Published on: November 5, 2007
Submitted on: April 10, 2007
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 35 times.
This article's PDF has been downloaded 33 times.