On the \(\lambda Y\) calculus (Q1886326)

In this short and elegant article, the \(\lambda Y\) calculus, which extends the simply typed \(\lambda\)-calculus by the fixed-point combinator \(Y\) of type \((A \to A) \to A\) for any type \(A\), is investigated. The following theorems are shown: (1) Higher-type fixed-point combinators are not definable from lower-type fixed-point combinators. This result was obtained as well by Werner and Damm using a different method. (2) It is decidable whether a given term has a normal form and whether a term has a head normal form. (3) It is undecidable whether two \(\lambda Y\) terms convert. This is done by encoding register machines in the \(\lambda Y\)-calculus. Furthermore, a decision procedure is given for the special case of two \(\lambda Y\) terms containing only \(Y\) of type \((0 \to 0) \to 0\).