We give a characterization of the sets of graphs that are both definable in Counting Monadic Second Order Logic (CMSO) and context-free, i.e., least solutions of Hyperedge-Replacement (HR) grammars introduced by Courcelle and Engelfriet. We prove the equivalence of these sets with: (a) recognizable sets (in the algebra of graphs with HR-operations) of bounded tree-width; we refine this condition further and show equivalence with recognizability in a finitely generated subalgebra of the HR-algebra of graphs; (b) parsable sets, for which there is an MSO-definable transduction from graphs to a set of derivation trees labelled by HR operations, such that the set of graphs is the image of the set of derivation trees under the canonical evaluation of the HR operations; (c) images of recognizable unranked sets of trees under an MSO-definable transduction, whose inverse is also MSO-definable. We rely on a novel connection between two seminal results, a logical characterization of context-free graph languages in terms of tree to graph MSO-definable transductions, by Courcelle and Engelfriet and a proof that an optimal-width tree decomposition of a graph can be built by an MSO-definable transduction, by Bojanczyk and Pilipczuk.
翻译:我们给出了同时可在计数幺半二阶逻辑(CMSO)中定义且为上下文无关(即Courcelle与Engelfriet引入的超边替换文法的最小解)的图集合的特征刻画。我们证明这些集合等价于:(a)具有有界树宽的可识别集合(在带HR运算的图代数中);我们进一步细化该条件,证明其等价于在HR图代数的有限生成子代数中的可识别性;(b)可解析集合,即存在从图到由HR运算标记的推导树集合的MSO可定义转换,使得该图集合是推导树集合在HR运算规范求值下的像;(c)在MSO可定义转换下(其逆转换也是MSO可定义的)可识别无秩树集合的像。我们的证明建立在两个开创性结果的新颖联系之上:其一是Courcelle与Engelfriet关于上下文无关图语言在树到图MSO可定义转换方面的逻辑特征刻画,其二是Bojanczyk与Pilipczuk关于可通过MSO可定义转换构建图的最优宽度树分解的证明。