On the λY calculus

The λY calculus is the simply typed λ calculus augmented with the fixed point operators. We show three results about λY: (a) the word problem is undecidable, (b) weak normalisability is decidable, and (c) higher type fixed point operators are not definable from fixed point operators at smaller types.