{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T03:49:02Z","timestamp":1649216942519},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,2,9]],"date-time":"2018-02-09T00:00:00Z","timestamp":1518134400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,6,28]]},"abstract":"\n Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing P\n time<\/jats:sc>\n . The question whether there is a logic that expresses exactly the polynomial-time computable properties of finite structures, which has been open for more than 30 years, is one of the most important and challenging problems in finite model theory.\n <\/jats:p>\n \n The strength of Choiceless Polynomial Time is its ability to perform isomorphism-invariant\n computations<\/jats:italic>\n over structures, using hereditarily finite sets as data structures. But, because of isomorphism-invariance, it is choiceless in the sense that it cannot select an arbitrary element of a set\u2014an operation that is crucial for many classical algorithms. CPT can define many interesting P\n time<\/jats:sc>\n queries, including (a certain version of) the Cai-F\u00fcrer-Immerman (CFI) query. The CFI-query is particularly interesting, because it separates fixed-point logic with counting from P\n time<\/jats:sc>\n and has since remained the main benchmark for the expressibility of logics within P\n time<\/jats:sc>\n .\n <\/jats:p>\n The CFI-construction associates with each connected graph a set of CFI-graphs that can be partitioned into exactly two isomorphism classes called odd and even CFI-graphs. The problem is to decide, given a CFI-graph, whether it is odd or even. For the case where the CFI-graphs arise from ordered graphs, Dawar, Richerby, and Rossman proved that the CFI-query is CPT-definable. However, definability of the CFI-query over general graphs remains open.<\/jats:p>\n Our first contribution generalises the result by Dawar, Richerby, and Rossman to the variant of the CFI-query derived from graphs with colour classes of logarithmic size, instead of colour class size one. Second, we consider the CFI-query over graph classes where the maximal degree is linear in the size of the graphs. For the latter, we establish CPT-definability using only sets of small, constant rank, which is known to be impossible for the general case.<\/jats:p>\n In our CFI-recognising procedures we strongly make use of the ability of CPT to create sets, rather than tuples only, and we further prove that, if CPT worked over tuples instead, then no such procedure would be definable. We introduce a notion of \u201csequencelike objects\u201d based on the structure of the graphs\u2019 symmetry groups, and we show that no CPT-program that only uses sequencelike objects can decide the CFI-query over complete graphs, which have linear maximal degree. From a broader perspective, this generalises a result by Blass, Gurevich, and van den Bussche about the power of isomorphism-invariant machine models (for polynomial time) to a setting with counting.<\/jats:p>","DOI":"10.1145\/3154456","type":"journal-article","created":{"date-parts":[[2018,2,9]],"date-time":"2018-02-09T18:54:03Z","timestamp":1518202443000},"page":"1-27","source":"Crossref","is-referenced-by-count":0,"title":["Definability of Cai-F\u00fcrer-Immerman Problems in Choiceless Polynomial Time"],"prefix":"10.1145","volume":"19","author":[{"given":"Wied","family":"Pakusa","sequence":"first","affiliation":[{"name":"Mathematical Foundations of Computer Science, RWTH Aachen University"}]},{"given":"Svenja","family":"Schalth\u00f6fer","sequence":"additional","affiliation":[{"name":"Mathematical Foundations of Computer Science, RWTH Aachen University, Aachen, Germany"}]},{"given":"Erkal","family":"Selman","sequence":"additional","affiliation":[{"name":"Logic and Theory of Discrete Systems, RWTH Aachen University, Aachen, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS\u201914)","volume":"8634","author":"Abu Zaid F."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78127-1_11"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00005-6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1190150152"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the International Workshop on Abstract State Machines. Springer, 22--33","author":"Blass A."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01305232"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90012-5"},{"key":"e_1_2_1_8_1","unstructured":"A. Dawar. 2015. The nature and power of fixed-point logic with counting. ACM SIGLOG News (2015) 8--21. 10.1145\/2728816.2728820 A. Dawar. 2015. The nature and power of fixed-point logic with counting. ACM SIGLOG News (2015) 8--21. 10.1145\/2728816.2728820"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.24"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.11.011"},{"key":"e_1_2_1_11_1","volume-title":"Fields of Logic and Computation II (LNCS)","volume":"9300","author":"Gr\u00e4del E."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.68"},{"key":"e_1_2_1_13_1","unstructured":"E. Gr\u00e4del and W. Pakusa. 2015. Rank logic is dead long live rank logic!CoRR (a conference version appeared in the Proceedings of CSL\u201915) abs\/1503.05423 (2015). E. Gr\u00e4del and W. Pakusa. 2015. Rank logic is dead long live rank logic!CoRR (a conference version appeared in the Proceedings of CSL\u201915) abs\/1503.05423 (2015)."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.11"},{"key":"e_1_2_1_15_1","volume-title":"Current Trends in Theoretical Computer Science","author":"Gurevich Y."},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"N. Immerman. 1986. Relational queries computable in polynomial time. Inf. Control 68 (1986) 86--104. 10.1016\/S0019-9958(86)80029-8 N. Immerman. 1986. Relational queries computable in polynomial time. Inf. Control 68 (1986) 86--104. 10.1016\/S0019-9958(86)80029-8","DOI":"10.1016\/S0019-9958(86)80029-8"},{"key":"e_1_2_1_17_1","unstructured":"B. Laubner. 2011. The Structure of Graphs and New Logics for the Characterization of Polynomial Time. Ph.D. Dissertation. HU Berlin. B. Laubner. 2011. The Structure of Graphs and New Logics for the Characterization of Polynomial Time. Ph.D. Dissertation. HU Berlin."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"62","author":"Pakusa W."},{"key":"e_1_2_1_19_1","volume-title":"Fields of Logic and Computation","author":"Rossman B."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3154456","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,3]],"date-time":"2021-03-03T00:41:38Z","timestamp":1614732098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3154456"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,28]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,6,28]]}},"alternative-id":["10.1145\/3154456"],"URL":"http:\/\/dx.doi.org\/10.1145\/3154456","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2018,6,28]]}}}