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

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

Research output: Contribution to journalArticle

Published

Documents

Abstract

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
Volume18
Issue number3
DOIs
StatePublished - 21 Aug 2017

Research outputs

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

ID: 27971992