关于推导模重写的终止性
计算机科学中的逻辑
2016-08-16 v1
摘要
我们研究在代数构造演算（Calculus of Algebraic Constructions）中，对重写模等式集合的终止性。该演算是对构造演算（Calculus of Constructions）的一种扩展，引入了由高阶重写规则定义的函数和谓词。在先前的工作中，我们基于可计算闭包（computable closure）的概念，定义了一般语法条件，以确保重写与β归约组合的终止性。本文表明，若这些等式生成的等价类是有限的，且等式是线性的，并且满足基于可计算闭包的一般语法条件，则上述结果在考虑重写模等式的情况下仍然成立。这包括交换律和结合律等等式，并提供了对终止模等式的原创处理。
引用
@article{arxiv.cs/0610071,
title = {Rewriting modulo in Deduction modulo},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:cs/0610071},
year = {2016}
}