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 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 syntax graph of the scheme, and hence paths in the tree generated...

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
• Keywords: Computer Science, LICS 2008, Order-n Cpda, Order-n Recursion Schemes, Recursion Schemes