可计算性闭包：十年后
摘要：计算闭合性的概念被引入来证明具有一阶匹配的高阶重写的终止性，这是Jean-Pierre Jouannaud和Mitsuhiro Okada在1997年的一份草案中提出的，后来作为作者的博士论文基础。在本文中，我们展示了这个概念如何在`a la Miller模式下的beta-规范重写与beta-eta匹配修正、在某个等式理论下的匹配修正重写以及高阶数据类型（具有具有功能递归参数的构造函数）处理中使用。最后，我们展示了如何将计算闭合转化为一个简单的规约序，其中在高阶情况下包含Jean-Pierre Jouannaud和Albert Rubio的高阶递归路径序，并且在一阶情况下等于通常的一阶递归路径序。
作者：Fr''ed''eric Blanqui (INRIA Lorraine - LORIA)
论文ID：0707.1372
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-07-11