{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T16:18:49Z","timestamp":1781021929543,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Horizon 2020 Research and Innovation Programme","award":["101031081"],"award-info":[{"award-number":["101031081"]}]},{"name":"Horizon 2020 Research and Innovation Programme","award":["101027412"],"award-info":[{"award-number":["101027412"]}]},{"DOI":"10.13039\/501100003246","name":"Dutch Research Council","doi-asserted-by":"crossref","award":["VI.Veni.232.286"],"award-info":[{"award-number":["VI.Veni.232.286"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic programming constructs (sequencing, non-deterministic choice, and iteration) it is able to express all\n                    <jats:italic toggle=\"yes\">non-deterministic<\/jats:italic>\n                    finite state control flow over a finite set of primitives. It is natural to ask whether there exists a similar finite set of constructs that can capture all\n                    <jats:italic toggle=\"yes\">deterministic<\/jats:italic>\n                    computation. We show that this is not the case. More precisely, the deterministic fragment of KAT is not generated by\n                    <jats:italic toggle=\"yes\">any<\/jats:italic>\n                    finite set of regular control flow operations. This generalizes earlier results about the expressivity of the traditional control flow operations, i.e., sequential composition, if-then-else and while.\n                  <\/jats:p>","DOI":"10.1145\/3704861","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"718-744","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Algebras for Deterministic Computation Are Inherently Incomplete"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2538-5846","authenticated-orcid":false,"given":"Balder","family":"ten Cate","sequence":"first","affiliation":[{"name":"University of Amsterdam, Amsterdam, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[{"name":"Leiden University, Leiden, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. \u201cNetKAT: semantic foundations for networks.\u201d In: POPL 113\u2013126. doi: 10.1145\/2535838.2535862 10.1145\/2535838.2535862.","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/867190"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_3_2_5_1","unstructured":"Edward A. Ashcroft and Zohar Manna. 1972. \u201cThe translation of GOTO programs into WHILE programs.\u201d In: IFIP. Vol. 1 250\u2013255."},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Bart Bogaerts Balder ten Cate Brett McLean and Jan Van den Bussche. 2023. Preservation theorems for Tarski\u2019s relation algebra. (2023). doi: 10.48550\/ARXIV.2305.04656 10.48550\/ARXIV.2305.04656.","DOI":"10.48550\/ARXIV.2305.04656"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365646"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"issue":"7","key":"e_1_3_2_9_1","first-page":"1009","article-title":"\u201cUne approche pour r\u00e9duire la complexit\u00e9 du flot de contr\u00f4le dans les programmes C","volume":"21","author":"Cass\u00e9 Hugues","year":"2002","unstructured":"Hugues Cass\u00e9, Louis F\u00e9raud, Christine Rochange, and Pascal Sainrat. 2002. \u201cUne approche pour r\u00e9duire la complexit\u00e9 du flot de contr\u00f4le dans les programmes C.\u201d Tech. Sci. Informatiques, 21, 7, 1009\u20131032.","journal-title":"Tech. Sci. Informatiques"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.020"},{"key":"e_1_3_2_11_1","unstructured":"Ernie Cohen Dexter Kozen and Frederick Smith. July 1996. The Complexity of Kleene Algebra with Tests. Tech. rep. TR96-1598. (July 1996)."},{"key":"e_1_3_2_12_1","unstructured":"Jaco de Bakker and Lambert Meertens. 1972. Simple recursive program schemes and inductive assertions. Tech. rep. MR 142\/72. https:\/\/ir.cwi.nl\/pub\/9134."},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183285"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCL.1994.288377"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(73)80040-6"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532430"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394744"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Niels Bj\u00f8rn Bugge Grathwohl Dexter Kozen and Konstantinos Mamouras. 2014. \u201cKAT + B!\u201d In: CSL-LICS 44:1\u201344:10. doi: 10.1145\/2603088.2603095 10.1145\/2603088.2603095.","DOI":"10.1145\/2603088.2603095"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","unstructured":"Tobias Kapp\u00e9 Todd Schmid and Alexandra Silva. 2023. \u201cA Complete Inference System for Skip-free Guarded Kleene Algebra with Tests.\u201d In: ESOP 309\u2013336. doi: 10.1007\/978-3-031-30044-8_12 10.1007\/978-3-031-30044-8_12.","DOI":"10.1007\/978-3-031-30044-8_12"},{"key":"e_1_3_2_21_1","first-page":"3","article-title":"\u201cRepresentation of Events in Nerve Nets and Finite Automata","author":"Kleene Stephen C.","year":"1956","unstructured":"Stephen C. Kleene. 1956. \u201cRepresentation of Events in Nerve Nets and Finite Automata.\u201d Automata Studies, 3\u201341.","journal-title":"Automata Studies"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(71)90018-4"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80043-7"},{"key":"e_1_3_2_24_1","first-page":"117","article-title":"\u201cAutomata on Guarded Strings and Applications","volume":"24","author":"Kozen Dexter","year":"2003","unstructured":"Dexter Kozen. 2003. \u201cAutomata on Guarded Strings and Applications.\u201d Matematica Contemporanea, 24, 117\u2013139.","journal-title":"Matematica Contemporanea"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 2008. \u201cNonlocal Flow of Control and Kleene Algebra with Tests.\u201d In: LICS 105\u2013117. doi: 10.1109\/LICS.2008.32 10.1109\/LICS.2008.32.","DOI":"10.1109\/LICS.2008.32"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47843-2_15"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Maria-Christina Patron. 2000. \u201cCertification of Compiler Optimizations Using Kleene Algebra with Tests.\u201d In: CL 568\u2013582. doi: 10.1007\/3-540-44957-4_38 10.1007\/3-540-44957-4_38.","DOI":"10.1007\/3-540-44957-4_38"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Frederick Smith. 1996. \u201cKleene Algebra with Tests: Completeness and Decidability.\u201d In: Proc. Computer Science Logic (CSL) 244\u2013259. doi: 10.1007\/3-540-63172-0_43 10.1007\/3-540-63172-0_43.","DOI":"10.1007\/3-540-63172-0_43"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Wei-Lung Dustin Tseng. 2008. \u201cThe B\u00f6hm-Jacopini Theorem Is False Propositionally\u201d In: MPC 177\u2013192. doi: 10.1007\/978-3-540-70594-9_11 10.1007\/978-3-540-70594-9_11.","DOI":"10.1007\/978-3-540-70594-9_11"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90023-0"},{"key":"e_1_3_2_32_1","unstructured":"Maurice Nivat. 1972. \u201cLangages alg\u00e9briques sur le magma libre et s\u00e9mantique des sch\u00e9mas de programme.\u201d In: ICALP 293\u2013308."},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Maurice Nivat. 1974. On the interpretation of recursive program schemes. Tech. rep. doi: 10.22028\/D291-26058 10.22028\/D291-26058.","DOI":"10.22028\/D291-26058"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/355609.362337"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"Damien Pous. 2015. \u201cSymbolic Algorithms for Language Equivalence and Kleene Algebra with Tests.\u201d In: POPL 357\u2013368. doi: 10.1145\/2676726.2677007 10.1145\/2676726.2677007.","DOI":"10.1145\/2676726.2677007"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Todd Schmid Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2021. \u201cGuarded Kleene Algebra with Tests: Coequations Coinduction and Completeness.\u201d In: ICALP. Vol. 198 142:1\u2013142:14. doi: 10.4230\/LIPICS.ICALP.2021.142 10.4230\/LIPICS.ICALP.2021.142.","DOI":"10.4230\/LIPICS.ICALP.2021.142"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"Igor Sedl\u00e1r. 2023. Kleene Algebra with Dynamic Tests: Completeness and Complexity. (2023). doi: 10.48550\/ARXIV.2311.06937 10.48550\/ARXIV.2311.06937.","DOI":"10.48550\/ARXIV.2311.06937"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Nate Foster Justin Hsu Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2020. \u201cGuarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time.\u201d In: POPL 61:1\u201361:28. doi: 10.1145\/3371129 10.1145\/3371129.","DOI":"10.1145\/3371129"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Cheng Zhang Tobias Kapp\u00e9 David E. Narv\u00e1ez and Nico Naus. 2024. \u201cCF-GKAT: Efficient Validation of Control-Flow Transformations.\u201d In: POPL 21:1\u201421:27. doi: 10.1145\/3704857 10.1145\/3704857.","DOI":"10.1145\/3704857"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704861","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704861","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:53Z","timestamp":1770200213000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704861"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704861"],"URL":"https:\/\/doi.org\/10.1145\/3704861","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}