On the Expressivity of Linear Recursion Schemes
On the Expressivity of Linear Recursion Schemes
复制标题
论线性递归方案的表现力
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
A. Murawski
中科院分区：
文献类型：
--
作者：
P. Clairambault;A. Murawski
我们调查的表达能力的高阶递归计划（HORS）限制线性类型。两个形式主义被认为是：乘法加性HORS（MAHORS），其具有线性函数类型和乘积，以及乘法HORS（MHORS），仅基于线性函数类型。对于MAHORS，我们建立了一个等价的表现力的结果与树栈自动机的变体。因此，我们可以证明MAHORS严格地比一阶HORS更有表达力，它们与二阶HORS是不可比拟的，并且相关的分支语言位于可折叠下推层次结构的第三层。在乘法的情况下，我们证明了MHORS等价于一种特殊的下推自动机。因此，任何MHORS都可以在多项式时间内转换为等效的一阶MHORS。此外，我们表明，MHORS生成规则树，并可以在指数时间内转换为等价的0阶HORS。因此，MHORS具有与0-HORS相同的表达能力，但它们可以指数级地更简洁。我们的研究结果是通过结合游戏语义，几何互动和自动机理论的技术。2012 ACM学科分类计算理论→程序语义学
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. 2012 ACM Subject Classification Theory of computation → Program semantics