In this note we consider three problems concerning the lambda Y calculus obtained from the simply typed lambda calculus by the addition of fixed point combinators Y :(A → A ) → A.
The "paradoxical" combinator Y was first discussed in Curry & Feys Vol 1 [3]. It appears first in a typed context in Scott [7] and also in Richard Platek?s thesis [5], and forms the basis for L.C.F [6] and its descendants.
In this note we shall consider
(1) the question of whether higher type Y are "definable" from lower type Y. We shall show that it is not the case in this context, sharpening a result of ours from [8]. A similar result has been obtained by Warner Damm; (2) the question of the decidability of termination. More precisely, we shall show that it is decidable whether a given term has a normal form. This extends results of Plotkin and Bercovicci. [2]. By similar methods we show that we show that it is decidable whether a term has a head normal form, and whether a term has a finite Bohm tree; (3) the question of the decidability of the word problem. This question was first put to us by Albert Meyer 20 years ago. We shall show that it is in general undecidable whether two lambda Y terms convert. This is done by encoding the behavior of register machines. In addition we shall give a decision procedure for the special case of only Y?s of type (0 → 0) → 0.
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb