Volume 6: January - December 1996

Issue 5: October 1996


Pruning simply typed [lambda]-terms

  • Pruning simply typed [lambda]-terms
  • S. Berardi Dipartimento di Informatica dell'Universita' di Torino, Corso Svizzera 185, 10149 Torino, Italy


    We say that a simply typed [lambda]-term is a 'pruning' of another one if the former is obtained from the latter by replacing some subterms with dummy constants. We prove that 'pruning' preserves observational behaviour of a simply typed [lambda]-term if it does not modify the type nor the context (assignment of types to free variables) of the term. This result is used to define a map F1 : {simply typed [lambda]-terms} -> {simply typed [lambda]-terms} removing redundant code in functional programs. In the rest of the paper we prove some property of F1 interesting from computational viewpoint. An algorithm to compute F1 is in the Appendix.

    Keywords: Simply typed lambda calculus, dead code, program extraction.

    Pages: 663 - 681

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Last updated 19 Nov 96

    Part of the OUP Journals World Wide Web service.

    Copyright Oxford University Press, 1996