We give a characterization of the sets of graphs that are both \emph{definable} in Counting Monadic Second Order Logic (CMSO) and \emph{context-free}, i.e., least solutions of Hyperedge-Replacement (HR) grammars introduced by Courcelle and Engelfriet \cite{courcelle_engelfriet_2012}. We prove the equivalence of these sets with: % (a) \emph{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) \emph{parsable} sets, for which there is a 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 a definable transduction, whose inverse is also 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 definable transductions, by Courcelle and Engelfriet and a proof that an optimal-width tree decomposition of a graph can be built by an definable transduction, by Bojańczyk and Pilipczuk.
翻译:本文刻画了同时满足以下两个条件的图集合:既在可数单子二阶逻辑(CMSO)中\emph{可定义},又具有\emph{上下文无关性},即作为Courcelle与Engelfriet所引入的超边替换(HR)文法的最小解。我们证明了这些集合与以下条件的等价性:%(a)在有界树宽的图HR运算代数中的\emph{可识别}集合;我们进一步细化该条件,证明其等价于在有限生成HR图代数子代数中的可识别性;%(b)\emph{可解析}集合,存在从图到以HR运算标记的派生树集合的可定义转换,使得图集合是派生树集合在HR运算规范求值下的像;%(c)在可定义转换(其逆转换也可定义)下,可识别非秩化树集合的像。%我们的证明基于两项开创性成果的新颖联系:一是Courcelle与Engelfriet提出的关于树到图可定义转换的上下文无关图语言逻辑特征化,二是Bojańczyk与Pilipczuk证明的图最优宽度树分解可通过可定义转换构建的理论。