无穷项重写的投影
计算机科学中的逻辑
2016-09-26 v2
摘要
项重写中的证明项是归约序列，更一般地是收缩活动的一种表示方式，允许区分例如同时归约与顺序归约。有限、一阶、左线性项重写的证明项在 Terese 著作第 8 章中有所描述。在先前的工作中，我们定义了有限证明项形式体系的一个扩展，使其能够描述无穷一阶项重写中的收缩，并给出了置换等价的一个刻画。在这项工作中，我们讨论了如何使用证明项对可能无限的归约序列的投影进行建模。同样地，其基础是 Terese 第 8.7 节中描述的有限重写投影的刻画。我们将这一刻画扩展到无穷项重写，并通过精确描述结构等价在投影概念发展中所起的作用对其加以精炼。我们提出的刻画产生了一个确定的表达式，即一个证明项，它描述了一个无穷归约在另一个之上的投影。为了说明投影的工作方式，我们展示了如何通过一个（可能无限的）归约和构成其一部分的单步各自的投影，来获得它们的公共归约结果。我们通过若干例子表明，所提出的定义在超出该结果涵盖范围的情形下也能产生预期的行为。最后，我们讨论了极限概念如何在我们对无限归约投影的定义中被使用。
引用
@article{arxiv.1605.07808,
title = {Projections for infinitary rewriting},
author = {Carlos Lombardi and Alejandro Ríos and Roel de Vrijer},
journal= {arXiv preprint arXiv:1605.07808},
year = {2016}
}