pith. machine review for the scientific record. sign in

arxiv: 2605.00295 · v1 · submitted 2026-04-30 · 💻 cs.LO

Recognition: unknown

Polymorphism Meets DHOL

Cezary Kaliszyk, Florian Rabe, Rhea Ranalter

Pith reviewed 2026-05-09 19:20 UTC · model grok-4.3

classification 💻 cs.LO
keywords polymorphismdependent higher-order logicDHOLHOLtheorem provingTPTPlogic embedding
0
0 comments X

The pith

Polymorphic dependent higher-order logic can be translated to standard HOL while supporting dependent encodings.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines syntax and semantics for a polymorphic extension of DHOL, which combines dependent types with classical higher-order logic. This allows more flexible encodings of domains such as size-bounded data structures, category theory, and proof theory. The authors extend the existing translation from DHOL to HOL to handle polymorphism and implement the result in a logic-embedding tool. Evaluation on TPTP formalizations shows that the translated problems can be solved by off-the-shelf HOL theorem provers, creating a practical PDHOL prover for experimentation.

Core claim

We develop the syntax and semantics of polymorphic DHOL and extend the translation to HOL accordingly. Implementation in the logic-embedding tool, together with an off-the-shelf HOL theorem prover, creates a PDHOL theorem prover for experimenting, as shown by evaluation on a range of TPTP formalizations.

What carries the argument

The extended DHOL-to-HOL translation that incorporates polymorphic quantification and dependent types while preserving the original embedding.

Load-bearing premise

Extending the DHOL-to-HOL translation to support polymorphism preserves soundness, completeness, and the ability to encode target domains without introducing inconsistencies.

What would settle it

A concrete polymorphic dependent theorem or theory that becomes inconsistent or unprovable after translation to HOL, yet was consistent or provable in the source logic.

Figures

Figures reproduced from arXiv: 2605.00295 by Cezary Kaliszyk, Florian Rabe, Rhea Ranalter.

Figure 1
Figure 1. Figure 1: DHOL Judgments In [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: DHOL Rules for theories and contexts. Finally, the four rules for forming contexts are parallel to the four rules for forming substitutions. For example, Rule SubTp shows how to extend a substitution δ for ∆ to a substitution for ∆, α : type by adding a type substitute A for α. The rules in [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: DHOL Rules for Types and Terms 4 Translating PDHOL to PHOL Overview Like for DHOL the translation applies dependency erasure, written with an overline X, to turn PDHOL syntax into PHOL syntax. Note that because the latter is a fragment of the former, we can reuse all PDHOL notations to write PHOL syntax. Intuitively, term-dependent types are translated into types without their term arguments. The lost info… view at source ↗
Figure 4
Figure 4. Figure 4: Definition of norm[t] with changes highlighted. sRed(tA) := tA if t has quasi-preimage of type A sRed(fΠx:AB tA) := sRed(sRed(fΠx:AB) sRed(tA)) if fΠx:A.B tA not beta-eta reducible In the following, the term tA on the left-hand side is assumed to not be almost proper with a quasi-preimage of type A : sRed(tA) := sRed(t βη A ) if t eta-beta reducible sRed(sA =A tA′ ) := sRed(sA) =A sRed(tA) sRed(Fo ⇒ Go) :=… view at source ↗
Figure 5
Figure 5. Figure 5: Definition of sRed(t). This is aided by passing, for each term, a DHOL type A to the function, effectively associating them with a quasi-preimage. This is mainly necessary for λ-functions where there are potentially many quasi-preimages of differing types. To ensure correctness, it is, of course, required that an indexed term tA is of [PITH_FULL_IMAGE:figures/full_fig_p025_5.png] view at source ↗
read the original abstract

DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops the syntax and semantics of polymorphic Dependent Higher-Order Logic (PDHOL), extends the existing DHOL-to-HOL translation to accommodate polymorphism, implements the extended translation in the logic-embedding tool, and evaluates the resulting system on a range of TPTP formalizations, thereby providing an automated PDHOL theorem prover via off-the-shelf HOL provers.

Significance. If the translation is faithful, the work would meaningfully extend DHOL's applicability to polymorphic dependent encodings in domains such as category theory and proof theory while retaining access to mature HOL automation. The concrete implementation and TPTP evaluation constitute a practical contribution that enables immediate experimentation; these are strengths that should be retained in any revision.

major comments (2)
  1. [§4 (Translation)] §4 (Translation): The paper states that the translation is extended and that soundness is preserved via the semantic model, yet no theorem is formulated or proved establishing that every PDHOL derivation maps to a valid HOL derivation (and conversely for the image). The interaction between polymorphic instantiation and the existing extensionality and dependent-type rules is described only informally; this is load-bearing for the claim that the implementation yields a sound PDHOL prover.
  2. [§3 (Semantics)] §3 (Semantics): The semantic clauses for polymorphic types and their interaction with dependent function spaces are given, but no lemma or proposition shows that the interpretation is preserved under the translation rules or that the model validates the polymorphic extension of the DHOL axioms. Without this, the semantic justification for soundness remains incomplete.
minor comments (2)
  1. [§5 (Implementation)] §5 (Implementation): The description of how the logic-embedding tool handles polymorphic type variables and the generated HOL signatures would benefit from a small concrete example or pseudocode snippet to improve reproducibility.
  2. [Evaluation] Evaluation section: The abstract and evaluation paragraph mention 'a range of TPTP formalizations' but do not report the number of problems, success rates, or comparison with non-polymorphic DHOL; these quantitative details should be supplied.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and valuable comments on our manuscript. We address the major comments point by point below, outlining the revisions we intend to incorporate to strengthen the formal justification of our results.

read point-by-point responses

  1. Referee: [§4 (Translation)] The paper states that the translation is extended and that soundness is preserved via the semantic model, yet no theorem is formulated or proved establishing that every PDHOL derivation maps to a valid HOL derivation (and conversely for the image). The interaction between polymorphic instantiation and the existing extensionality and dependent-type rules is described only informally; this is load-bearing for the claim that the implementation yields a sound PDHOL prover.

    Authors: We concur that an explicit formulation and proof of the translation's soundness would provide a more rigorous foundation. In the revised version, we will introduce a dedicated theorem in Section 4 that establishes the preservation of derivations under the translation, including a detailed discussion of how polymorphic instantiation interacts with extensionality and dependent-type rules. This will be supported by the semantic model already presented. revision: yes

  2. Referee: [§3 (Semantics)] The semantic clauses for polymorphic types and their interaction with dependent function spaces are given, but no lemma or proposition shows that the interpretation is preserved under the translation rules or that the model validates the polymorphic extension of the DHOL axioms. Without this, the semantic justification for soundness remains incomplete.

    Authors: We appreciate this observation. To complete the semantic justification, we will add a lemma in Section 3 demonstrating that the interpretation of PDHOL terms and types is preserved by the translation rules. Additionally, we will include a proposition verifying that the semantic model satisfies the polymorphic extensions of the DHOL axioms. These additions will directly support the soundness claim. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained extension of prior DHOL/HOL work

full rationale

The paper defines polymorphic DHOL syntax/semantics and extends the existing DHOL-to-HOL translation as a direct construction, then implements and evaluates it on TPTP problems. No load-bearing step reduces by construction to its own inputs, fitted parameters, or self-citation chains; the central soundness/completeness preservation is asserted via the new semantic model rather than derived from prior results by the same authors in a circular manner. This matches the default case of an honest non-finding.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Only abstract available, so ledger is limited to background assumptions stated there; no free parameters or invented entities are described.

axioms (2)
  • domain assumption DHOL is an extensional, classical logic equipped with dependent types.
    Directly stated in the abstract as the starting point.
  • domain assumption Translation from DHOL to HOL enables use of modern automated theorem provers.
    Assumed as the basis for extending the translation to the polymorphic case.

pith-pipeline@v0.9.0 · 5413 in / 1241 out tokens · 39934 ms · 2026-05-09T19:20:09.143878+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

35 extracted references · 11 canonical work pages

  1. [1]

    Allen.A Non-Type-Theoretic Semantics for Type-Theoretic Language

    S. Allen.A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987

    1987

  2. [2]

    Andrews.An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof

    P. Andrews.An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986

    1986

  3. [3]

    Parametricity and dependent types

    Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In Paul Hudak and Stephanie Weirich, editors,Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 345–356. ACM, 2010.doi:10.1145/1863543.1863592

    work page doi:10.1145/1863543.1863592 2010

  4. [4]

    Bhayat and G

    A. Bhayat and G. Reger. A polymorphic vampire - (short paper). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors,Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Pro- ceedings, Part II, volume 12167 ofLecture Notes in Computer Science, pages 361–

    2020

  5. [5]

    Springer, 2020.doi:10.1007/978-3-030-51054-1\_21

    work page doi:10.1007/978-3-030-51054-1 2020

  6. [6]

    A. Church. A Formulation of the Simple Theory of Types.Journal of Symbolic Logic, 5(1):56–68, 1940.doi:10.2307/2266170

    work page doi:10.2307/2266170 1940

  7. [7]

    The Coq Proof Assistant: Reference Manual

    Coq Development Team. The Coq Proof Assistant: Reference Manual. Technical report, INRIA, 2015

    2015

  8. [8]

    (Extensions de la Superposition pour l’Arithmétique Linéaire Entière, l’Induction Structurelle, et bien plus encore)

    Simon Cruanes.Extending Superposition with Integer Arithmetic, Structural In- duction, and Beyond. (Extensions de la Superposition pour l’Arithmétique Linéaire Entière, l’Induction Structurelle, et bien plus encore). PhD thesis, École Poly- technique, Palaiseau, France, 2015. URL:https://tel.archives-ouvertes.fr/ tel-01223502

    2015

  9. [9]

    Hammer for coq: Automation for dependent type theory.J

    Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory.J. Autom. Reason., 61(1-4):423–453, 2018. URL:https://doi.org/ 10.1007/s10817-018-9458-4,doi:10.1007/S10817-018-9458-4

    work page doi:10.1007/s10817-018-9458-4 2018

  10. [10]

    de Moura, S

    L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean Theorem Prover (System Description). In A. Felty and A. Middeldorp, editors, Automated Deduction, pages 378–388. Springer, 2015

    2015

  11. [11]

    Felty and Dale Miller

    Amy P. Felty and Dale Miller. Encoding a dependent-type lambda-calculus in a logic programming language. In Mark E. Stickel, editor,10th International Con- ference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceed- ings, volume 449 ofLecture Notes in Computer Science, pages 221–235. Springer, 1990.doi:10.1007/3-540-52885-7\_90. 20 R. ...

    work page doi:10.1007/3-540-52885-7 1990

  12. [12]

    M. Gordon. HOL: A Proof Generating System for Higher-Order Logic. In G. Birtwistle and P. Subrahmanyam, editors,VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer-Academic Publishers, 1988

    1988

  13. [13]

    Gordon and A

    M. Gordon and A. Pitts. The HOL Logic. In M. Gordon and T. Melham, editors, Introduction to HOL, Part III, pages 191–232. Cambridge University Press, 1993

    1993

  14. [14]

    Harrison

    J. Harrison. HOL Light: A Tutorial Introduction. InProceedings of the First International Conference on Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996

    1996

  15. [15]

    Hofmann.Extensional Constructs in Intensional Type Theory

    M. Hofmann.Extensional Constructs in Intensional Type Theory. CPHC/BCS distinguished dissertations. Springer, 1997

    1997

  16. [16]

    Jacobs and T

    B. Jacobs and T. Melham. Translating dependent type theory into higher order logic. In M. Bezem and J. Groote, editors,Typed Lambda Calculi and Applications, pages 209–29, 1993

    1993

  17. [17]

    Martin-Löf

    P. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. InProceedings of the ’73 Logic Colloquium, pages 73–118. North-Holland, 1974

    1974

  18. [18]

    Proceedings of 12th International Joint Conference on Automated Reasoning

    J. Niederhauser, C. E. Brown, and C. Kaliszyk. Tableaux for automated reasoning in dependently-typed higher-order logic. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors,Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 ofLecture Notes in Compu...

    work page doi:10.1007/978-3-031-63498-7 2024

  19. [19]

    Nipkow, L

    T. Nipkow, L. Paulson, and M. Wenzel.Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, 2002

    2002

  20. [20]

    U. Norell. The Agda WiKi, 2005.http://wiki.portal.chalmers.se/agda

    2005

  21. [21]

    S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D.Kapur,editor,11th International Conference on Automated Deduction (CADE), pages 748–752. Springer, 1992

    1992

  22. [22]

    Admissible types-to-pers relativization in higher-order logic

    Andrei Popescu and Dmitriy Traytel. Admissible types-to-pers relativization in higher-order logic. In A. Ahmed, R. Findler, D. Garg, and F. Pottier, editors, Principles of Programming Languages, pages 1214–1245. ACM, 2023

    2023

  23. [23]

    F. Rabe. Semantics for Dependently-Typed HOL. In A. Biere, C. Lutz, and S. Negri, editors,Automated Reasoning. Springer, 2026. to appear

    2026

  24. [24]

    doi: 10.1007/978-3-642-39634-2\_14.https://inria.hal.science/hal-00816699

    Vincent Rahli, Mark Bickford, and Abhishek Anand. Formal program optimization in Nuprl using computational equivalence and partial types. In Sandrine Blazy, ChristinePaulin-Mohring,and David Pichardie, editors,Interactive Theorem Prov- ing - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 ofLecture Notes ...

    work page doi:10.1007/978-3-642-39634-2 2013

  25. [25]

    Ranalter, C

    D. Ranalter, C. E. Brown, and C. Kaliszyk. Experiments with choice in dependently-typed higher-order logic. In Nikolaj S. Bjørner, Marijn Heule, and Andrei Voronkov, editors,LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, volume 100 ofEPiC Series in Computin...

    2024

  26. [26]

    URL:https://doi.org/10.29007/2v8h,doi:10.29007/2V8H

    work page doi:10.29007/2v8h

  27. [28]

    Riazanov and A

    A. Riazanov and A. Voronkov. The design and implementation of Vampire.AI Communications, 15:91–110, 2002

    2002

  28. [29]

    Rothgang and F

    C. Rothgang and F. Rabe. Subtyping in dependently-typed higher-order logic. In R. Thiemann and C. Weidenbach, editors,Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, volume 15979 ofLecture Notes in Computer Science, pages 98–114. Springer, 2025.doi:10.1007/978-3-0...

    work page doi:10.1007/978-3-032-04167-8 2025

  29. [30]

    Rothgang, F

    C. Rothgang, F. Rabe, and C. Benzmüller. Theorem Proving in Dependently Typed Higher-Order Logic. In B. Pientka and C. Tinelli, editors,Automated De- dution, pages 438–455. Springer, 2023

    2023

  30. [31]

    Rothgang, F

    C. Rothgang, F. Rabe, and C. Benzmüller. Dependently-Typed Higher-Order Logic.ACM Transactions on Computational Logic, 27(1), 2025

    2025

  31. [32]

    Southern.A Framework for Reasoning about LF Specifications

    M. Southern.A Framework for Reasoning about LF Specifications. PhD thesis, University of Minnesota, 2021

    2021

  32. [33]

    A. Steen. An extensible logic embedding tool for lightweight non-classical reasoning (short paper). In B. Konev, C. Schon, and A. Steen, editors,Practical Aspects of Automated Reasoning, volume 3201 ofCEUR Workshop Proceedings. CEUR- WS.org, 2022

    2022

  33. [34]

    Steen and C

    A. Steen and C. Benzmüller. The higher-order prover Leo-III. In G. De Giacomo, A. Catalá, B. Dilkina, M. Milano, S. Barro, A. Bugarín, and J. Lang, editors, European Conference on Artificial Intelligence, pages 2937–2938. IOS Press, 2020

    2020

  34. [35]

    Steen, M

    A. Steen, M. Wisniewski, and C. Benzmüller. Going polymorphic - th1 reasoning for leo-iii. In Thomas Eiter, David Sands, Geoff Sutcliffe, and Andrei Voronkov, editors,IWIL Workshop and LPAR Short Presentations, volume 1 ofKalpa Pub- lications in Computing, pages 100–112. EasyChair, 2017.doi:10.29007/jgkw

    work page doi:10.29007/jgkw 2017

  35. [36]

    default term

    P.Vukmirovic,A.Bentkamp,J.Blanchette,S.Cruanes,V.Nummelin,andS.Tour- ret. Making higher-order superposition work.J. Autom. Reason., 66(4):541– 564, 2022. URL:https://doi.org/10.1007/s10817-021-09613-z,doi:10.1007/ S10817-021-09613-Z. A Preservation Proof.Thoerem 1 is proved by straightforward induction on derivations. The sub-proofs for the individual pro...

    work page doi:10.1007/s10817-021-09613-z 2022