标题： DHOL中的子类型——扩展预印本 显示英文标题

标题： Subtyping in DHOL -- Extended preprint

摘要： 最近引入的依赖类型高阶逻辑（DHOL）在表达能力和自动化支持之间提供了一个有趣的折中方案。 它牺牲了类型系统的可判定性，以显著扩展其相对于标准HOL的表达能力。 然而，它通过将DHOL翻译为HOL，保留了强大的自动定理证明支持。 我们利用这种设计，将精化类型和商类型扩展到DHOL中。 这两种类型通常由实践者请求，但很少由自动定理证明器提供。 这是因为它们本质上需要不可判定的类型，因此很难 retrofit 到可判定的类型系统中。 但有了DHOL已经完成的主要工作，添加它们不仅是可能的，而且优雅且简单。 具体来说，我们将精化类型和商类型作为子类型的一种特殊情况来添加。 这使得相关的规范包含关系或投影映射变为恒等映射，从而避免了表示上的昂贵变化。 我们展示了扩展语言的语法、语义以及到HOL的翻译，包括可靠性和完整性的证明。 显示英文摘要

摘要： The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its expressiveness over standard HOL. Yet it retains strong automated theorem proving support via a sound and complete translation to HOL. We leverage this design to extend DHOL with refinement and quotient types. Both of these are commonly requested by practitioners but rarely provided by automated theorem provers. This is because they inherently require undecidable typing and thus are very difficult to retrofit to decidable type systems. But with DHOL already doing the heavy lifting, adding them is not only possible but elegant and simple. Concretely, we add refinement and quotient types as special cases of subtyping. This turns the associated canonical inclusion resp. projection maps into identity maps and thus avoids costly changes in representation. We present the syntax, semantics, and translation to HOL for the extended language, including the proofs of soundness and completeness.