| |
VOLUME 3, ISSUE 4, PAPER 2
|
A Note on Shortest Developments
|
©Morten Heine Sørensen, Formalit
|
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.
|
Publication date: November 5, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(4:2)2007
Hit Counts: 1773 |
 Creative Commons | |
