Collapsible Pushdown Automata and Recursion Schemes. / Hague, Matthew; Ong, C.-H. Luke; Murawski, Andrzej; Serre, Olivier.

In: ACM Transactions on Computational Logic, Vol. 18, No. 3, 11.08.2017, p. 1-42.

Research output: Contribution to journalArticle




We consider recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) 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 ad infinitum, an infinite tree, called its value tree. A fundamental question is to provide an equivalent description of the trees generated by recursion schemes by a class of machines. In this paper we answer this open question by introducing collapsible pushdown automata (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. 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.
Original languageEnglish
Pages (from-to)1-42
Number of pages42
JournalACM Transactions on Computational Logic
Issue number3
StatePublished - 11 Aug 2017

Research outputs

This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 27971992