The Confluence Problem for Flat TRSs(New Trends in Theory of Computation and Algorithm)
Ichiro Mitsuhashi, Michio Oyamaguchi, Florent Jacquemard · Institutional Repositories DataBase (IRDB) · 2006
We prove that confluence is undecidable br flat TRSs.Here, a TRS is flat if the heights of the $1\epsilon \mathrm{R}$ and right-hand sides of each rewrite rule $\mathrm{r}\epsilon$ at most one. 1 Introduction A term rewriting system $(\mathrm{T}\mathrm{R}S)$ is a set of directed equations (called rewrite rules).A TRS is confluent $(\mathrm{C}\mathrm{h}\mathrm{u}\mathrm{r}\mathrm{d}\succ$ Rosser) if any two convertible terms are joinable.Confluenoe is an important property sinoe it implies the unicity of normal forms [1], and has received much attention so far.But, confluenoe is undecidable in general and so even if we restricts to monadic or semi-constructor TRSs [6].On the other hand, it is known decidable for terminating TRSs [5] and $\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{h}\triangleright$ (ground or variable) TRSs [2].In paricular, confluence is decidable for right-linear shallow TRSs [3], hence we show here that the right-linearity oondition is necessary for decidabilty.Reoently, Jacquemard [4] has reported that confluenoe is undecidable for flat TRSs.Here, a TRS is flat if the heights of the left and $\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{h}\triangleright \mathrm{h}\mathrm{a}\mathrm{n}\mathrm{d}$ sides of each rewrite rule are at most one.However, we found that the proof is incorrect.In this paper, we give a correct proof of the undecidability. PreliminariesWe assume that the reader is familiar with standard deffiAtioo of rewrite systems [1] and we just recall here the main notations used in this paper.Let $\epsilon$ be the empty sequence.Let $X$ be a set of variables.Let $F$ be a flnite set of operation symbols graded by an arity function $\mathrm{a}\mathrm{r}:Farrow \mathrm{N}(=\{0,1,2, \cdots\}),$ $F_{n}=\{f\in F|\mathrm{a}\mathrm{r}(f)=n\}$ .Let $T$ be a set of terms built from $X$ and $F$ We use $x$ as a variable, $f,$ $h$ as function symbols, $t,$ $s,t$ as terms, $\theta$ as a substitution.The heig $ht$ of a term is defined as follows: $\mathrm{h}\mathrm{e}\mathrm{i}\epsilon \mathrm{h}\mathrm{t}(a)=0$ if $a$ is a variable or a constant and height $(f(t_{1}, \ldots,t_{n}))=$ $1+ \max\{\mathrm{h}\mathrm{e}\mathrm{i}\mathrm{g}\mathrm{h}\mathrm{t}(t_{1}), \ldots, \mathrm{h}\mathrm{e}\mathrm{i}_{l}\mathrm{h}\mathrm{t}(t_{n})\}$ if $n>0$ .A position in a term is expressed by a sequence of positive integers, and pogitions are partially ordered by the preflx ordering $\geq$ .Let $s_{1\mathrm{p}}$ be the subterm of $s$ at position $p$ .Let $s\geq_{\mathrm{u}\mathrm{b}}.t$ if $t$ is a subterm of $s$ .Forposition$p$ and term $t$ , we use $\epsilon[t]_{p}$ to denote the term obtained from $s$ by replacing a subterm $s_{1\mathrm{p}}$ by $t$ .A $nun\backslash l\epsilon$ rule $\alphaarrow\beta$ is a directed equation over terms.A $TRSR$ is a finite set of rewrite rules.A term $s$ reduces to $t$ at position $p$ by a TRS $R$ , denoted $sarrow_{R}t\mathrm{p}$ , if $s_{1p}=\alpha\theta$ and $t=\epsilon[\beta\theta]_{\mathrm{p}}$ for some rewrite rule $\alphaarrow\beta$ and substitution 9.For $s-_{R}\mathrm{p}t,$ $p$ and $R$ may be omitted.Let $arrow^{=}b\mathrm{e}arrow\cup=$ , and 4-the inverse $\mathrm{o}\mathrm{f}arrow$ .$s$ and $t$ are $joinabl\epsilon$ if $s\wedge^{*}\cdotarrow^{*}t$ , denoted $s\downarrow t$ .$t$ is reachable from $s$ if $\epsilonarrow^{l}t$ .$r$ is confluent on TRS $R$ if for every $sarrow_{R}^{l}farrow_{R}^{*}t,$ $s\downarrow t$ .A TRS $R$ is confluent if every $f$ is confluent on $R$ .Let 7: $\epsilon_{1}4_{s_{2}\cdotsarrow s_{n}}^{\mathrm{P}\mathrm{P}\cdot-\iota}$ be a rewrite sequencc.This sequence is abbreviated to 7: si $arrow^{*}s_{n}$ .or is called p-invariant if $q>p$ for any redex position $q$ of 7, and we write 7:Deflnition 2 A finite automaton is a 5-tuple $(Q, \Sigma, \delta, FS_{\Phi},)$ where $Q$ is a finite set of states, $\Sigma$ is a finite set of iuput symbols, 6: $Q\mathrm{x}\Sigmaarrow Q$ is a function, $FS\subseteq Q$ is a mte set of fnal states, and $q_{0}\in Q$ is the initial $\epsilon \mathrm{t}\mathrm{a}\mathrm{t}\mathrm{e}$ .