关于名词句法和排列不动点的研究
摘要：一种基于原始固定点约束概念的名义术语alpha等价关系的新公理化方法的提出。我们证明了原来的原子和术语之间的标准新鲜关系可以从更原始的置换固定点概念派生出来，并利用这一结果来证明新的α-等价公理化的正确性。这导致了一种新的名义一致性概念，其中一致性问题的解是一个固定点上下文和一个替换的对。尽管它可能似乎不像基于新鲜约束的标准名义一致者那样自然，但是基于固定点约束的一致者概念在考虑等式理论时表现得更好：例如，在存在可交换性的情况下，名义一致性仍然是有限的，而使用新鲜上下文表示的一致性变成了无限。我们提供了关键点等价的定义，这个定义考虑了A、C和AC理论。基于这个等价的概念，我们证明了C一致性是有限的，并提供了一个完整和完备的C一致性算法，作为名义一致性关于AC和其他具有置换属性的等式理论发展的第一步。
作者：Mauricio Ayala-Rinc''on, Maribel Fern''andez and Daniele Nantes-Sobrinho
论文ID：1902.08345
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22