License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.35
URN: urn:nbn:de:0030-drops-123577
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12357/
Go to the corresponding LIPIcs Volume Portal

Hondet, Gabriel ; Blanqui, Frédéric

The New Rewriting Engine of Dedukti (System Description)

pdf-format:
LIPIcs-FSCD-2020-35.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{hondet_et_al:LIPIcs:2020:12357,
  author =	{Gabriel Hondet and Fr{\'e}d{\'e}ric Blanqui},
  title =	{{The New Rewriting Engine of Dedukti (System Description)}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12357},
  URN =		{urn:nbn:de:0030-drops-123577},
  doi =		{10.4230/LIPIcs.FSCD.2020.35},
  annote =	{Keywords: rewriting, higher-order pattern-matching, decision trees}
}

Keywords: rewriting, higher-order pattern-matching, decision trees
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: https://github.com/deducteam/lambdapi.git

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI