单调第二阶逻辑可定义图的上下文无关集的特征化
Characterizations of Monadic Second Order Definable Context-Free Sets of Graphs
AI总结：
本文特征化了由单调第二阶逻辑和上下文无关文法定义的图集，通过树宽、可解析性及树转换等方法证明其等价性。
摘要：
我们给出了同时可由计数单调第二阶逻辑（CMSO）定义且上下文无关的图集的特征化，即超边替换（HR）文法的最小解。我们证明了这些集等价于：（a）具有有界树宽的图在图代数中的可识别集；我们进一步细化这一条件，并显示其等价于在HR代数的有限生成子代数中可识别；（b）可解析集，其中存在一个可定义的转换，将图转换为带有HR操作标记的推导树集，使得图集是推导树集在HR操作的规范评估下的像；（c）在可定义的转换下，可识别无等级树集的像，其反向也是可定义的。我们依赖于两个开创性结果之间的新联系，即Courcelle和Engelfriet对上下文无关图语言的逻辑特征化，以及Bojanczyk和Pilipczuk证明最优宽度树分解可通过可定义的转换构建的证明。
英文摘要：
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 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 Bojanczyk and Pilipczuk.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
