Characterising Choiceless Polynomial Time with First-Order Interpretations

Choice less 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 Choice less Polynomial Time (with and without counting) based on iterated first-order interpretations. The fundamental mechanism of Choice less 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 Härtig 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 Choice less 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 one-dimensional interpretations).