Dedukti 的新重写引擎
编程语言
2022-02-16 v2 符号计算
摘要
Dedukti 是 -演算模重写的一个类型检查器，它是爱丁堡逻辑框架 LF 的扩展，其中函数和类型符号可由重写规则定义。因此它包含一个根据用户所给重写规则重写 LF 项与类型的引擎。该引擎的一个关键组成部分是匹配算法，用于找出可触发的规则。在本文中，我们描述 Dedukti 所支持的重写规则类以及匹配算法的新实现。Dedukti 支持对带绑定子的项使用非线性重写规则，并如同组合归约系统（CRS）中那样使用高阶模式匹配。新的匹配算法将 Luc Maranget 在 OCaml 编译器中引入的决策树技术扩展到这一更一般的语境中。
引用
@article{arxiv.2010.16115,
title = {The New Rewriting Engine of Dedukti},
author = {Gabriel Hondet and Frédéric Blanqui},
journal= {arXiv preprint arXiv:2010.16115},
year = {2022}
}