Document Open Access Logo

A Shallow Embedding of Pure Type Systems into First-Order Logic

Author Lukasz Czajka

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2016.9.pdf
  • Filesize: 0.56 MB
  • 39 pages

Document Identifiers

Subject Classification

Keywords
  • pure type systems
  • first-order logic
  • hammers
  • proof automation
  • dependent type theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We define a shallow embedding of logical proof-irrelevant Pure Type Systems (piPTSs) into minimal first-order logic. In logical piPTSs a distinguished sort *^p of propositions is assumed. Given a context Gamma and a Gamma-proposition tau, i.e., a term tau such that Gamma |- tau : *^p, the embedding translates tau and Gamma into a first-order formula F_Gamma(tau) and a set of first-order axioms Delta_Gamma. The embedding is not complete in general, but it is strong enough to correctly translate most of piPTS propositions (by completeness we mean that if Gamma |- M : tau is derivable in the piPTS then F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma). We show the embedding to be sound, i.e., if F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma, then Gamma |- M : tau is derivable in the original system for some term M. The interest in the proposed embedding stems from the fact that it forms a basis of the translations used in the recently developed CoqHammer automation tool for dependent type theory.

Cite As Get BibTex

Lukasz Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 9:1-9:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2016.9

Author Details

Lukasz Czajka

References

  1. A. Aguirre. Towards a provably correct encoding from F^* to SMT. Technical report, INRIA, 2016. Google Scholar
  2. H. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, volume 2, pages 118-310. Oxford University Press, 1992. Google Scholar
  3. H. Barendregt, M. Bunder, and W. Dekkers. Systems of illative combinatory logic complete for first-order propositional and predicate calculus. J. Symb. Logic, 58(3):769-788, 1993. Google Scholar
  4. B. Barras and B. Grégoire. On the role of type decorations in the calculus of inductive constructions. In CSL 2005, pages 151-166, 2005. Google Scholar
  5. G. Barthe. The relevance of proof-irrelevance. In ICALP'98, pages 755-768, 1998. Google Scholar
  6. G. Barthe, J. Hatcliff, and M.H. Sørensen. A notion of classical pure type system. Electr. Notes Theor. Comput. Sci., 6:4-59, 1997. Google Scholar
  7. G. Barthe and M.H. Sørensen. Domain-free pure type systems. J. Funct. Program., 10(5):417-452, 2000. Google Scholar
  8. J. Blanchette, S. Böhme, A. Popescu, and N. Smallbone. Encoding monomorphic and polymorphic types. Logical Methods in Computer Science, 12(4), 2016. Google Scholar
  9. J. Blanchette, C. Kaliszyk, L. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101-148, 2016. Google Scholar
  10. M. Bunder and W. Dekkers. Pure type systems with more liberal rules. J. Symb. Logic, 66(4):1561-1580, 2001. Google Scholar
  11. K. Claessen, A. Lillieström, and N. Smallbone. Sort it out with monotonicity. In CADE 2011, pages 207-221. Springer, 2011. Google Scholar
  12. T. Coquand and H. Herbelin. A-translation and looping combinators in pure type systems. J. Funct. Program., 4(1):77-88, 1994. Google Scholar
  13. Ł. Czajka. Higher-order illative combinatory logic. J. Symb. Logic, 73(3):837-872, 2013. Google Scholar
  14. Ł. Czajka and C. Kaliszyk. Goal translation for a hammer for Coq (extended abstract). In HaTT 2016, volume 210 of EPTCS, pages 13-20, 2016. Google Scholar
  15. Ł. Czajka and C. Kaliszyk. Hammer for Coq: Automation for dependent type theory. J. Autom. Reasoning, 61(1-4):423-453, 2018. Google Scholar
  16. A. Felty. Encoding the calculus of constructions in a higher-order logic. In LICS '93, pages 233-244, 1993. Google Scholar
  17. A. Felty and D. Miller. Encoding a dependent-type lambda-calculus in a logic programming language. In CADE '90, pages 221-235, 1990. Google Scholar
  18. H. Geuvers. Logics and Type Systems. PhD thesis, University of Nijmegen, 1993. Google Scholar
  19. H. Geuvers and E. Barendsen. Some logical and syntactical observations concerning the first-order dependent type system lambda-P. Mathematical Structures in Computer Science, 9(4):335-359, 1999. Google Scholar
  20. H. Geuvers and M.-J. Nederhof. Modular proof of strong normalization for the Calculus of Constructions. J. Funct. Program., 1(2):155-189, 1991. Google Scholar
  21. B. Jacobs and T. Melham. Translating dependent type theory into higher order logic. In TLCA '93, pages 209-229, 1993. Google Scholar
  22. L. Kovács and A. Voronkov. First-order theorem proving and Vampire. In CAV 2013, pages 1-35, 2013. Google Scholar
  23. A. Miquel. The implicit calculus of constructions. In TLCA 2001, pages 344-359, 2001. Google Scholar
  24. A. Miquel and B. Werner. The not so simple proof-irrelevant model of CC. In TYPES 2002, volume 2646 of LNCS. Springer, 2003. Google Scholar
  25. S. Schulz. System description: E 1.8. In LPAR 2013, pages 735-743, 2013. Google Scholar
  26. Z. Snow, D. Baelde, and G. Nadathur. A meta-programming approach to realizing dependently typed logic programming. In PPDP '10, pages 187-198, 2010. Google Scholar
  27. K. Sojakova and F. Rabe. Translating a dependently-typed logic to first-order logic. In WADT 2008, pages 326-341, 2008. Google Scholar
  28. M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. Google Scholar
  29. T. Tammet and J.M. Smith. Optimized encodings of fragments of type theory in first order logic. In TYPES '95, pages 265-287, 1995. Google Scholar
  30. B. Werner. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, 4(3:13):1-20, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact