一句话：证明在 PCF 中按类型层级限制不动点算子会形成严格递归层级，低层不动点无法定义高层不动点。
论文研究 Plotkin 的 PCF 语言中按类型层级限制不动点算子所得的各个子语言。具体地，对每个 k，只允许层级不超过 k 的类型使用不动点算子，称其为递归层级 k 的子语言。作者证明这些子语言构成严格层级：对于层级为 k 的类型，其不动点算子无法用更低层级的不动点算子定义，即使只要求到观测等价也不行。这回答了 Berger 提出的问题。证明方法大量使用嵌套顺序过程（nested sequential procedures，也称 PCF Böhm 树）理论，该理论在 Longley 与 Normann 的专著中已系统阐述。
We consider the sublanguages of Plotkin's PCF obtained by imposing some bound k on the levels of types for which fixed point operators are admitted. We show that these languages form a strict hierarchy, in the sense that a fixed point operator for a type of level k can never be defined (up to observational equivalence) using fixed point operators for lower types. This answers a question posed by Berger. Our proof makes substantial use of the theory of nested sequential procedures (also called PCF B\"ohm trees) as expounded in the recent book of Longley and Normann.