无选择计算与对称性:可定义性的局限
Choiceless Computation and Symmetry: Limitations of Definability
AI总结:
本文证明无选择多项式时间(CPT)无法在超立方体上计算具有对数大小颜色类的预序,从而表明现有CPT解决CFI问题的技术无法推广到无序输入,为分离CPT与PTIME提供了新证据。
摘要:
寻找一种能够刻画PTIME的逻辑是有限模型理论中一个长期悬而未决的问题。最具前景的候选逻辑之一便是带计数的无选择多项式时间(CPT)。抽象地说,CPT是一种同构不变的计算模型,它以遗传有限集作为数据结构。虽然很容易验证CPT语句的求值可以在多项式时间内完成,但其逆命题已经开放了20多年:有限结构的每一个PTIME可判定性质是否都能在CPT中表达?我们试图朝着否定答案的方向取得进展,并证明无选择多项式时间无法在每个超立方体中计算一个具有对数大小颜色类的预序。原因在于这样的预序具有超多项式多个自同构像,这使得CPT不可能定义它们。虽然计算这样的预序并不是一个能够立即分离P与CPT的判定问题,但它的重要性在于以下原因:所谓的蔡—菲雷尔—伊默曼(CFI)问题是逻辑的标准基准之一,也许最为人所知的是它将带计数的定点逻辑(FPC)与P分离开来。因此,很自然地将其也视为分离CPT与P的一个潜在候选。这方面已知最强的正面结果指出,如果输入结构中存在一个具有对数大小颜色类的预序,那么CPT能够解决CFI。我们的结果意味着这一方法不能被推广到无序输入。换句话说,无序超立方体上的CFI是一个PTIME问题,但可以证明它无法用最先进的无选择算法技术来处理。
英文摘要:
The search for a logic capturing PTIME is a long standing open problem in finite model theory. One of the most promising candidate logics for this is Choiceless Polynomial Time with counting (CPT). Abstractly speaking, CPT is an isomorphism-invariant computation model working with hereditarily finite sets as data structures. While it is easy to check that the evaluation of CPT-sentences is possible in polynomial time, the converse has been open for more than 20 years: Can every PTIME-decidable property of finite structures be expressed in CPT? We attempt to make progress towards a negative answer and show that Choiceless Polynomial Time cannot compute a preorder with colour classes of logarithmic size in every hypercube. The reason is that such preorders have super-polynomially many automorphic images, which makes it impossible for CPT to define them. While the computation of such a preorder is not a decision problem that would immediately separate P and CPT, it is significant for the following reason: The so-called Cai-Fürer-Immerman (CFI) problem is one of the standard benchmarks for logics and maybe best known for separating fixed-point logic with counting (FPC) from P. Hence, it is natural to consider this also a potential candidate for the separation of CPT and P. The strongest known positive result in this regard says that CPT is able to solve CFI if a preorder with logarithmically sized colour classes is present in the input structure. Our result implies that this approach cannot be generalised to unordered inputs. In other words, CFI on unordered hypercubes is a PTIME-problem which provably cannot be tackled with the state-of-the-art choiceless algorithmic techniques.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。