| J.R. Kennaway (2007) | |||||||||||||||
Abstract | |||||||||||||||
| In a previous paper we have established the theory of transfinite reduction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. From the viewpoint of infinitary rewriting, the Bohm model of the lambda calculus can be seen as an infinitary term model. In contrast to term rewriting, there are several different possible notions of infinite term, which give rise to different Bohmlike models, which embody different notions of lazy or eager computation. 1 Introduction In this paper we extend to the lambda calculus the theory of transfinite term rewriting developed in [8]. Infinitary rewriting is a natural generalisation of finitary rewriting which extends it with the notion of computing towards a possibily infinite limit. Such limits naturally arise in the semantics of lazy functional languages, in which it is possible to write and compute with terms which intuitively denote infinite data structures, such as a list of all the integers. I... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||