Higher-Order Pushdown Trees are Circularly Computable

Abstract : We are interested in the problem of expressiveness of the following operations in the category of sets: finite products and coproducts, initial algebras (induction) and final coalgebras (coinduction). These operations are the building blocks of a logical system that allows circularity in Gentzen-style proofs. Proofs in this system are seen as simple programs, while the cut-elimination process is viewed as a running automaton with a memory device. In this paper, we show that higher-order trees, those accepted by higher-order pushdown automata, are computable in this setting, by providing an explicit simulation of the automata by cut-elimination.
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-01099127
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:22:02 PM
Last modification on : Friday, March 9, 2018 - 11:26:03 AM
Long-term archiving on : Wednesday, April 1, 2015 - 10:11:11 AM

File

jfla15_submission_8.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01099127, version 1

Collections

Citation

Jérôme Fortier. Higher-Order Pushdown Trees are Circularly Computable. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099127⟩

Share

Metrics

Record views

106

Files downloads

73