2026-07-19T17:51:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10994 2024-03-06T10:47:00Z ddc:004 open_access

On the Expressivity of Linear Recursion Schemes Clairambault, Pierre Murawski, Andrzej S. higher-order recursion schemes linear logic game semantics geometry of interaction We investigate the expressive power of higher-order recursion schemes (HORS) restricted to linear types. Two formalisms are considered: multiplicative additive HORS (MAHORS), which feature both linear function types and products, and multiplicative HORS (MHORS), based on linear function types only. For MAHORS, we establish an equi-expressivity result with a variant of tree-stack automata. Consequently, we can show that MAHORS are strictly more expressive than first-order HORS, that they are incomparable with second-order HORS, and that the associated branch languages lie at the third level of the collapsible pushdown hierarchy. In the multiplicative case, we show that MHORS are equivalent to a special kind of pushdown automata. It follows that any MHORS can be translated to an equivalent first-order MHORS in polynomial time. Further, we show that MHORS generate regular trees and can be translated to equivalent order-0 HORS in exponential time. Consequently, MHORS turn out to have the same expressive power as 0-HORS but they can be exponentially more concise. Our results are obtained through a combination of techniques from game semantics, the geometry of interaction and automata theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pierre Clairambault and Andrzej S. Murawski 2019 Is Part Of LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2019.50 urn:nbn:de:0030-drops-109945 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.50 eng https://creativecommons.org/licenses/by/3.0/legalcode