Collapsible pushdown automata and labeled recursion schemes. equivalence, safety and effective selection

Abstract : Higher-order recursion schemes are rewriting systems for simply typed terms and they are known to be equiexpressive with collapsible pushdown automata (CPDA) for generating trees. We argue that CPDA are an essential model when working with recursion schemes. First, we give a new proof of the translation of schemes into CPDA that does not appeal to game semantics. Second, we show that this translation permits to revisit the safety constraint and allows CPDA to be seen as Krivine machines. Finally, we show that CPDA permit one to prove the effective MSO selection property for schemes, subsuming all known decidability results for MSO on schemes.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-00733467
Contributor : Arnaud Carayol <>
Submitted on : Tuesday, March 8, 2016 - 9:31:56 AM
Last modification on : Friday, January 4, 2019 - 5:32:57 PM
Long-term archiving on : Sunday, November 13, 2016 - 10:02:35 AM

File

CS12.pdf
Files produced by the author(s)

Identifiers

Citation

Arnaud Carayol, Olivier Serre. Collapsible pushdown automata and labeled recursion schemes. equivalence, safety and effective selection. LICS 2012, Jun 2012, Dubrovnik, Croatia. pp.165-174, ⟨10.1109/LICS.2012.73⟩. ⟨hal-00733467⟩

Share

Metrics

Record views

273

Files downloads

243