| Infinitary Lambda Calculus (1997) | |||||||||||||||
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 Bohm-like models, which embody different notions of lazy or eager computation. 1 Introduction 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 expressions which intuitively denote infinite data structures, such as a list of all the integers. If the limit of a reduction 3 Email addresses: jrk@sys.uea.ac.uk, jwk@cwi.nl, mrs@sys.uea.ac.uk, and... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||