"OWHY is Y in the Typed Lambda Calculus"

ABSTRACT:

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 . It appears first in a typed context in Scott's work and also in Richard Platek's thesis , and forms the basis for L.C.F and its decendents. 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 an old result of ours. 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. (3) the question of the decidability of the word problem. We shall show that it is in general undecidable whether two lambda Y terms interconvert. This solves an old problem due to Albert Meyer, and is done by an encoding of register machines. In addition, we shall give a decision proceedure for the special case of only Y's of type (0->0)->0.
 

Back to Talks Page