Collapsible Pushdown Automata and Recursion Schemes
Collapsible Pushdown Automata and Recursion Schemes
复制标题
可折叠下推自动机和递归方案
DOI：
10.1145/3091122
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
O. Serre
中科院分区：
文献类型：
--
作者：
M. Hague;A. Murawski;C. Ong;O. Serre
可折叠下推自动机（Collapsible Pushdown Automata，CPDA）是一种新的高阶下推自动机，它的栈中的每个符号都有一个指向下一个栈的链接，除了高阶的push和pop操作外，CPDA还有一个重要的操作叫做collapse，它的作用是将栈s“折叠”到栈s最上面的符号的链接所指示的前缀。我们的第一个结果是，CPDA是equi-expressive与递归计划的发电机（可能是无限的）排名树。在一个方向上，我们给出了一个简单的算法，将一个阶n CPDA到一个阶n递归方案，生成相同的树，均匀地为所有n Gt= 0。在另一个方向，使用游戏语义的想法，我们给了一个有效的转换阶n递归计划（不假设是同质类型的，因此不一定安全），以阶n CPDA，计算遍历的抽象语法图的计划，因此在树中的路径产生的计划。我们的equi-expressivity结果是第一个自动机理论表征高阶递归计划。因此，CPDA也是简单类型lambda演算的一个特征，它具有递归（从未解释的一阶符号生成）和（纯）无辜策略。一个重要的后果，equi-expressivity的结果是，它允许我们减少决策问题的递归方案产生的树CPDA等价的问题，反之亦然。因此，我们表明，作为Ong最近结果的结果，（模态μ演算模型检查递归方案生成的树是n-EXPTIME完全的），解决n阶CPDA配置图上的奇偶博弈问题是n-EXPTIME完全的，包含了几个关于高阶下推图上博弈可解性的著名结果，Walukiewicz，Cachat和Knapik等人。我们工作的另一个贡献是通过推广该领域的标准技术来证明相同的可解性结果。利用我们的等表示性结果，我们得到了Ong结果的一个新的证明。与高阶下推图相比，我们证明了CPDA的配置图的一元二阶理论是不可判定的。由此可见，作为图的生成器，CPDA比高阶下推自动机更有表现力。
Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order push and pop operations, CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the topmost symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of (possibly infinite) ranked trees. In one direction, we give a simple algorithm that transforms an order-n CPDA to an order-n recursion scheme that generates the same tree, uniformly for all n Gt= 0. In the other direction, using ideas from game semantics, we give an effective transformation of order-n recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) to order-n CPDA that compute traversals over an abstract syntax graph of the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first automata-theoretic characterization of higher-order recursion schemes. Thus CPDA are also a characterization of the simply-typed lambda calculus with recursion (generated from uninterpreted 1st-order symbols) and of (pure) innocent strategies. An important consequence of the equi-expressivity result is that it allows us to reduce decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. Thus we show, as a consequence of a recent result by Ong (modal mu-calculus model-checking of trees generated by recursion schemes is n-EXPTIME complete), that the problem of solving parity games over the configuration graphs of order-n CPDA is n-EXPTIME complete, subsuming several well-known results about the solvability of games over higher-order pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Another contribution of our work is a self-contained proof of the same solvability result by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of Ong's result. In contrast to higher-order pushdown graphs, we show that the monadic second-order theories of the configuration graphs of CPDA are undecidable. It follows that -- as generators of graphs -- CPDA are strictly more expressive than higher-order pushdown automata.
登录
查看更多内容
递归方案和逻辑反射
DOI：
10.1109/lics.2010.40
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Broadbent C
通讯作者：
Broadbent C
安全 Lambda 演算
影响因子：
0.6
作者：
Blum W
通讯作者：
Blum W
自动机无限运行的简单类型 Lambda 术语的有限语义
影响因子：
0.6
作者：
Aehlig K
通讯作者：
Aehlig K
2 级可折叠下推图是树自动的
DOI：
10.2168/lmcs-9(1:12)2013
发表时间：
2013
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Alexander Kartzow
通讯作者：
Alexander Kartzow