在高阶逻辑中加入精细类型和商类型，让证明更灵活且自动支持。
Subtyping in DHOL -- Extended preprint
- 用子类型机制优雅扩展依赖型高阶逻辑，支持精细和商类型。
- 新增类型在转换到标准高阶逻辑时保持可证明性与完整性。
- 适合需要复杂类型系统的形式化验证开发者使用。
最近提出的依赖型高阶逻辑（DHOL）在表达力与自动化支持之间取得良好平衡：牺牲类型系统判定性以显著提升表达力，同时通过可靠且完备的翻译机制保留强大的自动化定理证明能力。本文利用这一设计，向DHOL中引入了精细类型和商类型——这两类在实践中常被需求但极少由自动化定理证明器支持的特性。原因在于它们本质上要求不可判定的类型检查，难以嵌入判定型系统。而由于DHOL已承担主要计算负担，添加这些类型不仅可行，而且优雅简洁。具体地，我们将精细类型和商类型作为子类型的特例处理，使相关的包含映射或投影映射退化为恒等映射，从而避免了表示层面的开销。本文给出了扩展语言的语法、语义及到标准高阶逻辑的翻译规则，并证明了其可靠性和完备性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。