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 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 language | English |
---|---|
Pages (from-to) | 1-42 |
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
- Lambda-Calculus
- Automata
- Higher-Order Recursion Schemes
- Higher-Order (Collapsible) Pushdown Automata
Projects
- 1 Finished
-
Verification of Concurrent and Higher-Order Recursive Programs
Eng & Phys Sci Res Council EPSRC
1/05/13 → 30/04/18
Project: Research