Document Open Access Logo

The New Rewriting Engine of Dedukti (System Description)

Authors Gabriel Hondet, Frédéric Blanqui



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.35.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Gabriel Hondet
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, Laboratoire Spécification et Vérification, Gif-sur-Yvette, France
Frédéric Blanqui
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, Laboratoire Spécification et Vérification, Gif-sur-Yvette, France

Acknowledgements

The authors thank Bruno Barras and Rodolphe Lepigre for their help in developing the new rewriting engine of Dedukti.

Cite AsGet BibTex

Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 35:1-35:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.35

Abstract

Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an extension of Edinburgh’s logical framework LF where functions and type symbols can be defined by rewrite rules. It therefore contains an engine for rewriting LF terms and types according to the rewrite rules given by the user. A key component of this engine is the matching algorithm to find which rules can be fired. In this paper, we describe the class of rewrite rules supported by Dedukti and the new implementation of the matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders using higher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matching algorithm extends the technique of decision trees introduced by Luc Maranget in the OCaml compiler to this more general context.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Operational semantics
Keywords
  • rewriting
  • higher-order pattern-matching
  • decision trees

Metrics

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

References

  1. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. http://lsv.fr/~dowek/Publi/expressing.pdf, 2019. Draft. URL: http://lsv.fr/~dowek/Publi/expressing.pdf.
  2. F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  3. 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
  4. R. Cauderlier. http://doi.org/10.1007/978-3-319-94821-8_9. In Proceedings of the 9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, 2018. URL: http://doi.org/10.1007/978-3-319-94821-8_9.
  5. Francisco Durán and Hubert Garavel. The rewrite engines competitions: A rectrospective. In TACAS, 2019. Google Scholar
  6. Satoshi Egi. Egison: Non-linear pattern-matching against non-free data types. ArXiv, abs/1506.04498, 2015. Google Scholar
  7. Satoshi Egi and Yuichi Nishiwaki. Non-linear pattern matching with backtracking for non-free data types. ArXiv, abs/1808.10603, 2018. Google Scholar
  8. S. Eker. Fast matching in combinations of regular equational theories. Electronic Notes in Theoretical Computer Science, 4:90-109, 1996. RWLW96, First International Workshop on Rewriting Logic and its Applications. URL: https://doi.org/10.1016/S1571-0661(04)00035-0.
  9. R. Harper, F. Honsell, and G. Plotkin. http://doi.org/10.1145/138027.138060. Journal of the ACM, 40(1):143-184, 1993. URL: http://doi.org/10.1145/138027.138060.
  10. G. Hondet. https://hal.inria.fr/hal-02317471. Master’s thesis, ENAC and Université Paul Sabatier, 2019. URL: https://hal.inria.fr/hal-02317471.
  11. J. W. Klop, V. van Oostrom, and F. van Raamsdonk. http://doi.org/10.1016/0304-3975(93)90091-7. Theoretical Computer Science, 121:279-308, 1993. URL: http://doi.org/10.1016/0304-3975(93)90091-7.
  12. R. Lepigre and C. Raffalli. http://doi.org/10.4204/EPTCS.274.4. In Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Electronic Proceedings in Theoretical Computer Science 274, 2018. URL: http://doi.org/10.4204/EPTCS.274.4.
  13. T. Libal and D. Miller. http://doi.org/10.4230/LIPIcs.FSCD.2016.26. In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 52, 2016. URL: http://doi.org/10.4230/LIPIcs.FSCD.2016.26.
  14. L. Maranget. http://doi.org/10.1145/1411304.1411311. In Proceedings of the ACM SIGPLAN Workshop on ML, 2008. URL: http://doi.org/10.1145/1411304.1411311.
  15. D. Miller. http://doi.org/10.1093/logcom/1.4.497. Journal of Logic and Computation, 1(4):497-536, 1991. URL: http://doi.org/10.1093/logcom/1.4.497.
  16. Kristoffer H. Rose. CRSX - Combinatory Reduction Systems with Extensions. In Manfred Schmidt-Schauß, editor, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), volume 10 of Leibniz International Proceedings in Informatics (LIPIcs), pages 81-90, Dagstuhl, Germany, 2011. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.RTA.2011.81.
  17. R. Saillard. https://pastel.archives-ouvertes.fr/tel-01299180. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.
  18. F. Thiré. http://doi.org/10.4204/EPTCS.274.5. In Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Electronic Proceedings in Theoretical Computer Science 274, 2018. URL: http://doi.org/10.4204/EPTCS.274.5.
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