一句话：该论文研究渐进类型迁移空间的关键可判定性，给出三种算法并证明判定极大元存在性为 NP 难。
论文关注渐进类型迁移：程序员可通过更精确的类型标注改进程序可读性、效率与安全性，而迁移过程需要工具支持。作者为渐进类型迁移空间建立可判定性基础，提出三种算法，分别判定迁移空间是否有限、是否具有顶元素、是否为单元素集，并证明判定其是否具有极大元素是 NP 难的。作者实现了这些算法，并在微基准测试套件上验证其行为符合预期。这些结果有助于在迁移探索中提供更好的工具支持。
Programmers can use gradual types to migrate programs to have more precise type annotations and thereby improve their readability, efficiency, and safety. Such migration requires an exploration of the migration space and can benefit from tool support, as shown in previous work. Our goal is to provide a foundation for better tool support by settling decidability questions about migration with gradual types. We present three algorithms and a hardness result for deciding key properties and we explain how they can be useful during an exploration. In particular, we show how to decide whether the migration space is finite, whether it has a top element, and whether it is a singleton. We also show that deciding whether it has a maximal element is NP-hard. Our implementation of our algorithms worked as expected on a suite of microbenchmarks.