代数交叉类型一致性问题
摘要：代数交集类型一致化问题(AITUP)是与交集类型系统中几个自然的决定性问题相关的证明搜索中的一个重要组成部分。目前尚不清楚AITUP问题是否可判定，因此该问题仍然开放。本文通过展示AITUP问题是指数时间难解的证明给出了第一个不平凡的下界结果(主要结果)。此外，我们还证明了即使在秩1解(替换其值域被限制为包含秩1类型的情况下)，该结果仍然成立。此外，我们还为交集类型匹配问题(单向一致化)提供了一个参数困难性结果，该问题已知是NP完全的。 本文将AITUP问题置于一致化理论的背景中。交集类型的等式理论可以被表述为一个带有ACI(结合、交换和幂等)运算符(交集类型)和关于第二个运算符(函数类型)的分配性质的代数理论。尽管该问题在代数上是自然且有趣的，但它似乎在一致化理论中占据一个迄今未研究过的位置，我们对该问题的研究表明需要新的方法来理解该问题。因此，为了下界证明，我们无法从现有的ACI一致化理论中进行缩减，并使用两人对弈铺砖游戏的博弈论方法。
作者：Andrej Dudenhefner, Moritz Martens, Jakob Rehof
论文ID：1611.05672
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22