We give a characterization of those sets of graphs that are both definable in Counting Monadic Second Order Logic (CMS) and context-free, i.e., least solutions of Hyperedge-Replacement (HR)-grammars introduced by Courcelle and Engelfriet. We give the following equivalent characterizations: (a) a set of graphs is recognizable (in the algebra that consists of all graphs and HR-operations) and has bounded tree-width; further, we refine this condition and show equivalence with recognizability in a finite-sort subalgebra of the graph algebra; (b) the set is parsable, i.e., there is an MS-definable transduction from graphs to a set of derivation trees labelled by HR-operations, such that the set of graphs is the image of this set of trees under the evaluation of the HR-operations; (c) the set of graphs is the image of unranked recognizable set of trees under an MS-definable transduction whose inverse is also MS-definable. The main goal of this paper is to present the above characterization, of which several directions are already known, in an accessible and unified way. We rely on a novel connection between two seminal results, a logical characterization of context-free graph languages in terms of tree to graph MS-definable transductions, by Courcelle and Engelfriet~, and a proof that an optimal-width tree decomposition of a graph can be built by an MS-definable transduction, by Bojanczyk and Pilipczuk.
翻译:我们给出了那些同时可在计数单子二阶逻辑(CMS)中定义且是上下文无关的(即Courcelle和Engelfriet引入的超边替换(HR)文法的极小解)图集合的刻画。我们得到以下等价刻画:(a)一个图集合是可识别的(在由所有图和HR运算构成的代数中)且具有有界树宽;进一步地,我们细化该条件,证明其等价于在图形代数的有限排序子代数中的可识别性;(b)该集合是可解析的,即存在一个从图到由HR运算标记的派生树集合的MS可定义转导,使得该图集合是这些树在HR运算求值下的像;(c)该图集合是在逆映射也是MS可定义的一类MS可定义转导下,无秩可识别树集合的像。本文的主要目标是以易于理解且统一的方式呈现上述刻画(其中若干方向已有已知结果)。我们依赖于两个开创性结果之间的新联系:Courcelle和Engelfriet提出的关于从树到图的MS可定义转导的上下文无关图语言的逻辑刻画,以及Bojanczyk和Pilipczuk证明的关于可通过MS可定义转导构建图的最优宽度树分解的结果。