The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.

翻译：有限PCF可达性问题的可判定性已被用作函数式程序全自动验证工具的理论基础。然而，对于带有副作用的有限PCF（如异常、代数效应和引用）的轻微扩展，可达性问题往往变得不可判定，这阻碍了上述验证工具向支持带副作用函数式程序的扩展。本文首先给出了有限PCF四种扩展不可判定性的简明证明，这有助于我们理解和分析不可判定性的来源。随后我们聚焦于带有引用的扩展，通过类型系统给出了一个可判定片段。据我们所知，这是首个非平凡的可判定片段，其特征是包含引用单元的高阶递归函数。