paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Characterizations of Monadic Second Order Definable Context-Free Sets of Graphs

一元二阶可定义上下文无关图集合的刻画
LMCS vol.Volume 22, Issue 12026匹配度 1/10 · 该论文属于逻辑与自动机、图语法与 CMSO 刻画的理论工作,虽与形式化方法和程序验证的基础理论相关,但未涉及用户关注的核心方向:LLM/Agent 与静态分析交叉、浮点程序分析或贝叶斯程序分析。其研究目标、方法和场景均与当前研究画像距离较远。引用 0 inbox
Radu Iosif, Florian Zuleger
crossref: 2026-09-10

AI 速览

一句话:给出 CMSO 可定义且上下文无关图语言的三种等价刻画,并连接树到图可定义转换与可定义树分解。

本文刻画既可由计数一元二阶逻辑(CMSO)定义、又上下文无关的图集合,即 Hyperedge-Replacement(HR)文法的最小解。作者证明它们等价于:(a) HR-图代数中有界树宽的 recognizable 集合,且可细化到有限生成子代数;(b) parsable 集合:存在到以 HR 操作为标签的派生树的可定义转换,使图集合为该派生树集合在典范求值下的像;(c) 可识别无秩树集合在可定义转换下的像,且逆转换也可定义。方法上,作者建立 Courcelle–Engelfriet 的树到图可定义转换刻画与 Bojańczyk–Pilipczuk 的最优宽度树分解可定义构造之间的新联系。评估为理论证明。

问题
问题:哪些图集合同时具有 CMSO 可定义性和上下文无关性(HR 文法最小解),并如何用代数与转换概念刻画它们。
方法
方法:证明与有界树宽 recognizable 集合、parsable 集合、以及可识别无秩树在可定义转换下的像三者的等价,并利用 Courcelle–Engelfriet 与 Bojańczyk–Pilipczuk 的结果建立新联系。
评估
评估:理论证明,给出等价性定理;无实验评估。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{IosifZ26,
  title = {Characterizations of Monadic Second Order Definable Context-Free Sets of Graphs},
  author = {Radu Iosif and Florian Zuleger},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 1},
  year = {2026},
  doi = {10.46298/lmcs-22(1:22)2026}
}