## Abstract

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
ABSTRACT

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