数理解析研究所講究録 1222 巻 2001 年 105-113

105

Parallel Computation
andSynchronized Term Rewriting Systems-Extended Abstract-

Ken-Etsu Fujita (藤田 憲悦)
Shimane University(島根大学)
fujiken@cis.shimane-u.ac.jp

Aart Middeldorp
University of Tsukuba(筑波大学)
ami@is.tsukuba.ac.jp

Abstract
We present an extension of term rewriting systems with the mechanism of synchronization, called synchronized TRSs. The notion of synchronization is newly introduced for synchronizing applications of rewrite rules. The construction of
nized TRSs can be regarded as acombination problem of TRSs. We prove fundamental properties of synchronized ground TRSs:-ground synchronized TRSs.
(1) Termination property is decidable for finite$\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{c}\mathrm{h}\mathrm{r}\triangleright$$\mathrm{r}\mathrm{i}\grave{\mathrm{g}}\mathrm{h}\mathrm{t}$(2) The reachability problem for synchronized ground TRSs is undecidable.
We show two prooS of the second result, using the halting problem for two counter
automata and using Post’s correspondence problem. The prooffi also reveal explicitly arole of synchronization to be acorrespondence or coordination relation among
computations.

1Introduction
The notion of term rewriting systems (TRSs) gives amathematical model of computationin terms of aset of rewrite rules. In particular, the traditional TRSs play a role of anaturalmodel of sequential computations. We present an extension of term rewriting systems
with the mechanism of synchronization, called synchronized TRSs. Synchronization is
widely used as amechanism of parallel programming with explicit concurrency. The notionof synchronization is newly introduced into TRSs from the motivation for synchronizing
applications of rewrite rules, i.e., synchronized computation. The new notion captures
intrinsically paralel computation. We prove fundamental properties of synchronized TRSs:(1) Termination is decidable for finite right-ground synchronized TRSs.
(2) The reachabilty problem for synchronized ground TRSs is undecidable.

106
It is well-known that termination for finite right-ground TRSs is decidable. We show that
this property also holds for finite right-ground synchronized TRSs, although the parallel
computation is not closed under contexts. On the other hand, the reachabilty problem
of ground TRSs is known -complete[TN83], and the decidabilty result is now extended
to more general cases [Oya90, NT99]. However, from the second result the reachabilty
problem becomes undecidable even in the case of synchronized ground TRSs. Moreover,synchronized ground TRSs has Turing computability. The encodings used in the prooffi also
reveal explicitly arole or mechanism of synchronization in pure programming languages.
The notion of synchronization is involved in the work on Metaterm Rewriting Calculus(MRC) by Ohshima and Sakabe [OS99]. Although both have synchronized annotations(labels) for rewrite rules, the key distinction is that occurrences and to be synchronously, and hence our resultsinrewritten are explicitly mentioned as anew term
obtained here cannot be applied to their calculus straightforwardly.
$\mathcal{P}$$t_{2}$$t_{1}$$t_{1}\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{c}t_{2}$$[\mathrm{O}\mathrm{S}\Re]$2Synchronized Term Rewriting Systems(1) the term$s$in the left-hand side is not avariable, and(2) the variables appeared in the-hand side are contained in the left-hand side .
$t$$\mathrm{r}\mathrm{i}\phi \mathrm{t}$$s$riting system is
We write $sarrow t$ for , . Let be aset of rewrite rules. A
aterm rewriting system any set. For simplicity we often
defined as apair (of rewrite rules. Aterm rewriting system is called finite if is afinite set. If for each$larrow r$ $\in R$ the right- and side
contains no variables, then the term rewriting system is
caUd right-ground.
Acontext is obtained from term by replacing one occurrence of the subterm withaspecial symbol $[]$ cffled ahole. Aterm context is denoted by $t[]$ . For aterm context $t[]$
and aterm , $t[s]$ denotes aterm obtained by placing into the hole of $t[]$ . Asubstitution
for every $f\in F_{n}$ .
is amap from to such thatfor someis defined as
Aone step rewriting (reduction) relation$larrow r\in R$ . We say that the term
applicationbythe(contracted)
tois reduced
is called a redex. Aterm is in nomal $fom$ if and only if it contains
of $larrow r$ $\in R$ , and, and the reflexive and transitiveby
no redex. We denote the transitive closure, respectively
closure by$\langle$

$s$

$R$

$t)$

$t\mathrm{e}\mathrm{m}$

$oe$

$R$

$\mathrm{c}\mathrm{a}\mathrm{u}$$\Sigma,R\rangle$

$R$

$R$

$R$

$r$

$te\mathrm{m}$

$s$

$s$

$\mathcal{T}$$\sigma$$\mathcal{T}$$\sigma(f(t_{1},\ldots,t_{n}))=f(\sigma(t_{1}), \ldots,\sigma(t_{l},))$$t[\sigma(l)]\prec_{R}t[\sigma(r)]$$arrow R$$t[\sigma(r)]$$t[\sigma(l)]$$\sigma(l)$$\mathrm{o}\mathrm{f}arrow R$$\prec_{R}^{*}$$\prec_{R}^{+}$

107
riting system (STRS) to be aterm rewriting
Second we define asynchronizedWe
write : $larrow r$ for alabelled rewrite rule,rules.
system consisting of labelled rewrite
where is called alabel or an annotation for synchronization. An STRS is called finite
right-ground if is afinite set and the right-hand side of every rule in contains novariables. A ground STRS is an STRS in which no rewrite rule contains variables. Aone
by an STRS is defined as contracting, at pairwise disjoint
step rewriting relation
positions in aterm, maximal number of redexes simultaneously by rewrite rules only with, and the reflexive
is denoted by
the same annotation. The transitive closure of. We cffi computation by the application ofand transitive closure is byparallel computation.
For instance, let be the following STRS:$te\mathrm{m}re$

$i$

$R$

$i$

$R$

$R$

$R$

$=_{R}$$\mathrm{Z}_{R}$$\supset_{R}^{+}$$=_{R}$$=_{R}^{\mathrm{s}}$$\mathrm{m}\mathrm{n}\cdot \mathrm{m}\mathrm{a}\mathrm{N}\mathrm{y}$$R$$R=(\begin{array}{ll}1\cdot.aarrow b 2\cdot.barrow c1\cdot.aarrow c 2\cdot.carrow a1..f(x)arrow g(x,x) \end{array})$

Then we have one step reduction by maximally parallel computation, as follows:$f(a)\supset_{R}f(b)$ , $f(c)$ , or $g(a, a)$ ;$g(a, f(a))\supset_{R}g(b, f(b))$ , $g(b, f(c))$ , $g(c, f(b))$ , $g(c, f(c))$ , $g(b,g(a,a))$ , or $g(c,g(a, a))$ ;$g(a, b)\Xi_{R}g(b, b)$ ,, or $g(a, c)$ .
$\mathrm{g}(\mathrm{c},$iRom the definition, the maximally parallel computation is not closed under acontext. In thisin general. That is, for aterm context $t[]$ , $t[s_{1}]p_{R}t[s_{2}]$ even though$t[s_{1}]=_{R}t[s_{2}]$thatthedefinition
.
clear
from
It
is
some
context
forcase, we only obtain$R$, where $|R|$ denotes aTRS obtained by omitting the labels from . The inverse
does not hold true, in general, because of the synchronized annotations.
direction
This property is an essential point of giving encodings in the following sections, so that thecorrespondence relation of Post’s correspondence problem is naturally represented as thenotion of synchronization together with ground terms as well as the coordination of thetwo counters of automata. In the following sections, we investigate the termination andreachability properties for STRSs with the maximally parallel computation.
$s_{1}\supset_{R}s_{2}$$\mathrm{P}[]$$\supset_{R}\subseteqarrow_{|R|}^{+}$$\supset_{R}^{+}\supseteqarrow_{|R|}^{+}$

3Termination for finite right-ground STRSs
In this section, we prove that termination is decidable for finite right-ground STRSs. An
STRS is terminating (strongly nomalizing or noetherian) if and only if there is no infinite. An STRS is weakly nomalizing if every term has areduction sequence
normal form.
$R$$t_{1}\supset_{R}t_{2}\supset_{R}\cdots$

Lemma 1An STRS is not terminating if and only if it admits infinite reduction sequencesthat contain a root rewrite step.

Proof. We show the if part since the only-if part is clear. Assume that we have an. By induction on the structure of , weinfinite reduction sequence Seq: $t_{1}=$ $t_{2}=$prove that there also exists an infinite reduction sequence that contain aroot rewrite step.
$\cdots$$t_{1}$

108
The base case is obvious, i.e., aconstant itself is contracted.
Suppose $t_{1}=f(s_{1}, \ldots, s_{1*})$ . If Seq contains no root rewrite steps, then all the steps takeplace in the proper subtenns , , . The number of the subtenns is finite, while Seq
number of rewrite steps. Hence, from pigeonhole principle there exists
admits an:that admits an infinite reduction. According to the induction hypothesis, we also havean infinite reduction that contains aroot rewrite step.
$t_{1}$$s_{1}$$\ldots$$s_{n}$$\underline{\inf \mathrm{i}\mathrm{n}\mathrm{i}}\mathrm{t}\mathrm{e}$$S$$\square$Corollary 1A right-ground STRS $R$ is terminating if and only
$R$ ,is terminating.

$|.f$for any rule $i:larrow r\in$$r$

had aninfinite reduction sequence. From Lemma 1, the infinite path contains aroot rewrite step.
-yound STRS guarantees that aredex is the right- and side of arewrite rule.
Aacontradiction.
of them are terminating, which

Proof. We show the only-if part since the if part is clear. Suppose that$R$$\cdot\ovalbox{\tt\small REJECT} \mathrm{t}$$\mathrm{N}\mathrm{o}\mathrm{w}\square$$\mathrm{m}$$\dot{g}\mathrm{v}\mathrm{a}\mathrm{e}$Lemma 2Let be a finite right-ground STRS.
is not terminating if and only for some term context $t[]$ and a redex $mle$ : $larrow r\in R$ ,.
we have
$R$

$R$

$i$

$|.f$

$r$ $3_{R}^{+}t[r]$

.

. If

is not terminating,sequence Seq:
infinitean
havesuch that wethen ffom Corollary 1 there exists ::: $larrow r\in R$ is$\equiv t_{1}3_{R}t_{2}3_{R}\cdots$ . According to the excluded middle, the rewrite rule
applied in Seq or not.
Case where :: $larrow r$ is applied in Seq:
We have $3_{R}^{*}\#[\sigma(l)]3_{R}t[r]$ for some term contexts $f[]$ and $t[]$ .
:.
by the use of the induction hypothesis for
The statement can be$t[r]=_{R}^{+}t_{1}[t[r]]=_{R}^{+}\cdots$for
For the only-if part, if we have $r3_{R}^{+}t[r]$ , then we also haveHence,, even though the computation is not closed under contexts.
some context
induces an infinite reduction sequence, and is not terminating.
$Pmf$ The if part is proved by induction on the cardinalty of $R$$R$$larrow r$ $\in R$

$i$

$r$

$r$

$\mathrm{O}\mathrm{t}\mathrm{h}\alpha \mathrm{w}\mathrm{i}\mathrm{s}\mathrm{e}$$R\backslash \{i:larrow r\}$$\infty \mathrm{f}\mathrm{f}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{d}$$t_{1}[]$$\square r$$R$

Proposition 1Termination is decidable for finite right-grv und STRSs.

Proof. The decision procedure for termination of finite rigb round STRSs is derived

from Lemma 2. Generate the reducts of the right-hand sides of aU the rewrite rules in afor some context $t[]$ , then the STRS isbreadth-first way. If we do not observe
terminating from Lemma 2, and hence the process of the reductions eventually terminates.
If we observe $r3_{R}^{+}t[r]$ for some context $t[]$ , then the STRS cannot be terminating
Lemma 2.
$r$

$3_{R}^{+}t[r]$$\mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}\square$

We are currently investigating whether other known (un)decidability results for restricted classes of TRSs carry over to STRSs.

109
4Synchronization and Post’s Correspondence Problem
property is undecidsection, we prove that theIn this section and theterms,and that ground STRSs has Turing
able for STRSs even consisting only of groundcomputability. The decidable reachability property cannot be carried over to ground STRSs
from ground TRSs. The reachability problem for STRSs is, given an STRS $R$ and terms
or not.
and , to decide whether$\mathrm{r}\mathrm{e}a\mathrm{c}\mathrm{h}\mathrm{a}\mathrm{b}\underline{\mathrm{i}\mathrm{l}\mathrm{i}}\mathrm{t}\mathrm{y}$$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{i}\cdot \mathrm{g}$$t_{1}$$t_{1}=_{R}^{\mathrm{s}}t_{2}$$t_{2}$

Let be anon-empty finite set including at least two symbols, called alphabet. For
be aset of aU words over
simplicity, we set as {0, 1} without loss of generalty. Letofarbitrary
finiteset
excludingwords. Given anpairs of corresponding non-null words on , then Post’s correspondence decision problem, such that
(PCP) [POs46] is to decide if there exist ,i2,$\Sigma$$\Sigma^{+}$$\Sigma$$\Sigma$$\{(\alpha:,\sqrt{}^{})|\alpha:,\sqrt{}^{}\in\Sigma^{+}(1\leq i\leq n)\}$$\mathrm{n}\mathrm{u}\mathrm{U}$$\Sigma$$i_{1}$$(k\geq 1, 1\leq i_{\mathrm{j}}\leq n)$$\ldots$$i_{k}$$\alpha:_{1}\alpha_{2}\dot{.}\cdots$$\alpha:_{k}=\sqrt.\cdot 1\sqrt.\cdot 2\ldots$$\sqrt.\cdot k$.

Given an instance of Post’s correspondence problem, then define the following STRS
over the signature consisting of constants , $b,c$ , , unary function symbols 0, 1, and abinary function symbol :
$R$

$a$

$d$

$f$

.
$R=(n.\cdot+3^{\cdot}..\cdot.0(d)arrow dn+3.0(c)arrow cn+1.0(b)arrow dn+1.0(a)arrow c1.aarrow\alpha_{1}1(a)1.barrow\sqrt(b)$$1(d)arrow dn.barrow\sqrt n(b)n.aarrow\alpha.*n+2.1(a)arrow cn+4\cdot 1(c)arrow cn+2\cdot 1(b)arrow d(a))$$n..+4^{\cdot}..\cdot$

where the natural numbers 1, 2, ..., $n+4$ are used as annotations for synchronization.
Lemma 3 $f(a, b)=_{R}^{*}f(c,d)$ if and only if the instance of Post’s correspondence problem
has a solution.

Proof.

with$(\Rightarrow)$$1\leq j\leq n$

The term $f(a, b)$ can be reduced only by the use of rewrite rules annotated. Then we obtain$f(a, b)\supset_{R}^{+}f(\alpha:_{1}(\alpha_{2}.\cdot\cdots\alpha:_{k}(a)\cdots), \sqrt{}^{_{1}}(\sqrt|.2\ldots\sqrt\dot{.}k(b)\cdots))$

for some , , , . Now one can apply only rewrite rules annotated with either $n+1$ or$n+2$ , and then apply only the rules annotated with either $n+3$ or $n+4$ . The right-handside is here reduced to $f(c, d)$ ffom the assumption, which implies thatfrom the definition of rules annotated with $n+1,n+2,n+3,n+4$ .
, , . We now havefor some
Assume that$i_{1}$$i_{2}$$\ldots$$i_{k}$$\alpha:_{1}\alpha_{2}.\cdot\cdots$$\alpha_{k}.\cdot=$$\sqrt i_{1}\sqrt.\cdot 2\ldots\sqrt.\cdot k$$(\Leftarrow)$$\alpha:_{1}\alpha_{2}.\cdot\cdots\alpha_{\dot{1}_{k}}=\sqrt{}^{_{1}}\sqrt _{2}\cdots$ $\sqrt.\cdot k$$i_{1},i_{2}$$\ldots$$i_{k}$$f(a,b)=_{R}^{+}f(\alpha:_{1}(\alpha:_{2k}\cdots\alpha\dot{.}(a)\cdots),\sqrt.\cdot 1(\sqrt|.2\ldots\sqrt|.k(b)\cdots))$.

Then from the synchronized applications of rewrite rules annotated with either $n+1$ or$n+2$ , foUowing with either $n+3$ or $n+4$ , one eventually has$f(\alpha:_{1}(\alpha_{\dot{1}2}\ldots\alpha_{k}\dot{.}(a)\cdots),\sqrt{}^{_{1}}(\sqrt{}^{_{2}}\cdots\sqrt|.k(b)\cdots))=_{R}^{+}f(c, d)$since$\alpha:_{1}\alpha:_{2}\cdots\alpha:_{k}=\sqrt{}^{_{1}}\sqrt _{2}\cdots$$\sqrt\cdot.k$.

,$\square$110
Theorem 1The reachability problem for ground STRSs is undecidable.

Proof. Rom Lemma 3and [POs46].

$\square$

The theorem above says that it is unsolvable to determine whether the term $f(a, b)$ has
anormal form. In other words, it is undecidable to decide whether the STRS constructed
ffom PCP is weakly normalzing or not.
$R$

5Synchronization and TwO-Counter Automata
Two Counter Automata

5.1

Following [HU79, Sch97], we briefly introduce two counter automata.
tion on counters, and stands for astates of counters, as follows:{ $NOP$,INC, $DEC$ }:operations on counters$T\in \mathcal{T}=\{Z, NZ\}$ :states of acounter$O$denotes an opera-$T$$\mathrm{O}\in O$$=$

AtwO-counter automaton is defined by an off-line Turing machine with two counters,

as foUows:
Two Counter Automaton$\langle Q, q., q" \delta,C_{1}, C_{2}\rangle$$\bullet$:aset of states including an initial state-step deterministic function from:a$Q$$\delta$$\mathrm{n}\mathrm{a}\mathrm{t}$$q_{l}$

and afinal statesuch thatto$q_{f}$$\mathcal{T}^{2}\mathrm{x}Q$$O^{2}\mathrm{x}Q$$\langle T_{1},T_{2},q\rangle\ovalbox{\tt\small REJECT}\mapsto\iota(O_{1},O_{2},\phi\rangle$$C_{1}$,$C_{2}$:two counters denoting natural numbers

An instantaneous description of the two counter automaton is defined asfollows:
Instantaneous description of the automaton (ID), where $n_{t},n_{}’\in N$;FinalStarting$\langle C_{1}, C_{2}, q\rangle$, as$\bullet$$(n_{1},n_{2},q)\ovalbox{\tt\small REJECT}\mapsto s(n_{1}’,\mathrm{n}_{2}’$$\phi\rangle$$\mathrm{I}\mathrm{D}:(0,0,q_{f}\}$$\mathrm{I}\mathrm{D}:(0,0,q.\rangle$

For atechnical reason, without loss of generality we have the following assumption (A):), then there is no transition such that
If
,
, or
,
.
(
for
is uniquely
Remarked that the assumption guarantees that ($(q,\phi)$.
determined by the pair of the two states$\langle T_{1},T_{2},q_{1}\rangle\mapsto s\langle O_{1},O_{2},q_{2}$$T_{1}’,T_{2}’,q_{1}\rangle\mapsto s(U_{1}, U_{2},q_{2})$$T_{1}\neq T_{1}’$$T_{2}\neq T_{2}$$O_{1}\neq\sigma_{1}$$O_{2}\neq\sigma_{2}$$T_{1},T_{2},q\rangle\vdash\nu_{\delta}\langle O_{1},O_{2},\phi\rangle$

Theorem 2([Min61, Fis66, HU79])
A twO-counter automaton can simulate an arbitrary Turing machine.

5.2

Encoding of$\mathrm{C}_{2}$-Automata via Synchronized Ground TRS

ounter automata via ground TRS, because one
It is, in general, impossible to encode
has Theorems 2while ground TRSs have less computational power than Turing machine.
$\mathrm{t}\mathrm{w}\triangleright$

111First we observe what is the essential distinction between tw0-counter automata and ground
TRSs. Filling the deep gap naturally leads to the notion of synchronized TRSs.
Following [Sch97], we use one bimy-function symbol , and constants 0, 1andfor $q_{j}\in Q$ , where. For aset , card(Q) denotes the cardinalty of the
set.
$f$

$q_{\mathrm{j}}^{1},q_{j}^{2}$$Q$$1\leq j\leq \mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}(\mathrm{Q})$$\bullet$$)$

Code of the transition :. For $j\in\{1, \ldots, k\}$ ,
Let
rules
$\delta$$\bullet$$\langle T_{1},T_{2},q_{1}\rangle\vdasharrow\langle O_{1}, O_{2},q_{2}\rangle$$k=\mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}(\mathrm{Q})$$\mathcal{R}$consisting of$\delta$

is coded as aunion of the two sets of the rewrite$=\mathcal{R}_{1}\cup \mathcal{R}_{2}=\{b_{j}^{1}arrow b_{j}^{\prime 1}|j=1, \ldots,k\}$$b\mathrm{j}$$arrow\theta j$$\cup\{b_{\dot{f}}^{2}arrow b_{\mathrm{j}}^{\Omega}|j=1, \ldots, k\}$$(i=1,2)$ which are defined based on (A), as follows:

Here, R. describes acomputation relating to the counter $i(i=1,2)$ . Now we can simulate
each transition of ID’s$\langle 0, 0, q_{s}\rangle\vdash+_{\delta}\langle n, n’, q\rangle\vdash+_{\delta}\cdots$

via the two steps rewriting denoted by$t_{\langle 0,0,q.\rangle}arrow_{\mathcal{R}}^{2}t_{\{\cdot*,n’,q\rangle}arrow_{\mathcal{R}}^{2}\cdots$

Lemma 4If we have$arrow_{\mathcal{R}}^{2}$.

$\langle n_{1},n_{2}, q_{1}\rangle|arrow_{\delta}\langle n_{1}’,n_{2}’, q_{2}\rangle$, then$t_{(n_{1},\mathfrak{n}_{2},q_{1})}arrow_{\mathcal{R}}^{2}t_{\langle n_{\acute{1}},.*_{\acute{2}},q_{2}\}}$.

Proof. Rom the case analysis on the definition of the implementation of .
$\delta$

Proposition 2
A twO-counter auto maton stops, then$\square$$f(f(0,q_{s}^{1}),f(0,q_{s}^{2}))arrow_{\mathcal{R}}^{\mathrm{P}}f(f(0, q_{f}^{1}),f(0,q_{f}^{2}))$.

Proof. Rom Lemma 4.

$\square$Noted that the inverse direction of Proposition 2is not true in general. For instance,:take the$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\dot{\mathrm{w}}\mathrm{n}\mathrm{g}$$\delta$$\delta$$=\{\langle NZ,NZ,q_{2}\rangle\mapsto_{\delta_{4}}\langle DEC,DEC,q_{f}\rangle\langle NZ,NZ,q_{1}\rangle\mapsto_{\delta_{2}}\langle NOP,NOP,q_{2}\rangle\langle Z,Z,q_{s}\rangle|arrow_{\delta_{1}}\langle INC,NOP,q_{1}\rangle,,$$\langle NZ,NZ,q_{3}\rangle\mapsto_{\delta_{5}}\langle DEC,DEC,q_{f}\rangle\langle NZ,Z,q_{1}\rangle\vdash\succ_{\delta_{3}}\langle NOP,INC,q_{3}\rangle,\}$,Then we obtain the expected transitions:$\langle 0, 0, q_{s}\rangle\vdasharrow\delta_{1}\langle 1,0,q_{1}\rangle\vdash*_{\delta_{3}}\langle 1,1,q_{3}\rangle\vdash+_{\delta_{5}}\langle 0,0,q_{f}\rangle$

However, not only this but also the following can be obtained by the rewriting$f(f(0,q_{s}^{1})$,$f(0, q_{s}^{2}))arrow_{\mathcal{R}}^{2}f(f(0,f(1, q_{1}^{1})), f(0, q_{1}^{2}))$$arrow_{\mathcal{R}}f(f(0, f(1,q_{2}^{1})),f(0,q_{1}^{2}))arrow_{\mathcal{R}}f(f(0, f(1,q_{2}^{1})),f(0, f(1,q_{3}^{2})))$$arrow_{\mathcal{R}}f(f(0, q_{f}^{1}),f(0, f(1,q_{3}^{2})))arrow_{\mathcal{R}}f(f(0,q_{f}^{1}),$ $f(0,q_{f}^{2}))$$\prec_{\mathcal{R}}$:112
which cannot give an ID. In order to obtain the inverse direction, it is not enough to make asimple union of the two rewriting systems; we need amechanism of synchronization between
Now we define asynchronized ground TRSand &the two rewrite rules, f
and 74, as follows:over$\ovalbox{\tt\small REJECT} \mathrm{X}$$\ovalbox{\tt\small REJECT} \mathrm{r}$.

$b!\ovalbox{\tt\small REJECT}$$bl^{1}$$\ovalbox{\tt\small REJECT}$$\ovalbox{\tt\small REJECT}_{Z}$$\mathcal{R}^{s}=\{s_{j} :$\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT} f$

1.

$\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT} f$b_{j}^{1}arrow b_{j}^{\prime 1}|j=1, \ldots,k\}\cup\{s_{j} :b_{j}^{2}arrow b_{j}^{\prime 2}|j=1, \ldots, k\}$,where the rewrite rules with the same annotation can be applied in parallel, which means
be implemented by synchronous rewritingthat the synchronization of the two counters
and .
over
It is remarked that in Schubert’s encoding via second-0rder unification [Sch97, Sch98],
plays arole of the synchronization for the two counters.
the coordination equation (We now have the inverse direction of Proposition 2in the following sense:$s_{j}$$\mathrm{c}\mathrm{a}.\mathrm{n}$$\mathcal{R}_{1}$$\mathcal{R}_{2}$$s_{4},u_{4}\rangle$

Proposition 3

If.

$f(f(0, q_{l}^{1}),f(0,q^{2}.))3_{\mathcal{R}}’$

Proof. If we have$f(f(0,q_{f}^{1}),$ $f(0,q_{f}^{2}))$.

$t\{n1,||2,q_{1}\}\Rightarrow \mathcal{R}$$t\mathrm{t}^{n_{\acute{1}}.\pi_{\acute{2}}},oe$, then a twO-counter automaton stops.

), then$(n_{1},n_{2},q_{1}\rangle\vdash*\iota(n_{1}’,n_{2}’,q_{2}\rangle.$$\square$

Theorem 3A ground STRS can simulate an arbitrary Turing machine.
The reachability problem is undecidable for ground STRSs.

Proof. We can also establish the same statement as Proposition 2with respect to,$=_{\mathcal{R}\square }^{*}.$

and ffom Proposition 3and Theorem 2.

References[BN98] Baader, R. and T. Nipkow: Term Rewiting and All That, Cambridge University
Press, 1998.
[Fis66] Fischer, P. C.: Turing Machines with Restricted Memory Access, Information andControl 9, pp. 364-379, 1966.
[Hue80] Huet, G. :Confluent Reductions: Abstract Properties and Applications to Term
Rewriting Systems, Journal of the Association for Computing Machinery, Vol. 27,
No. 4, pp. 797-821, 1980.

[HU79] Hopcroft, J. E. and J. D. UUman: In rroduction to Automata Theory, Languages
and Computation, Addison-Wesley, 1979.
[K1092] Klop, J. W.: Term Rewriting Systems, Handbook of Logic in Computer ScienceVol. 2, Oxford University Press, Pp. 1-116, 1998.
[Min61] Minsky, M. L.: Recursive Unsolvability of Post’s Problem of “TAG” and Other
Topics in Theory of Turing Machines, Annals of Mathematics, Vol. 74, No. 3, pp.
437-455, 1961.

113[NT99] Nagaya, T. and Y. Toyama: Decidabilty for left-linear growing term rewriting
70,1999.
systems, Lecture Notes in Computer Science 1631, PP.
$256\ovalbox{\tt\small REJECT}$[Oya90] Oyamaguchi, M.: The Reachability and Joinabilty Problems for Right-GroundTerm-Rewriting Systems, Journal of Information Processing, Vol. 13, No. 3, pp.
347-354, 1990.
[OS99] Ohshima, A. and T. Sffibe: Design of the Interpreter for Metaterm Rewriting
Calculus with Dynamic Discrimination Nets, Technical Report of IEICE, SS99-61,
pp. 9-16, 1999 (in Japanese).
[POs46] Post, E. L.: Avariant of recursively unsolvable problem, Bulletin of the American
Mathematical Society, Vol. 52, No. 4, pp. 246-268, 1946.
[Sch97] Schubert, A.: Second-0rder unification and type inference for Church-style, Tech.
Report TR 97-02 (239), Institute of Informatics, Warsaw University, January 1997.

[Sch98] Schubert, A.: Second-0rder unification and type inference for Church-style, Proc.
ACM Symposium on Principles of Prog ramming Languages, pp. 279-288, 1998.
[TN83] Togashi, A. and S. Noguchi: Some Decision Problems and Their Time Complexity
for Term Rewriting Systems, The Institute of Electronics, Information and Cornrnunication Engineers Transactions on Information and Systems, Vol. J66-D, No. 10,
pp. 1177-1184,1983 (in Japanese).