LIPIcs.FSCD.2020.35.pdf
- Filesize: 0.51 MB
- 16 pages
Document
The New Rewriting Engine of Dedukti (System Description)
Authors
Frédéric Blanqui 
-
Part of:
Volume:
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-06-28
File
Document Identifiers
Author Details
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
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)
0PDF Downloads
References
- 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.
-
F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998.
-
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.
- 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.
-
Francisco Durán and Hubert Garavel. The rewrite engines competitions: A rectrospective. In TACAS, 2019.
-
Satoshi Egi. Egison: Non-linear pattern-matching against non-free data types. ArXiv, abs/1506.04498, 2015.
-
Satoshi Egi and Yuichi Nishiwaki. Non-linear pattern matching with backtracking for non-free data types. ArXiv, abs/1808.10603, 2018.
- 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.
- 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.
- G. Hondet. https://hal.inria.fr/hal-02317471. Master’s thesis, ENAC and Université Paul Sabatier, 2019. URL: https://hal.inria.fr/hal-02317471.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- R. Saillard. https://pastel.archives-ouvertes.fr/tel-01299180. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.
- 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.