文章基本信息

标题：On the Expressivity of Linear Recursion Schemes
本地全文：下载
作者：Pierre Clairambault ; Andrzej S. Murawski
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：138
页码：1-14
DOI：10.4230/LIPIcs.MFCS.2019.50
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：higher-order recursion schemes; linear logic; game semantics; geometry of interaction