Morten Heine Sørensen - A Note on Shortest Developments

lmcs:838 - Logical Methods in Computer Science, November 5, 2007, Volume 3, Issue 4 - https://doi.org/10.2168/LMCS-3(4:2)2007
A Note on Shortest DevelopmentsArticle

Authors: Morten Heine Sørensen

    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.


    Volume: Volume 3, Issue 4
    Published on: November 5, 2007
    Imported on: April 10, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    1 Document citing this article

    Consultation statistics

    This page has been seen 921 times.
    This article's PDF has been downloaded 225 times.