In this paper, we investigate problems which are dual to the unification problem, namely the Fixed Point (FP) problem, Common Term (CT) problem and the Common Equation (CE) problem for string rewriting systems. Our main motivation is computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point (FP) problem is reducible to the common term problem. Our new results are: (i) the fixed point problem is undecidable for finite convergent string rewriting systems whereas it is decidable in polynomial time for finite, convergent and dwindling string rewriting systems, (ii) the common term problem is undecidable for the class of dwindling string rewriting systems, and (iii) for the class of finite, monadic and convergent systems, the common equation problem is decidable in polynomial time but for the class of dwindling string rewriting systems, common equation problem is undecidable.
翻译:本文研究了与统一问题对偶的问题,即字符串重写系统中的不动点问题、公共项问题和公共方程问题。我们的主要动机是计算系统中的不动点,例如编程语言中的循环不变量。我们证明不动点问题可归约到公共项问题。我们的新结果如下:(i) 对于有限收敛的字符串重写系统,不动点问题不可判定,而对于有限、收敛且萎缩的字符串重写系统,该问题可在多项式时间内判定;(ii) 对于萎缩字符串重写系统类,公共项问题不可判定;(iii) 对于有限、一元且收敛的系统类,公共方程问题可在多项式时间内判定,但对于萎缩字符串重写系统类,公共方程问题不可判定。