$D_{<:}$的不可判定性及其判定片段
Undecidability of $D_{<:}$ and Its Decidable Fragments
摘要：
依赖对象类型（DOT）是一个包含路径依赖类型、交集类型和对象自引用的演算，它是Scala 3的核心演算。虽然演算已经被证明是合理的，但DOT中的类型检查是否是可判定的仍然是开放的。本文给出了DOT的一个语法子集$D_{<:}$的类型检查和子类型的不可判定性证明。事实证明，即使对于$D_{<:}$，不可判定性也令人惊讶地难以显示，这一点可以通过过去尝试的反例得到证明。为了证明不可判定性，我们发现了范式中的$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 bad bounds 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
