The recursion hierarchy for PCF is strict

We consider the sublanguages of Plotkin's PCF obtained by imposing some boundk on the levels of types for which fixed point operators are admitted. We showthat these languages form a strict hierarchy, in the sense that a fixed pointoperator for a type of level k can never be defined (up to observationalequivalence) using fixed point operators for lower types. This answers aquestion posed by Berger. Our proof makes substantial use of the theory ofnested sequential procedures (also called PCF B\"ohm trees) as expounded in therecent book of Longley and Normann