Collapsible pushdown automata and recursion schemes
Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order stack operations pushi and popi, CPDA have an important operation called collapse, whose effect...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
2008
|
| _version_ | 1797060006852427776 |
|---|---|
| author | Hague, M Murawski, A Ong, C Serre, O Soc, I |
| author_facet | Hague, M Murawski, A Ong, C Serre, O Soc, I |
| author_sort | Hague, M |
| collection | OXFORD |
| description | Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order stack operations pushi and popi, CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the topmost symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of (possibly infinite) ranked trees. In one direction, we give a simple algorithm that transforms an order-n CPDA to an order-n recursion scheme that generates the same tree, uniformly for all n ≥ 0. In the other direction, using ideas from game semantics, we give an effective transformation of order-n recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) to order-n CPDA that compute traversals over an abstract syntax graph of the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first automata-theoretic characterization of higherorder recursion schemes. Thus CPDA are also a characterization of the simply-typed lambda calculus with recursion (generated from uninterpreted lst-order symbols) and of (pure) innocent strategies. An important consequence of the equi-expressivity result is that it allows us to reduce decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. Thus we show, as a consequence of a recent result by Ong (modal mu-calculus model-checking of trees generated by recursion schemes is n-EXPTIME complete), that the problem of solving parity games over the configuration graphs of order-n CPDA is n-EXPTIME complete, subsuming several well-known results about the solvability of games over higher-order pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Another contribution of our work is a self-contained proof of the same solvability result by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of Ong's result. In contrast to higher-order pushdown graphs, we show that the monadic second-order theories of the configuration graphs of CPDA are undecidable. It follows that - as generators of graphs - CPDA are strictly more expressive than higher-order pushdown automata. © 2008 IEEE. |
| first_indexed | 2024-03-06T20:11:41Z |
| format | Conference item |
| id | oxford-uuid:2ac8c529-f65e-4db3-86b8-e562a839fb76 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:11:41Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:2ac8c529-f65e-4db3-86b8-e562a839fb762022-03-26T12:27:06ZCollapsible pushdown automata and recursion schemesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:2ac8c529-f65e-4db3-86b8-e562a839fb76Symplectic Elements at Oxford2008Hague, MMurawski, AOng, CSerre, OSoc, ICollapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order stack operations pushi and popi, CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the topmost symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of (possibly infinite) ranked trees. In one direction, we give a simple algorithm that transforms an order-n CPDA to an order-n recursion scheme that generates the same tree, uniformly for all n ≥ 0. In the other direction, using ideas from game semantics, we give an effective transformation of order-n recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) to order-n CPDA that compute traversals over an abstract syntax graph of the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first automata-theoretic characterization of higherorder recursion schemes. Thus CPDA are also a characterization of the simply-typed lambda calculus with recursion (generated from uninterpreted lst-order symbols) and of (pure) innocent strategies. An important consequence of the equi-expressivity result is that it allows us to reduce decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. Thus we show, as a consequence of a recent result by Ong (modal mu-calculus model-checking of trees generated by recursion schemes is n-EXPTIME complete), that the problem of solving parity games over the configuration graphs of order-n CPDA is n-EXPTIME complete, subsuming several well-known results about the solvability of games over higher-order pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Another contribution of our work is a self-contained proof of the same solvability result by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of Ong's result. In contrast to higher-order pushdown graphs, we show that the monadic second-order theories of the configuration graphs of CPDA are undecidable. It follows that - as generators of graphs - CPDA are strictly more expressive than higher-order pushdown automata. © 2008 IEEE. |
| spellingShingle | Hague, M Murawski, A Ong, C Serre, O Soc, I Collapsible pushdown automata and recursion schemes |
| title | Collapsible pushdown automata and recursion schemes |
| title_full | Collapsible pushdown automata and recursion schemes |
| title_fullStr | Collapsible pushdown automata and recursion schemes |
| title_full_unstemmed | Collapsible pushdown automata and recursion schemes |
| title_short | Collapsible pushdown automata and recursion schemes |
| title_sort | collapsible pushdown automata and recursion schemes |
| work_keys_str_mv | AT haguem collapsiblepushdownautomataandrecursionschemes AT murawskia collapsiblepushdownautomataandrecursionschemes AT ongc collapsiblepushdownautomataandrecursionschemes AT serreo collapsiblepushdownautomataandrecursionschemes AT soci collapsiblepushdownautomataandrecursionschemes |