一句话：证明 D<: 的类型检查与子类型不可判定，并给出两个可判定片段与判定算法。
DOT 是 Scala 3 的核心演算，具有路径依赖类型、交叉类型和对象自引用；该演算虽已被证明可靠，但其类型检查是否可判定仍悬而未决。本文针对 DOT 的语法子集 D<:，证明类型检查与子类型关系不可判定，并指出此前尝试的反例说明证明的困难。作者发现 D<: 子类型规则的一种等价范式定义，将子类型反射显式表示为单条推理规则；移除该规则后得到两个可判定子类型片段，并给出判定算法。论文证明了算法相对这些片段的可靠性与完备性以及终止性，全部证明在 Coq 与 Agda 中机器化。
Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the calculus has been proven sound, it remains open whether type checking in DOT is decidable. In this paper, we establish undecidability proofs of type checking and subtyping of D <: , a syntactic subset of DOT. It turns out that even for D <: , undecidability is surprisingly difficult to show, as evidenced by counterexamples for past attempts. To prove undecidability, we discover an equivalent definition of the D <: subtyping rules in normal form. Besides being easier to reason about, this definition makes the phenomenon of subtyping reflection explicit as a single inference rule. After removing this rule, we discover two decidable fragments of D <: subtyping and identify algorithms to decide them. We prove soundness and completeness of the algorithms with respect to the fragments, and we prove that the algorithms terminate. Our proofs are mechanized in a combination of Coq and Agda.
@article{paperbot539,
title = {Undecidability of
<i>
d
<sub><:</sub>
</i>
and its decidable fragments},
author = {Jason Z. S. Hu and Ondřej Lhoták},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371077}
}