The new rewriting engine of Dedukti, with Gabriel Hondet, 15 pages, submitted.
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 rewriting rules. It therefore contains an engine for rewriting LF terms and types according to the rewriting 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 rewriting rules supported by Dedukti and the new implementation of the matching algorithm. Dedukti supports non-linear rewriting 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.