Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Choiceless Computation and Symmetry: Limitations of Definability

Benedikt Pago

TL;DR

The paper investigates whether Choiceless Polynomial Time (CPT) can capture PTIME by studying the definability of preorders in hypercubes. It develops an orbit-size framework for hereditarily finite objects under hypercube automorphisms and uses supporting partitions to bound stabilizers, proving a Super-Polynomial Orbit Theorem for preorders with colour classes of size $O(n)$; consequently, CPT cannot define such preorders in every hypercube. This yields a principled barrier to solving the Cai-Fürer-Immerman (CFI) problem in CPT for unordered inputs, since existing CPT techniques relying on such preorders cannot generalize. The results suggest that entirely new choiceless algorithmic ideas or data-structures beyond HF sets are needed to separate CPT from PTIME on unordered inputs, and they contribute to a deeper understanding of CPT’s limitations and the landscape of PTIME-definable properties.

Abstract

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.

Choiceless Computation and Symmetry: Limitations of Definability

TL;DR

The paper investigates whether Choiceless Polynomial Time (CPT) can capture PTIME by studying the definability of preorders in hypercubes. It develops an orbit-size framework for hereditarily finite objects under hypercube automorphisms and uses supporting partitions to bound stabilizers, proving a Super-Polynomial Orbit Theorem for preorders with colour classes of size ; consequently, CPT cannot define such preorders in every hypercube. This yields a principled barrier to solving the Cai-Fürer-Immerman (CFI) problem in CPT for unordered inputs, since existing CPT techniques relying on such preorders cannot generalize. The results suggest that entirely new choiceless algorithmic ideas or data-structures beyond HF sets are needed to separate CPT from PTIME on unordered inputs, and they contribute to a deeper understanding of CPT’s limitations and the landscape of PTIME-definable properties.

Abstract

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.
Paper Structure (9 sections, 27 theorems, 20 equations, 3 figures)

This paper contains 9 sections, 27 theorems, 20 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Choiceless computation and the undefinability of preorders
  3. Previous work and the significance of undefinable preorders
  4. Analysing orbits of hereditarily finite objects over hypercubes
  5. Approximating permutation groups with supporting partitions
  6. The Super-Polynomial Orbit Theorem
  7. The case of sublinearly bounded supports
  8. The case of linearly-sized supports
  9. Concluding remarks and future research

Key Result

Theorem 2

Let $(H_n)_{n \in \mathbb N}$ be the family of $n$-dimensional hypercubes. For each $n \in \mathbb N$, fix an ordered partition ${\cal P}_n = (C_1,...,C_{m_n})$ of $\{0,1\}^n$ such that each part $C_i$ has size at most ${\cal O}(n) = {\cal O}(\log |H_n|)$. Let $x_n$ be any symmetric (w.r.t. $H_n$) h

Figures (3)

  • Figure 1: Suppose $\overline{\sigma}$ is the identity permutation in both $\mathbf{SP}(A_1)$ and $\mathbf{SP}(A_2)$. Then any $\pi \in {\mathbf{Sym}}_n$ realising $\overline{\sigma}$ must stabilise each of the three parts of $\mathbf{SP}(A_1) \sqcap \mathbf{SP}(A_2)$ setwise.
  • Figure 3: An example with $A = \{a_1,a_2,a_3\} \subseteq B$ and a mapping $p$ that specifies an image for each string in $A$. Every $\sigma \in {\mathbf{Sym}}(B)$ that acts as the inverse of $p$ on $A$ can only be realised by a $\pi \in {\mathbf{Sym}}_n$ that complies with $Q_p$.
  • Figure 4: The set $A_n \subseteq B_n$ is chosen such that on the large parts of $\bigsqcap A_n$ in $S_n$ (the green area), every $b \in B_n \setminus A_n$ is constant/imbalanced. Elsewhere, $b$ may be arbitrary.

Theorems & Definitions (32)

  • Definition 1
  • Theorem 2
  • Corollary 3
  • Theorem 4: pakusa2018definability
  • Proposition 5: Orbit-Stabiliser
  • Proposition 6
  • Definition 7
  • Definition 8: Supporting Partition, anderson2017symmetric
  • Definition 9: anderson2017symmetric
  • Lemma 10: anderson2017symmetric
  • ...and 22 more