Rewriting Regular Inequalities (Extended Abstract)
Rewriting Regular Inequalities (Extended Abstract)
复制标题
DOI：
10.1007/3-540-60249-6_44
复制
发表时间：
1995-08
期刊：
影响因子：
--
通讯作者：
Valentin M. Antimirov
中科院分区：
文献类型：
--
作者：
Valentin M. Antimirov
本文对有限字母表A上的正则事件(语言)的代数REG[A]中的包含问题应用了代数规格说明和项重写方法：给定两个正则表达式r，t(在A上)，以检验不等式r<；t在REG[A]中是否有效。解决这个问题的标准方法是基于表达式r，t到确定性有限自动机(DFAS)的翻译；事实上，人们也可以使用r的非决定性自动机(NFA)。我们方法的主要特点是我们避免了这样的翻译，并开发了一个术语重写系统(Trs)来将r<；t简化为范式；当R<；t在Reg‘4中无效时，后者是假的。这提供了一个纯粹的代数(符号)决策过程--对于包容问题和文字问题--这本身似乎是一个有趣的贡献。2.此外，由于扩展了一些新的重写规则，我们的TRS在某些情况下提供了多项式大小的导数，而任何基于表达式到DFA的转换的算法都会导致指数爆破--我们用例子证明了这一点。当然，我们过程的最坏情况下的复杂性仍然是指数级的--这并不奇怪，因为问题是PSPACE-Complete[10，8，9]。在文章的最后，我们通过用自动机理论解释我们的TRS实现的推理过程，将我们的解决方案与标准的解决方案进行了更一般的比较。我们还利用了最近从文献[1]中引入的偏导数技巧。
In this paper we apply algebraic specification and term-rewriting methods to the containment problem in the algebra Reg [A] of regular events (languages) on a finite alphabet A formulated as follows: given two regular expressions r, t (on A), to check if the inequality r< t is valid in Reg [A]. Standard approaches to the problem are based on translation of the expressions r, t into deterministic finite automata (DFAs); in fact, one can also do with a non-determistic one (NFA) for r. The main peculiarity of our approach is that we avoid such a translation and develop a term-rewriting system (trs) to reduce r< t into a normal form; the latter is false whenever r< t is not valid in Reg'4]. This provides a purely algebraic (symbolic) decision procedure-both for the containment and word problems-that seems to be an interesting contribution per se. 2.Moreover, being extended with some new rewrite rules, our trs, in some cases provides derivations of polynomial size, while any algorithm based on translation of the expressions into DFAs gives rise to an exponential blow-up-we demonstrate this on examples. Of course, the worst-case complexity of our procedure is still exponential-this is not surprising, since the problem is PSPACE-complete [10, 8, 9]. At the end of the paper we provide a more general comparison of our solution with the standard ones by giving an automata-theoretic interpretation of the inference process implemented by our trs Some ideas of the present work come from [2]. We also employ a recently introduced technique of partial derivatives from [1].