Characterising Choiceless Polynomial Time with First-Order Interpretations
Abstract
—Choiceless Polynomial Time (CPT) is one of the
candidates in the quest for a logic for polynomial time. It is
a strict extension of fixed-point logic with counting, but to date
the question is open whether it expresses all polynomial-time
properties of finite structures. We present here alternative characterisations
of Choiceless Polynomial Time (with and without
counting) based on iterated first-order interpretations.
The fundamental mechanism of Choiceless Polynomial Time
is the manipulation of hereditarily finite sets over the input
structure by means of set-theoretic operations and comprehension
terms. While this is very convenient and powerful for the design
of abstract computations on structures, it makes the analysis of
the expressive power of CPT rather difficult. We aim to reduce
this functional framework operating on higher-order objects to
an approach that evaluates formulae on less complex objects.
We propose a more model-theoretic formalism, called
polynomial-time interpretation logic (PIL), that replaces the
machinery of hereditarily finite sets and comprehension terms
by traditional first-order interpretations, and handles counting
by Hartig quantifiers. In our framework, computations on finite ¨
structures are captured by iterations of interpretations, and a run
is a sequence of states, each of which is a finite structure of a
fixed vocabulary. Our main result is that PIL has precisely the
same expressive power as Choiceless Polynomial Time.
We also analyse the structure of PIL and show that many
of the logical formalisms or database languages that have been
proposed in the quest for a logic for polynomial time reappear
as fragments of PIL, obtained by restricting interpretations in
a natural way (e.g. by omitting congruences or using only onedimensional
interpretations).