论文标题
Dedukti的新重写引擎
The New Rewriting Engine of Dedukti
论文作者
论文摘要
Dedukti是$λ$$π$ -calculus modulo重写的类型检查器，这是爱丁堡的逻辑框架LF的扩展，其中函数和类型符号可以通过重写规则来定义。因此，它根据用户给出的重写规则为重写LF术语和类型的引擎提供。该引擎的关键组件是匹配的算法，以查找可以触发哪些规则的算法。在本文中，我们描述了Dedukti支持的重写规则类别以及匹配算法的新实现。 Dedukti支持与组合减少系统（CRS）中使用型订单模式匹配的粘合剂对术语的非线性重写规则。新的MatchingAlgorithm扩展了Luc Maranget在OcamlCompiler中引入的决策树的技术，以使其成为这种更一般的环境。
Dedukti is a type-checker for the $λ$$Π$-calculus modulo rewriting, an extension of Edinburgh's logicalframework LF where functions and type symbols can be defined by rewrite rules. It thereforecontains 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 thispaper, we describe the class of rewrite rules supported by Dedukti and the new implementation ofthe matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders usinghigher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matchingalgorithm extends the technique of decision trees introduced by Luc Maranget in the OCamlcompiler to this more general context.
