可计算性闭包：十年之后
计算机科学中的逻辑
2007-07-11 v1
摘要
可计算性闭包（computability closure）的概念由 Jean-Pierre Jouannaud 和 Mitsuhiro Okada 在 1997 年的一份草稿中引入，用于证明具有一阶匹配的高阶重写系统的终止性，该草稿后来成为作者博士论文的基础。在本文中，我们展示了该概念如何也可用于处理基于-正规化的重写（配合模-的匹配，即 Miller 模式的模式）、配合模某些等式理论的重写以及高阶数据类型（具有函数式递归参数的构造子的类型）。最后，我们展示了如何轻松地将可计算性闭包转化为一个归约序，该归约序在高阶情形下包含了 Jean-Pierre Jouannaud 和 Albert Rubio 的高阶递归路径序，而在一阶情形下则等同于通常的一阶递归路径序。
引用
@article{arxiv.0707.1372,
title = {Computability Closure: Ten Years Later},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:0707.1372},
year = {2007}
}