| From Finite to Infinite Lambda Calculi (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. This results in several new Bohm models of the lambda calculus, and new unifying descriptions of existing models. 1 Introduction In this note we outline our theory of infinite rewriting for lambda calculus. A more detailed version will appear in the forthcoming proceedings of RTA'95 [KKSdV95]. Infinitely long rewrite sequences of possibly infinite terms are of interest for several reasons. ffl First, it enriches finitary rewriting with the natural notion of computing towards some limit. If such a (possibly infinite) limit still contains redexes, then one can continue computing. The question of the computational meaning of such transfinite sequences will be dealt with below in the discussion of the Compressing Property. ffl Secondly, in functional programming real computations with terms implemented as graph... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||