（HO）RPO重访
摘要：计算关闭的概念被引入用于证明高阶重写和β-规约的终止性，并用于加强高阶递归路径排序。在本文中，我们更详细地研究了计算关闭与（高阶）递归路径排序之间的关系。我们证明了一阶递归路径排序等于从计算闭包自然定义的排序。在高阶情况下，我们得到一个包含高阶递归路径排序的排序，其良序性依赖于计算关闭的正确性。这为将高阶递归路径排序扩展到更丰富的类型系统提供了一种简单的方法。
作者：Fr''ed''eric Blanqui (INRIA Lorraine - LORIA)
论文ID：cs/0609037
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23