Projects per year
Abstract
We consider recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) and use them as generators of (possibly inﬁnite) ranked trees. A recursion scheme is essentially a ﬁnite typed deterministic term rewriting system that generates, when one applies the rewriting rules ad infinitum, an inﬁnite 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 (higherorder) 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 inﬁnite tree which is ﬁnally 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, higherorder recursion schemes and collapsible pushdown automata, are equiexpressive for generating inﬁnite ranked trees. This is achieved by giving eﬀective transformations in both directions.
Original language  English 

Pages (fromto)  142 
Number of pages  42 
Journal  ACM Transactions on Computational Logic 
Volume  18 
Issue number  3 
DOIs  
Publication status  Published  21 Aug 2017 
Keywords
 Theory
 Rewriting
 LambdaCalculus
 Automata
 HigherOrder Recursion Schemes
 HigherOrder (Collapsible) Pushdown Automata
Projects
 1 Finished

Verification of Concurrent and HigherOrder Recursive Programs
Hague, M. (PI)
Eng & Phys Sci Res Council EPSRC
1/05/13 → 30/04/18
Project: Research