一句话：给出 finitary PCF 四种扩展不可判定性的简单证明，并用类型系统刻画含引用单元的可判定片段。
finitary PCF 的可达性问题一直是函数式程序全自动验证工具的理论基础，但一旦加入异常、代数效应、引用等副作用，该问题往往变得不可判定，从而阻碍这类验证工具支持带副作用的函数式程序。本文首先为 finitary PCF 的四种扩展给出简洁的不可判定性证明，以帮助理解不可判定性的来源；随后聚焦于带引用单元的扩展，通过设计类型系统界定出一个可判定片段。据作者所知，这是首个包含引用单元且支持高阶递归函数的非平凡可判定片段。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Kobayashi25,
title = {On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus},
author = {Naoki Kobayashi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704875}
}