paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Partial derivatives on graphs for Kleene allegories

Kleene allegories 的图上偏导数
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 1/10 · 该论文研究 Kleene allegories 等式理论的可判定性与 EXPSPACE 复杂性，属于纯逻辑、自动机与关系代数理论，未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 18 inbox
Yoshiki Nakamura
逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：证明 Kleene allegories 等式理论可判定且为 EXPSPACE 完全，并用图上偏导数给出自动机构造。

本文研究 Kleene allegories 的等式理论可判定性。此前 Brunet 与 Pous 在 LICS 2015 证明了无恒等关系的关系 Kleene 格（Kleene allegories 的一个片段）的等式理论可在 EXPSPACE 内判定，但完整 Kleene allegories 的等式理论是否可判定仍是公开问题。作者通过将字符串上的 Antimirov 偏导数推广到图上，定义图上偏导数，并据此给出类似正则表达式的有限自动机构造算法。该构造为 Kleene allegories 的等式理论提供了判定程序，证明其可判定，并进一步确立其 EXPSPACE 完全性，从而回答了 Brunet 与 Pous 提出的首个公开问题。

问题
确定 Kleene allegories 的等式理论是否可判定及其复杂度，特别是回答 Brunet 与 Pous 关于该理论可判定性的公开问题。
方法
将字符串上的 Antimirov 偏导数推广为图上的偏导数，并用它构造有限自动机，从而得到等式理论的判定算法。
评估
通过复杂度分析证明 Kleene allegories 等式理论可判定且为 EXPSPACE 完全，给出与已有片段结果相匹配的界。
原文摘要（Abstract）

Brunet and Pous showed at LICS 2015 that the equational theory of identity-free relational Kleene lattices (a fragment of Kleene allegories) is decidable in EXPSPACE. In this paper, we show that the equational theory of Kleene allegories is decidable, and is EXPSPACE-complete, answering the first open question posed by their work. The proof proceeds by designing partial derivatives on graphs, which are generalizations of partial derivatives on strings for regular expressions, called Antimirov's partial derivatives. The partial derivatives on graphs give a finite automata construction algorithm as with the partial derivatives on strings.

链接与引用

DOI 原文 · DBLP

BibTeX 
@inproceedings{Nakamura17,
  title = {Partial derivatives on graphs for Kleene allegories},
  author = {Yoshiki Nakamura},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005132}
}