Subtyping in DHOL -- Extended preprint
This work addresses a practical need for refinement and quotient types in automated theorem provers, which are difficult to add to decidable systems, by leveraging DHOL's existing undecidable type system.
The authors extended dependent typed higher-order logic (DHOL) with refinement and quotient types by implementing them as special cases of subtyping, which avoids costly representation changes and maintains soundness and completeness in translation to 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.