The Monadic Second-order Logic Evaluation Problem on Finite Colored Trees: a Database-theoretic Approach
The Monadic Second-order Logic Evaluation Problem on Finite Colored Trees: a Database-theoretic Approach
复制标题
有限有色树上的一元二阶逻辑求值问题：数据库理论方法
DOI：
--
复制
发表时间：
2009
影响因子：
0.8
通讯作者：
Labrini Kalantzi
中科院分区：
文献类型：
--
作者：
Eugénie Foustoucos;Labrini Kalantzi
我们模型的一元二阶逻辑（MSO）的评价问题的有限着色树在一个纯粹的数据库理论框架，基于众所周知的MSO-自动机连接：我们减少了问题的非循环合取查询评价问题，一方面和一元数据集评价问题的另一方面。这种方法提供了使用关系代数表达式和数据库程序的优化评估方法来解决MSO问题的可能性（例如Yannakakis算法[27]和[3]中使用基于分辨率的过滤的重写方法，称为“魔术集”方法）：我们使用这些方法来评估我们的查询并估计其复杂性。据我们所知，这是第一次给出与关系代数相关的MSO求值问题的解决方案;此外，由于这种约简，我们证明了[8]中给出的基于自动机的算法构成了Yannakakis算法的一个特殊“实例”。除了我们提出的解决MSO评价问题的优化数据库方法外，我们的结果证明了着色树上的MSO可定义查询是数据记录可定义的;这个结果包含了[12]中的相应结果，该结果指出一元MSO查询是一元数据记录可定义的，并且还包含了众所周知的结果，即任何MSO可定义的树类都是一元数据记录可定义的。
We model the monadic second-order logic (MSO) evaluation problem on finite colored trees in a purely database theoretic framework, based on the well-knownMSO-automata connection: we reduce the problem to an acyclic conjunctive query evaluation problem on the one hand and to a monadic datalog evaluation problem on the other hand. This approach offers the possibility to solve the MSO problem using optimized evaluation methods for relational algebra expressions and for datalog programs (such as Yannakakis algorithm [27] and the rewriting method using resolutionbased filtering referred to as "magic sets" method in [3]): we use these methods for evaluating our queries and giving estimates of their complexity. This is the first time, to our knowledge, that a solution to the MSO evaluation problem related to relational algebra is given; furthermore, thanks to this reduction, we prove that the automata-based algorithm given in [8] constitutes a particular "instance" of Yannakakis algorithm. Besides the optimized database methods that we propose for solving the MSO evaluation problem, our results prove that MSO-definable queries over colored trees are datalog-definable; this result subsumes the corresponding result in [12] which states that unary MSO queries are monadic datalog-definable and it also subsumes the well-known result that any MSO-definable class of trees is monadic datalog-definable.