When is an extension of a specification consistent? Decidable and undecidable cases (Q1186708)

Given a specification \(spec_ 1=(\Sigma_ 1,E_ 1)\) and a subspecification \(spec=(\Sigma,E)\) it is in general undecidable, whether \(spec_ 1\) is a consistent enrichment of \(spec\). The paper is concerned with the following questions: a) What are sufficient syntactic restrictions on \(spec\) and \(spec_ 1\) such that the problem becomes decidable? Where is the borderline between decidability and undecidability? b) What are sufficient algebraic conditions such that the problem becomes decidable? In abstract data types a specification \(spec=(\Sigma,E)\) consists of a set \(\Sigma\) of function symbols and a set \(E\) of defining equations. A specification \(spec_ 1=(\Sigma_ 1,E_ 1)\) with \(\Sigma\subseteq\Sigma_ 1\) is a consistent enrichment of \(spec\) if for all \(\Sigma\)-terms \(s\), \(t\) one has \(s=_ E t\) iff \(s=_{E_ 1}t\). Here \(=_ E\) is the \(E\)-equality defined by the operation `replace equals by equals'. Normally one restricts to variable-free terms \(s\), \(t\). This restriction is dropped. Only unary function symbols are allowed. In this case the specification \(spec=(\Sigma,E)\) is equivalent to a string replacement system (Thue system): One has to regard the function symbols as letters and the terms as words in \(\Sigma^*\). So only string replacement systems are considered. A string rewriting system \(R\) over \(\Sigma\) is a set of oriented equations (rules) of the form \(\ell\to r\) with \(\ell,r\in\Sigma^*\). It is length-reducing if for all rules we have \(|\ell|>| r|\). It is monadic if for all rules we have \(|\ell|>| r|\) and \(2>| r|\). Let \((\Sigma_ 1,R_ 1)\) and \((\Sigma_ 2,R_ 2)\) be given such that \(\Sigma_ 1\subsetneqq\Sigma_ 2\). \(R_ 2\) is a consistent extension of \(R_ 1\) if for all \(u,v\in\Sigma^*_ 1\) we have \(u=_{R_ 1}v\) iff \(u=_{R_ 2}v\). The results are as follows: (1) The consistency problem is undecidable even if \(R_ 1\) is restricted to be empty and \(R_ 2\) is restricted to be length-reducing and confluent. (2) The consistency problem becomes decidable if \(R_ 1\) is restricted to have a decidable word problem and \(R_ 2\) is restricted to be monadic and confluent. These results indicate where the exact borderline between decidability and undecidability in terms of syntactic restrictions has to be sought. The following results give algebraic conditions under which the consistency problem is decidable. The string rewriting \(R\) is defining a group if the monoid defined by \(R\) is a group. (3) The consistency problem becomes decidable if \(R_ 1\) is restricted to be terminating, confluent on the congruence class \([e]_{R_ 1}\) and group-defining and \(R_ 2\) is restricted to be length-reducing, confluent and group-defining.