Collapsible Pushdown Automata and Recursion Schemes

Matthew Hague, Andrzej Murawski, C.-H. Luke Ong, Olivier Serre

Research output: Contribution to journalArticlepeer-review

48 Downloads (Pure)


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
Publication statusPublished - 21 Aug 2017


  • Theory
  • Rewriting
  • Lambda-Calculus
  • Automata
  • Higher-Order Recursion Schemes
  • Higher-Order (Collapsible) Pushdown Automata

Cite this