PCF的递归层次结构是严格的
摘要：对于Plotkin的PCF语言的子语言，我们考虑了通过对类型的级别施加一些限制k来获得固定点操作符的。我们证明了这些语言形成了一个严格的层次结构，即对于级别为k的类型，固定点操作符永远无法使用低级别类型的固定点操作符来定义（在观察等价的意义下）。这回答了Berger提出的一个问题。我们的证明在很大程度上利用了最近Longley和Normann的书中介绍的嵌套顺序过程（也称为PCF B"ohm树）的理论。
作者：John Longley
论文ID：1607.04611
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22