Lambda-confluence for context rewriting systems (Q2344748)

In a context rewriting system \(C = (\Sigma,\Gamma,I)\), \(\Gamma\) is a finite working alphabet that contains the input alphabet \(\Sigma\) as a subset, but neither \(\#\) nor \(\$ \), and \(I\) is a finite set of instructions \((x \mid z \rightarrow t \mid y)\), where \(x\in \Gamma^* \cup \#\Gamma^*\), \(y \in \Gamma^* \cup \Gamma^* \$\), and \(z,t \in \Gamma^*\). A word \(uzv\) can be rewritten as \(utv\) using the instruction \((x \mid z \rightarrow t \mid y)\) if \(x\) is a suffix of \(\# u\) and \(y\) is a prefix of \(v\$\). The language accepted by \(C\) consists of the words over \(\Sigma\) that can be reduced to the empty word \(\lambda\). The authors consider three special types of such systems defined by various restrictions on the instructions allowed, namely limited context restarting automata (lc-R-automata) of types \(\mathcal{R}_1\) and \(\mathcal{R}_2\), and clearing restarting automata. In all three cases the membership problem is decidable, with \(\mathrm{NTIME}(n^2)\) as an upper complexity bound, because all rewriting steps are length-reducing. However, the time complexity becomes linear if the system is \(\lambda\)-confluent, i.e., confluent in the equivalence class of the empty word. It is shown that \(\lambda\)-confluence is decidable in polynomial time for type-\(\mathcal{R}_2\) lc-R-automata, but not even recursively enumerable for clearing restarting automata or type-\(\mathcal{R}_1\) lc-R-automata. Context rewriting systems are closely related to string rewriting systems, and the main theorem of the paper, from which the above two undecidability results also follow, states that \(\lambda\)-confluence is not recursively enumerable for finite factor-erasing string rewriting systems.