# On stepwise explicit substitution

F. Kamareddine, R.P. Nederpelt

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

## Samenvatting

This paper starts by setting the ground for a lambda calculus notation that strongly mirrors the two fundamental operations of term construction, namely abstraction and application. In particular, we single out those parts of a term, called items in the paper, that are added during abstraction and application. This item notation proves to be a powerful device for the representation of basic substitution steps, giving rise to different versions of ß-reduction including local and global ß-reduction. In other words substitution, thanks to the new notation, can be easily formalised as an object language notion rather than remaining a meta language one. Such formalisation will have advantages with respect to various areas including functional application and the partial unfolding of definitions. Moreover our substitution is, we believe, the most general to date. This is shown by the fact that our framework can accommodate most of the known reduction strategies, which range from local to global. Finally, we show how the calculus of substitution of Abadi et al., can be embedded into our calculus. We show moreover that many of the rules of Abadi et al. are easily derivable in our calculus.
Originele taal-2 Engels 197-240 International Journal of Foundations of Computer Science 4 3 https://doi.org/10.1142/S0129054193000146 Gepubliceerd - 1993

## Vingerafdruk

Duik in de onderzoeksthema's van 'On stepwise explicit substitution'. Samen vormen ze een unieke vingerafdruk.