Higher-Order Pushdown Trees are Circularly Computable - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Higher-Order Pushdown Trees are Circularly Computable

Résumé

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.
Fichier principal
Vignette du fichier
jfla15_submission_8.pdf (337.42 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01099127 , version 1 (31-12-2014)

Identifiants

  • HAL Id : hal-01099127 , version 1

Citer

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⟩
75 Consultations
74 Téléchargements

Partager

Gmail Facebook X LinkedIn More