Interpretation Logic: an Alternative Characterisation of Choiceless Polynomial Time

We introduce a characterisation of Choiceless Polynomial Time based on first-order interpretations. Choiceless Polynomial Time with counting (introduced by Blass, Gurevich and Shelah) succeeds to define several queries that separate other logics from PTIME (e. g. the Cai-Fürer-Immerman query) and is thus an interesting candidate for a logic capturing PTIME. Originally, Choiceless Polynomial Time has been formalised as a machine model operating on structures by means of set-theoretic operations, especially creation of hereditarily finite sets. Despite the benefits of viewing the logic as a machine model, this makes it less accessible to model theoretic techniques. Computations in Choiceless Polymomial Time primarily define new relations over hereditarily finite sets. This closely resembles the process of updating relations with first-order interpretations, which suggests a characterisation with iterated first-order interpretations. Representing Choiceless Polynomial Time on the basis of first-order logic not only allows for a more concise definition, it also permits analysis using tools of finite model theory. Moreover, our characterisation makes it easy to define natural fragments of our logic and hence of Choiceless Polynomial Time. A characterisation of these fragments may, in turn, give useful insights into the expressibility of Choiceless Polynomial Time itself. We formalise the idea of iterated first-order interpretations with appropriate polynomial time and space constraints to create Interpretation Logic, a logic that is equivalent to Choiceless Polynomial Time. The main principle of Interpretation Logic is to iterate the application of a first-order interpretation to the input structure, where the halting condition and evaluation are given in first-order logic as well. In order to obtain a representation of the extension of Choiceless Polynomial Time by the counting operation, we show that it suffices to equip our logic with an equicardinality operation, namely, the Härtig quantifier. More precisely, we show that Choiceless Polynomial Time with counting can already be simulated by the extension of Choiceless Polynomial Time by an equicardinality operator. This is possible because Choiceless Polynomial Time programs have access to operations on hereditarily finite sets and thus on finite ordinals. Our main result is the equivalence of this extension of first-order logic by the equicardinality operation and the extension of Interpretation Logic by the Härtig quantifier, where the simulation requires representation of higher-order objects in the interpreted structures as well as a correspondence between different measures of space complexity.

Authors

• Svenja Schalthöfer

Keywords

No keywords are indexed for this paper.