INFINITARY LAMBDA-CALCULUS

In a previous paper we have established the theory of transfinite redu ction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. From the viewpoint of infinitar y rewriting, the Bohm model of the lambda calculus can be seen as an i nfinitary term model. In contrast to term rewriting, there are several different possible notions of infinite term, which give rise to diffe rent Bohm-like models, which embody different notions of lazy or eager computation.