Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity

Author Frédéric Blanqui



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.24.pdf
  • Filesize: 0.74 MB
  • 14 pages

Document Identifiers

Author Details

Frédéric Blanqui
  • Université Paris-Saclay, INRIA, ENS Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 4 avenue des Sciences 91190 Gif-sur-Yvette, France

Acknowledgements

The author thanks Thiago Felicissimo for his testing and remarks on the implementation of the present work in https://github.com/Deducteam/lambdapi, Guillaume Genestier for his careful reading of a first version of this paper, Gaspard Férey for his remarks on a first version of this paper, as well as the anonymous reviewers for their suggestions.

Cite AsGet BibTex

Frédéric Blanqui. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.24

Abstract

The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for b-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • logical framework
  • type theory
  • type universes
  • rewriting

Metrics

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

References

  1. B. Accattoli and B. Barras. Environments and the complexity of abstract machines. In Proceedings of the 19th International Conference on Principles and Practice of Declarative Programming, 2017. URL: https://doi.org/10.1145/3131851.3131855.
  2. Agda sort system. URL: https://agda.readthedocs.io/en/latest/language/sort-system.html.
  3. URL: http://aprove.informatik.rwth-aachen.de/.
  4. A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. A bi-directional refinement algorithm for the calculus of (co)inductive constructions. Logical Methods in Computer Science, 8:1-49, 2012. URL: https://doi.org/10.2168/LMCS-8(1:18)2012.
  5. A. Assaf. A framework for defining computational higher-order logics. PhD thesis, École Polytechnique, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01235303/.
  6. A. Assaf, G. Dowek, J.-P. Jouannaud, and J. Liu. Encoding proofs in Dedukti: the case of Coq proofs, 2016. Presented at the First International Workshop on Hammers for Type Theories (HaTT). URL: https://hal.inria.fr/hal-01330980.
  7. H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of logic in computer science. Volume 2. Background: computational structures, pages 117-309. Oxford University Press, 1992. Google Scholar
  8. B. Barras, J.-P. Jouannaud, P.-Y. Strub, and Q. Wang. CoqMTU: a higher-order type theory with a predicative hierarchy of universes parameterized by a decidable first-order theory. In Proceedings of the 26th IEEE Symposium on Logic in Computer Science, 2011. URL: https://doi.org/10.1109/LICS.2011.37.
  9. F. Blanqui. Type safety of rewrite rules in dependent types. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.13.
  10. F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré. Some axioms for mathematics. In Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 195, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.20.
  11. F. Blanqui, T. Hardin, and P. Weis. On the implementation of construction functions for non-free concrete data types. In Proceedings of the 16th European Symposium on Programming, Lecture Notes in Computer Science 4421, 2007. 15 pages. URL: https://doi.org/10.1007/978-3-540-71316-6_8.
  12. M. Boespflug, M. Dénès, and B. Grégoire. Full reduction at full throttle. In Proceedings of the 1st International Conference on Certified Programs and Proofs, Lecture Notes in Computer Science 7086, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_26.
  13. J. Chrząszcz. Modules in Coq are and will be correct. In Proceedings of the International Workshop on Types for Proofs and Programs, Lecture Notes in Computer Science 3085, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_9.
  14. D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9.
  15. S. Eker. Fast matching in combinations of regular equational theories. In Proceedings of the 1st International Workshop on Rewriting Logic and Applications, Electronic Notes in Theoretical Computer Science 4, 1996. URL: https://doi.org/10.1016/S1571-0661(04)00035-0.
  16. S. Eker. Associative-commutative rewriting on large terms. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 2706, 2003. URL: https://doi.org/10.1007/3-540-44881-0_3.
  17. G. Férey. Higher-Order Confluence andUniverse Embedding in theLogical Framework. PhD thesis, Université Paris-Saclay, France, 2021. Google Scholar
  18. M. Fernández and J.-P. Jouannaud. Modular termination of term rewriting systems revisited. In Proceedings of the 10th International Workshop on Specification of Abstract Data Types, Lecture Notes in Computer Science 906, 1994. URL: https://doi.org/10.1007/BFb0014432.
  19. G. Genestier. Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting. PhD thesis, Université Paris-Saclay, 2020. URL: https://hal.inria.fr/tel-03167579.
  20. G. Genestier. Encoding agda programs using rewriting. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.31.
  21. B. Gramlich. Modularity in term rewriting revisited. Theoretical Computer Science, 464:3-19, 2012. URL: https://doi.org/10.1016/j.tcs.2012.09.008.
  22. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. URL: https://doi.org/10.1145/138027.138060.
  23. G. Hondet and F. Blanqui. The new rewriting engine of dedukti. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.35.
  24. D. Kapur and P. Narendran. NP-completeness of the associative-commutative unification and related problems. Unpublished Manuscript. Computer Science Branch, General Electric Corporate Research and Development, Schenectady, NY. See [D. Kapur and P. Narendran, 1987], 1986. Google Scholar
  25. D. Kapur and P. Narendran. Matching, unification and complexity. SIGSAM Bull., 21(4):6-9, 1987. URL: https://doi.org/10.1145/36330.36332.
  26. S. Krstić and S. Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(1-2):87-106, 2005. URL: https://doi.org/10.1016/j.ic.2004.11.001.
  27. C. Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253-288, 1996. URL: https://doi.org/10.1006/jsco.1996.0011.
  28. P. Martin-Löf. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Proceedings of the 1973 Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1975. URL: http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-Predicative-Part-1975.pdf.
  29. M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu Matematykow Krajow Slowcanskich, Warszawa, Poland, 1929. Google Scholar
  30. R. Saillard. Type checking in the Lambda-Pi-calculus modulo: theory and practice. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.
  31. R. Shostak. Deciding combination of theories. Journal of the ACM, 31(1):1-12, 1984. Google Scholar
  32. M. Sozeau. Polymorphic universes. URL: https://coq.inria.fr/refman/addendum/universe-polymorphism.html.
  33. M. Sozeau and N. Tabareau. Universe polymorphism in Coq. In Proceedings of the 5th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 8558, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_32.
  34. TeReSe. Term rewriting systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  35. B. Ziliani and M. Sozeau. A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Journal of Functional Programming, 27(E10), 2017. URL: https://doi.org/10.1017/S0956796817000028.
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