非置换名词性抽象句法中的约束求解
Constraint solving in non-permutative nominal abstract syntax
摘要：
名义抽象语法是一种流行的一阶技术，用于编码和推理涉及绑定器的抽象语法。它的许多应用涉及约束求解。最常用的约束求解算法在名义抽象语法是Urban-Pitts-Gabbay名义统一算法，这是良好的行为，有一个成熟的理论，并在许多情况下是适用的。然而，某些问题需要一个约束求解器，它尊重名义逻辑的等变属性，如切尼的等变统一算法。这是更强大的，但更复杂和计算困难。在本文中，我们提出了一种新的算法来解决约束的一个简单的变种，我们称之为非置换的名义抽象语法。这个约束问题有类似的复杂性等变统一，但没有许多额外的复杂性等变统一术语语言。我们证明我们的算法是正确的，特别注意终止的问题，并提出了一个明确的翻译名称等变统一问题的非置换约束。
英文摘要：
Nominal abstract syntax is a popular first-order technique for encoding, and reasoning about, abstract syntax involving binders. Many of its applications involve constraint solving. The most commonly used constraint solving algorithm over nominal abstract syntax is the Urban-Pitts-Gabbay nominal unification algorithm, which is well-behaved, has a well-developed theory and is applicable in many cases. However, certain problems require a constraint solver which respects the equivariance property of nominal logic, such as Cheney's equivariant unification algorithm. This is more powerful but is more complicated and computationally hard. In this paper we present a novel algorithm for solving constraints over a simple variant of nominal abstract syntax which we call non-permutative. This constraint problem has similar complexity to equivariant unification but without many of the additional complications of the equivariant unification term language. We prove our algorithm correct, paying particular attention to issues of termination, and present an explicit translation of name-name equivariant unification problems into non-permutative constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
