Partial derivatives on graphs for Kleene allegories
Partial derivatives on graphs for Kleene allegories
复制标题
Kleene 寓言图的偏导数
DOI：
10.1109/lics.2017.8005132
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Nakamura Yoshiki
中科院分区：
文献类型：
--
作者：
辻本真規;酒井明人;松本洋介;中辻知;Nakamura Yoshiki;Nakamura Yoshiki
Brunet和Pous在LICS 2015上表明，无同一性关系Kleene格（Kleene寓言的一个片段）的等式理论在EXPSPACE中是可决定的。在本文中，我们证明了Kleene寓言的等式理论是可决定的，并且是expspace完备的，回答了他们的工作提出的第一个开放问题。证明通过设计图上的偏导数来进行，这是正则表达式中字符串上偏导数的推广，称为Antimirov的偏导数。图上的偏导数给出了与字符串上的偏导数一样的有限自动机构造算法。
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.