paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms

匹配命令式算法时间复杂度的基于规则的图程序
LMCS vol.Volume 22, Issue 22026匹配度 2/10 · 论文研究基于规则的图程序语言 GP2 的编译器数据结构与时间复杂度,属于程序语言/编译器方向,但未涉及 LLM、Agentic 程序、静态分析、浮点程序分析或贝叶斯程序分析等用户核心兴趣。其形式化证明与复杂度分析虽具 PL 理论色彩,但与应用场景相距较远。引用 1 inbox
Ziad Ismaili Alaoui, Detlef Plump
crossref: 2026-09-10

AI 速览

一句话:通过改进 GP 2 编译器的图数据结构,使基于规则的图程序在任意节点度图上达到命令式算法的时间复杂度。

基于规则的图程序通常难以达到传统命令式图算法的时间复杂度,主要瓶颈是图匹配的开销。此前工作表明,使用 GP 2 中的有根规则可使部分算法匹配命令式实现的运行时,但要求输入图节点度有界,且某些算法还要求连通。本文通过增强 GP 2 编译器生成的图数据结构,并在程序中利用该新结构,克服了这些限制。作者给出三个案例研究:连通性检查、无环性检查以及整数边权单源最短路径。前两个程序在任意节点度、可能不连通的图上线性时间运行;第三个在任意图上以 O(nm) 时间运行,匹配 Bellman-Ford 命令式实现。每个程序均被形式化证明正确性与时间复杂度,并在多种图类上进行了运行时实验。

问题
基于规则的图变换语言因图匹配开销难以达到命令式图算法的时间复杂度,且已有有根规则方案依赖节点度有界或连通性限制。
方法
增强 GP 2 编译器生成的图数据结构,并在基于规则的图程序中利用该结构,实现连通性、无环性与单源最短路径三个案例,并形式化分析正确性与复杂度。
评估
对每个程序给出正确性与时间复杂度的形式化证明,并在多种图类上进行运行时实验验证。
原文摘要(Abstract)

We report on recent advances in rule-based graph programming, which allow us to match the time complexity of some fundamental imperative graph algorithms. In general, achieving the time complexity of graph algorithms implemented in conventional languages using a rule-based graph-transformation language is challenging due to the cost of graph matching. Previous work demonstrated that with rooted rules, certain algorithms can be implemented in the graph programming language GP 2 such that their runtime matches the time complexity of imperative implementations. However, this required input graphs to have a bounded node degree and (for some algorithms) to be connected. In this paper, we overcome these limitations by enhancing the graph data structure generated by the GP 2 compiler and exploiting the new structure in programs. We present three case studies: the first program checks whether input graphs are connected, the second program checks whether input graphs are acyclic, and the third program solves the single-source shortest-paths problem for graphs with integer edge-weights. The first two programs run in linear time on (possibly disconnected) input graphs with arbitrary node degrees. The third program runs in time $O(nm)$ on arbitrary input graphs, matching the time complexity of imperative implementations of the Bellman-Ford algorithm. For each program, we formally prove its correctness and time complexity, and provide runtime experiments on various graph classes.

链接与引用

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

BibTeX
@article{abs-2501-09144,
  title = {Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms},
  author = {Ziad Ismaili Alaoui and Detlef Plump},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 2},
  year = {2026},
  doi = {10.46298/lmcs-22(2:20)2026}
}