Recursion Schemes and Logical Reflection
Recursion Schemes and Logical Reflection
复制标题
递归方案和逻辑反射
DOI：
10.1109/lics.2010.40
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Broadbent C
中科院分区：
文献类型：
--
作者：
Broadbent C
设R是一类结点标号无限树的生成元，L是描述树正确性的逻辑语言。给定R中的R和L中的phi，我们说r_phi是r的aphi-反射，只要（i）r和r_phi生成相同的底层树，并且（ii）假设由r生成的树t（r）的节点u具有标签f，则t（r_phi）的节点u的标签是f*，如果uin t（r）满足phi;否则它是f。因此，如果t（r）是程序r的计算树，我们可以把r_phi看作是R的一个变换，它可以在内部观察它对规范phi的行为。我们说R是（相长）反射的。如果有一个算法可以将给定的对（r，phi）转换为r_phi。在本文中，我们证明了高阶递归计划是反射w.r.t.模态μ演算和一元二阶逻辑（MSO）。为了得到这个结果，我们给出了第一个特征的奇偶游戏的获胜区域的过渡图的可折叠下推自动机（CPDA）：它们是由一类新的自动机定义的正则集。（n阶递归方案与n阶CPDA生成树的表达相同。作为一个推论，我们表明，这些计划是封闭的MSO-解释的操作下，然后由树展开一个香格里拉Caucal。
Let R be a class of generators of node-labelled infinite trees, and Lbe a logical language for describing correctness properties of the setrees. Given r in R and phi in L, we say that r_phi is aphi-reflection of r just if (i) r and r_phi generate the same underlying tree, and (ii) suppose a node u of the tree t(r) generated by r has label f, then the label of the node u of t(r_phi) is f* if uin t(r) satisfies phi; it is f otherwise. Thus if t(r) is the computation tree of a program r, we may regard r_phi as a transform of R that can internally observe its behaviour against a specification phi. We say that R is (constructively) reflective w.r.t. L just if there is an algorithm that transforms a given pair (r,phi) to r_phi. In this paper, we prove that higher-order recursion schemes are reflective w.r.t. both modal mu-calculus and monadic second order(MSO) logic. To obtain this result, we give the first characterisation of the winning regions of parity games over the transition graphs of collapsible pushdown automata (CPDA): they are regular sets defined by a new class of automata. (Order-n recursion schemes are equi-expressive with order-n CPDA for generating trees.) As a corollary, we show that these schemes are closed under the operation of MSO-interpretation followed by tree unfolding a la Caucal.
登录
查看更多内容
影响因子：
1
作者：
Colin Bennett;Ronald A. DeVore;R. Sharpley
通讯作者：
Colin Bennett;Ronald A. DeVore;R. Sharpley
依赖树自动机
DOI：
10.1007/978-3-642-00596-1_8
发表时间：
2009
期刊：
Inf. Comput.
影响因子：
--
作者：
C. Stirling
通讯作者：
C. Stirling
可折叠下推自动机和递归方案
DOI：
10.1145/3091122
发表时间：
2008
期刊：
2008 23rd Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
M. Hague;A. Murawski;C. Ong;O. Serre
通讯作者：
O. Serre
DOI：
10.1007/3-540-61604-7_60
发表时间：
1996-08
期刊：
--
影响因子：
--
作者：
David Janin;I. Walukiewicz
通讯作者：
David Janin;I. Walukiewicz
在无限项上具有可判定的一元理论
DOI：
10.1007/3-540-45687-2_13
发表时间：
2002
期刊：
2008 23rd Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
D. Caucal
通讯作者：
D. Caucal