A Note on Shortest Developments
Logic in Computer Science
2015-07-01 v2
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.
Cite
@article{arxiv.0708.0200,
title = {A Note on Shortest Developments},
author = {Morten Heine Sørensen},
journal= {arXiv preprint arXiv:0708.0200},
year = {2015}
}