{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:16Z","timestamp":1767929476846,"version":"3.49.0"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,7,31]],"date-time":"2017-07-31T00:00:00Z","timestamp":1501459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/C539753\/1, EP\/K009907\/1 and EP\/M023974\/1"],"award-info":[{"award-number":["EP\/C539753\/1, EP\/K009907\/1 and EP\/M023974\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,7,31]]},"abstract":"<jats:p>\n            We consider recursion schemes (not assumed to be\n            <jats:italic>homogeneously typed<\/jats:italic>\n            , and hence not necessarily\n            <jats:italic>safe<\/jats:italic>\n            ) and use them as generators of (possibly infinite) ranked trees. A recursion scheme is essentially a finite typed deterministic term rewriting system that generates, when one applies the rewriting rules\n            <jats:italic>ad infinitum<\/jats:italic>\n            , an infinite tree, called its\n            <jats:italic>value tree<\/jats:italic>\n            . A fundamental question is to provide an equivalent description of the trees generated by recursion schemes by a class of machines.\n          <\/jats:p>\n          <jats:p>\n            In this article, we answer this open question by introducing\n            <jats:italic>collapsible pushdown automata<\/jats:italic>\n            (CPDA), which are an extension of deterministic (higher-order) pushdown automata. A CPDA generates a tree as follows. One considers its transition graph, unfolds it, and contracts its silent transitions, which leads to an infinite tree, which is finally node labelled thanks to a map from the set of control states of the CPDA to a ranked alphabet.\n          <\/jats:p>\n          <jats:p>Our contribution is to prove that these two models, higher-order recursion schemes and collapsible pushdown automata, are equi-expressive for generating infinite ranked trees. This is achieved by giving effective transformations in both directions.<\/jats:p>","DOI":"10.1145\/3091122","type":"journal-article","created":{"date-parts":[[2017,8,14]],"date-time":"2017-08-14T12:24:33Z","timestamp":1502713473000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Collapsible Pushdown Automata and Recursion Schemes"],"prefix":"10.1145","volume":"18","author":[{"given":"Matthew","family":"Hague","sequence":"first","affiliation":[{"name":"Royal Holloway, University of London, Egham, United Kingdom"}]},{"given":"Andrzej S.","family":"Murawski","sequence":"additional","affiliation":[{"name":"DIMAP and Department of Computer Science, University of Warwick, Coventry, United Kingdom"}]},{"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5936-240X","authenticated-orcid":false,"given":"Olivier","family":"Serre","sequence":"additional","affiliation":[{"name":"IRIF, CNRS &amp; Universit\u00e9 Paris Diderot -- Paris 7, Paris cedex 13, France"}]}],"member":"320","published-online":{"date-parts":[[2017,8,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_31"},{"key":"e_1_2_1_4_1","volume-title":"Rudiments of -Calculus. Studies in Logic and the Foundations of Mathematics","author":"Arnold Andr\u00e9","unstructured":"Andr\u00e9 Arnold and Damian Niwi\u0144ski . 2001. Rudiments of -Calculus. Studies in Logic and the Foundations of Mathematics , Vol. 146 . Elsevier . Andr\u00e9 Arnold and Damian Niwi\u0144ski. 2001. Rudiments of -Calculus. Studies in Logic and the Foundations of Mathematics, Vol. 146. Elsevier."},{"key":"e_1_2_1_5_1","volume-title":"Automata-Based Presentations of Infinite Structures","author":"B\u00e1r\u00e1ny Vince","unstructured":"Vince B\u00e1r\u00e1ny , Erich Gr\u00e4del , and Sasha Rubin . 2011. Automata-Based Presentations of Infinite Structures . London Mathematical Society Lecture Notes Series, Vol . 379. Cambridge University Press , 1--76. Vince B\u00e1r\u00e1ny, Erich Gr\u00e4del, and Sasha Rubin. 2011. Automata-Based Presentations of Infinite Structures. London Mathematical Society Lecture Notes Series, Vol. 379. Cambridge University Press, 1--76."},{"key":"e_1_2_1_6_1","volume-title":"Type homogeneity is not a restriction for safe recursion schemes. CoRR abs\/1701.02118","author":"Blum William","year":"2017","unstructured":"William Blum . 2017. Type homogeneity is not a restriction for safe recursion schemes. CoRR abs\/1701.02118 ( 2017 ). https:\/\/arxiv.org\/abs\/1701.02118 William Blum. 2017. Type homogeneity is not a restriction for safe recursion schemes. CoRR abs\/1701.02118 (2017). https:\/\/arxiv.org\/abs\/1701.02118"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(1:3)2009"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.40"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of Computer Science Logic (CSL\u201913)","volume":"23","author":"Broadbent Christopher","year":"2013","unstructured":"Christopher Broadbent and Naoki Kobayashi . 2013 . Saturation-based model checking of higher-order recursion schemes . In Proceedings of Computer Science Logic (CSL\u201913) 27th Annual Conference of the EACSL (LIPIcs\u201913) , Vol. 23 . Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, 129--148. Christopher Broadbent and Naoki Kobayashi. 2013. Saturation-based model checking of higher-order recursion schemes. In Proceedings of Computer Science Logic (CSL\u201913) 27th Annual Conference of the EACSL (LIPIcs\u201913), Vol. 23. Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, 129--148."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_18"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500589"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_45"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.41"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24597-1_10"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45687-2_13"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90008-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90039-7"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00049-3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_53"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08138-0_5"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08342-1_13"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90009-3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80016-X"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(77)80034-2"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90051-X"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5117\/9789053565766"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(73)80040-6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS&rsquo;\u201913)","volume":"24","author":"Hague Matthew","year":"2013","unstructured":"Matthew Hague . 2013 . Saturation of concurrent collapsible pushdown systems . In Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS&rsquo;\u201913) (LIPIcs\u201913), Vol. 24 . Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, 313--325. Matthew Hague. 2013. Saturation of concurrent collapsible pushdown systems. In Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS&rsquo;\u201913) (LIPIcs\u201913), Vol. 24. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, 313--325."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.34"},{"key":"e_1_2_1_35_1","first-page":"285","article-title":"On full abstraction for PCF: i. models, observables and the full abstraction problem, ii. dialogue games and innocent strategies, iii. A fully abstract and universal game model. Info","volume":"163","author":"Martin J.","year":"2000","unstructured":"J. Martin , E. Hyland , and C.-H. Luke Ong . 2000 . On full abstraction for PCF: i. models, observables and the full abstraction problem, ii. dialogue games and innocent strategies, iii. A fully abstract and universal game model. Info . Comput. 163 (2000), 285 -- 408 . J. Martin, E. Hyland, and C.-H. Luke Ong. 2000. On full abstraction for PCF: i. models, observables and the full abstraction problem, ii. dialogue games and innocent strategies, iii. A fully abstract and universal game model. Info. Comput. 163 (2000), 285--408.","journal-title":"Comput."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07854-1_198"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings 26th Symposium on Theoretical Aspects of Computer Science (STACS\u201910)","volume":"5","author":"Kartzow Alexander","year":"2010","unstructured":"Alexander Kartzow . 2010 . Collapsible pushdown graphs of level 2 are tree-automatic . In Proceedings 26th Symposium on Theoretical Aspects of Computer Science (STACS\u201910) (LIPIcs\u201910), Vol. 5 . Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 501--512. Alexander Kartzow. 2010. Collapsible pushdown graphs of level 2 are tree-automatic. In Proceedings 26th Symposium on Theoretical Aspects of Computer Science (STACS\u201910) (LIPIcs\u201910), Vol. 5. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 501--512."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32589-2_50"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_21"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_15"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_117"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599415"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480933"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_18"},{"key":"e_1_2_1_45_1","unstructured":"Naoki Kobayashi. 2012. GTRecS2: A Model Checker for Recursion Schemes Based on Games and Types. A tool available at http:\/\/www-kb.is.s.u-tokyo.ac.jp\/&sim;koba\/gtrecs2\/. (2012).  Naoki Kobayashi. 2012. GTRecS2: A Model Checker for Recursion Schemes Based on Games and Types. A tool available at http:\/\/www-kb.is.s.u-tokyo.ac.jp\/&sim;koba\/gtrecs2\/. (2012)."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_2_1_48_1","first-page":"1170","article-title":"The hierarchy of indexed languages of an arbitrary level","volume":"15","author":"Maslov A. N.","year":"1974","unstructured":"A. N. Maslov . 1974 . The hierarchy of indexed languages of an arbitrary level . Soviet Math. Doklady 15 (1974), 1170 -- 1174 . A. N. Maslov. 1974. The hierarchy of indexed languages of an arbitrary level. Soviet Math. Doklady 15 (1974), 1170--1174.","journal-title":"Soviet Math. Doklady"},{"key":"e_1_2_1_49_1","first-page":"38","article-title":"Multilevel stack automata. Probl","volume":"12","author":"Maslov A. N.","year":"1976","unstructured":"A. N. Maslov . 1976 . Multilevel stack automata. Probl . Info. Trans.n 12 (1976), 38 -- 43 . A. N. Maslov. 1976. Multilevel stack automata. Probl. Info. Trans.n 12 (1976), 38--43.","journal-title":"Info. Trans.n"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364578"},{"key":"e_1_2_1_52_1","unstructured":"Maurice Nivat. 1972. On the interpretation of recursive program schemes. In Symposia Mathematica.  Maurice Nivat. 1972. On the interpretation of recursive program schemes. In Symposia Mathematica."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS\u201906)","author":"Luke Ong C.-H.","year":"2006","unstructured":"C.-H. Luke Ong . 2006 a. On model-checking trees generated by higher-order recursion schemes . In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS\u201906) . IEEE Computer Society, 81--90. C.-H. Luke Ong. 2006a. On model-checking trees generated by higher-order recursion schemes. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS\u201906). IEEE Computer Society, 81--90."},{"key":"e_1_2_1_54_1","unstructured":"C.-H. Luke Ong. 2006b. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. (2006). Preprint.  C.-H. Luke Ong. 2006b. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. (2006). Preprint."},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the 30th Annual IEEE Symposium on Logic in Computer Science (LICS","author":"Luke Ong C.-H.","year":"2015","unstructured":"C.-H. Luke Ong . 2015 a. Higher-order model checking: An overview . In Proceedings of the 30th Annual IEEE Symposium on Logic in Computer Science (LICS 2015). IEEE Computer Society, 1--15. C.-H. Luke Ong. 2015a. Higher-order model checking: An overview. In Proceedings of the 30th Annual IEEE Symposium on Logic in Computer Science (LICS 2015). IEEE Computer Society, 1--15."},{"key":"e_1_2_1_56_1","volume-title":"Normalisation by traversals. CoRR abs\/1511.02629","author":"Luke Ong C.-H.","year":"2015","unstructured":"C.-H. Luke Ong . 2015b. Normalisation by traversals. CoRR abs\/1511.02629 ( 2015 ). Retrieved from http:\/\/arxiv.org\/abs\/1511.02629 C.-H. Luke Ong. 2015b. Normalisation by traversals. CoRR abs\/1511.02629 (2015). Retrieved from http:\/\/arxiv.org\/abs\/1511.02629"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings 28th Symposium on Theoretical Aspects of Computer Science (STACS\u201911)","volume":"9","author":"Parys Pawe\u0142","year":"2011","unstructured":"Pawe\u0142 Parys . 2011 . Collapse operation increases expressive power of deterministic higher order pushdown automata . In Proceedings 28th Symposium on Theoretical Aspects of Computer Science (STACS\u201911) (LIPIcs\u201911), Vol. 9 . Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 603--614. Pawe\u0142 Parys. 2011. Collapse operation increases expressive power of deterministic higher order pushdown automata. In Proceedings 28th Symposium on Theoretical Aspects of Computer Science (STACS\u201911) (LIPIcs\u201911), Vol. 9. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 603--614."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.62"},{"key":"e_1_2_1_59_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin Michael","year":"1969","unstructured":"Michael Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Trans. Amer. Math. Soc. 141 (1969), 1 -- 35 . Michael Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1--35.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535873"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_12"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_2"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.012"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000590"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63165-8_221"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00027-0"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_10"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(3:2)2009"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_19"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_35"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3091122","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3091122","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:37:28Z","timestamp":1750217848000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3091122"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,31]]},"references-count":69,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7,31]]}},"alternative-id":["10.1145\/3091122"],"URL":"https:\/\/doi.org\/10.1145\/3091122","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,31]]},"assertion":[{"value":"2016-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-08-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}