Subtyping in DHOL -- Extended preprint

• URL: http://arxiv.org/abs/2507.02855v1
• Date: Thu, 03 Jul 2025 17:59:00 GMT
• Title: Subtyping in DHOL -- Extended preprint
• Abstract summary: Recently introduced dependent typed higher-order logic (DHOL) offers compromise between expressiveness and automation support.<n>We leverage this design to extend DHOL with refinement and quotient types.<n>We present the syntax, semantics, and translation to HOL for the extended language.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Alternative UX Extensions and Their Trade-offs for Code Completion in Pharo [0.13381749415517016]
  Complishon is Pharo's context-aware code completion engine.<n>This paper presents four extensions that address these limits.<n>For each extension, we describe the implementation, discuss alternative designs, and explain the trade-offs involved.
  arXiv  Detail & Related papers  (2026-07-27T10:42:53Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• Variational Learning for Insertion-based Generation [50.15012125719375]
  We introduce a probabilistic framework for learning insertion order in variable-length insertion models.<n>We propose the Insertion Process (IP), a generative model that jointly learns where to insert, what to insert, and when to terminate.
  arXiv  Detail & Related papers  (2026-06-01T11:59:46Z)
• Neuro-Symbolic Query Compiler [57.78201019000895]
  This paper presents QCompiler, a neuro-symbolic framework inspired by linguistic grammar rules and compiler design, to bridge this gap.<n>It theoretically designs a minimal yet sufficient Backus-Naur Form (BNF) grammar $G[q]$ to formalize complex queries.<n>The atomicity of the sub-queries in the leaf ensures more precise document retrieval and response generation, significantly improving the RAG system's ability to address complex queries.
  arXiv  Detail & Related papers  (2025-05-17T09:36:03Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  We introduce a type-constrained decoding approach that leverages type systems to guide code generation.<n>For this purpose, we develop novel prefix automata and a search over inhabitable types, forming a sound approach to enforce well-typedness on LLM-generated code.<n>Our approach reduces compilation errors by more than half and significantly increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• Experiments with Choice in Dependently-Typed Higher-Order Logic [3.072340427031969]
  We extend the DHOL term structure by Hilbert's indefinite choice operator $epsilon$. We define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL. We evaluate the extended translation on a set of dependent HOL problems that require choice.
  arXiv  Detail & Related papers  (2024-10-11T14:49:45Z)
• Automata-based constraints for language model decoding [9.137697105669142]
  Language models (LMs) are often expected to generate strings in some formal language. tuning requires significant resources, making it impractical for uncommon or task-specific formats. We solve these issues through the application of automata theory. Our system compiles constraints 7,000x faster, is provably correct, and can be extended in a modular fashion.
  arXiv  Detail & Related papers  (2024-07-11T00:25:01Z)
• Lexinvariant Language Models [84.2829117441298]
  Token embeddings, a mapping from discrete lexical symbols to continuous vectors, are at the heart of any language model (LM) We study textitlexinvariantlanguage models that are invariant to lexical symbols and therefore do not need fixed token embeddings in practice. We show that a lexinvariant LM can attain perplexity comparable to that of a standard language model, given a sufficiently long context.
  arXiv  Detail & Related papers  (2023-05-24T19:10:46Z)
• Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint [0.0]
  Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL.
  arXiv  Detail & Related papers  (2023-05-24T17:40:54Z)
• TypeT5: Seq2seq Type Inference using Static Analysis [51.153089609654174]
  We present a new type inference method that treats type prediction as a code infilling task. Our method uses static analysis to construct dynamic contexts for each code element whose type signature is to be predicted by the model. We also propose an iterative decoding scheme that incorporates previous type predictions in the model's input context.
  arXiv  Detail & Related papers  (2023-03-16T23:48:00Z)
• Recent advances in the Self-Referencing Embedding Strings (SELFIES) library [1.9573380763700712]
  String-based molecular representations play a crucial role in cheminformatics applications. Traditional string-based representations such as SMILES are often prone to syntactic and semantic errors when produced by generative models. SELF-referencIng Embedded Strings (SELFIES) was proposed that is inherently 100% robust, alongside an accompanying open-source implementation.
  arXiv  Detail & Related papers  (2023-02-07T17:24:08Z)
• Few-Shot Semantic Parsing with Language Models Trained On Code [52.23355024995237]
  We find that Codex performs better at semantic parsing than equivalent GPT-3 models. We find that unlike GPT-3, Codex performs similarly when targeting meaning representations directly, perhaps as meaning representations used in semantic parsing are structured similar to code.
  arXiv  Detail & Related papers  (2021-12-16T08:34:06Z)
• Asking without Telling: Exploring Latent Ontologies in Contextual Representations [12.69022456384102]
  We show that pretrained contextual encoders learn to encode meaningful notions of linguistic structure without explicit supervision. Our results provide new evidence of emergent structure in pretrained encoders, including departures from existing annotations.
  arXiv  Detail & Related papers  (2020-04-29T23:20:40Z)
• Improve Variational Autoencoder for Text Generationwith Discrete Latent Bottleneck [52.08901549360262]
  Variational autoencoders (VAEs) are essential tools in end-to-end representation learning. VAEs tend to ignore latent variables with a strong auto-regressive decoder. We propose a principled approach to enforce an implicit latent feature matching in a more compact latent space.
  arXiv  Detail & Related papers  (2020-04-22T14:41:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.