数理解析研究所講究録
918 巻 1995 年 85-98

85Transforming Termination by Self-LabellingMaria$\mathrm{C}.\mathrm{F}$. Ferreira1
1

Aart Middeldorp2

Hans Zantema1

Hitoshi Ohsaki2

Department of Computer Science, Utrecht University. Box 80.089, 3508 TB Utrecht, The Netherlands$\mathrm{P}.\mathrm{O}$2Institute of Information Sciences and Electronics
University of Tsukuba, Tsukuba 305, Japan

June 8, 1995
ABSTRACT
We introduce a new technique for proving termination of term rewriting systems. The]
of Zantelna’s semantic labelling technique, is especially useful fortechnique, aof transformation methods that attempt to prove termination bycorrectness
establishing theier to prove. We
into systems whose termination isrewritingtransforlning
apply the technique to distribution elimination, dummy elimination, and currying, resulting
in shorter correctness prook, stronger results, and a positive solution to an open problem.
$\mathrm{i}_{\mathrm{Z}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{a}$$\mathrm{t}\mathrm{e}\mathrm{r}\ln$1.

$\mathrm{s}\mathrm{y}\mathrm{s}\iota \mathrm{e}\mathrm{l}\mathrm{n}\mathrm{S}$$\mathrm{e}\mathrm{a}s$

Introduction

Termination is an undecidable property of term rewriting systems. In the literature (Dershowitz[2] contains an earlv survey of termination techniques) several methods for proving termination
are described that are quite successful in practice. We can distinguish roughly two kinds oftermination methods:(1) basic methods like recursive path order and polynomial interpretations that apply directly
to a given term rewriting system, and(2) methods that attempt to prove termination by transforming a given term rewriting system
into a term rewriting system whose termination is easier to prove, e.g. by a method of thefirst kind, and implies termination of the given system.
Transformation orders (Bellegarde and Lescanne [1]) and distribution elimination (Zantema [8])are examples of methods of the second kind. Semantic labelling (Zantema [7]) is a very powerful
method of this kind. The stalting point of the present paper is the observation that semanticlabelling is in a sense too powerful. We show that any terminating term rewriting system canbe transformed by semantic labelling into a system whose termination can be shown by therecursive path order. The proof of this result gives rise to a new termination method which wename self-labelling. We show that self-labelling is especially useful for proving the correctnessof termination methods of the second kind:

86

.
.
.

Using self-labelling we give a positive solution to an open problem in [8] concerning distribution elimination: right-linearity is not necessary for the correctness of distribution elimination in the absence of distribution rules. The proof reveals how to improve distribution
elimination in the absence of distribution rules.
Using self-labelling we give an alternative proof of the correctness of dummy elimination, a
recent transformation method of Ferreira and Zantema [3]. From the proof we infer how tolift the restriction that the symbol to be eliminated may not occur in the left-hand sides of
the rewrite rules.
Using self-labelling we give a short proof of the main result of Kennaway, Klop, Sleep, andDe Vries [4] stating the correctness of currying, which for the purpose of this paper we viewas a termination method of the second kind.
The proofs of the above results are remarkably similar.
The remainder of this paper is organized as follows. In the next section we recapitulatesemantic labelling. In Section 3 we show that every terminating term rewriting system can betransfornled bylabelling into a term rewriting system whose termination is very easy
to prove. This completeness result gives rise to the self-labelling technique. In Section 4 weuse self-labelling to solve the conjecture concerning distribution elimination. The self-labelling
proof gives rise to a stronger result, which we explain in Section 5. In Section 6 we observe how
self-labelling can be used to show the correctness of an extension of dummy elimination. Our
final illustration of the strength of self-labelling can be found in Section 7 where we present a
short proof of the preservation of termination under currying.
$\mathrm{s}\mathrm{e}\mathrm{n}\mathrm{u}\mathrm{a}\mathrm{n}\mathrm{t}\mathrm{i}_{\mathrm{C}}$

Preliminaries

2.

We assume the reader is faniiliar with the basics of term rewriting (as expounded in, e.g., Klop
[5] . This paper deals with the termination property. A term rewriting system (TRS for short)
is said to be terminating if it doesn’t admit infinite rewrite sequences. It is well-known
is terminating if and only if there exists a reduction order–a well-foundedthat a TRS
order that is closed under contexts and substitutions–onthat orients the rewrite rulesof from left to right. Another well-known fact states thatis a well-founded orderonfor any terminating TRS. Hereif and only if is a proper subterm of .
is in general not a reduction order as it lacks closure under contexts.
Observe thatIn this preliminary section we briefly recall the ingredients of semantic labelling (Zantema[7] . Actually we present a special case which is sufficient for our purposes. Let
be aan -algebra. Let
be a well-founded order on the carrier of
TRS and$(A,\succ)$. We say that the pairis a quosi-model forifof every function symbol
the interpretation
is weakly monotone (with respect toin all its coordinates, andfor every rewrite ruleand assignment. Heredenotes$)$$(F,\mathcal{R})$$(\mathcal{F}, \mathcal{R})$$T(\mathcal{F}, \mathcal{V})$$(arrow\tau_{\mathrm{L}}’\cup\triangleright)^{+}$$\mathcal{P}\sim$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$s\triangleright t$$(\mathcal{F}, \mathcal{P}_{\mathrm{c}})$

$t$

$s$

$(arrow r_{\backslash }\cup\triangleright)^{+}$

$)$

.
.

$(\mathcal{F},\mathcal{R})$$A=(_{A}4, \{f_{A}\}f\in \mathcal{F})$$\mathcal{F}$$A$$\succ$$A$$(\mathcal{F}, R)$$f_{A}$$f\in \mathcal{F}$$\succ)$$[\alpha](l)\succ_{\Gamma}[\alpha](r)$$larrow r\in \mathcal{R}$$\alpha:\mathcal{V}arrow A$$[\alpha]$

87

the unique homomorphism from$\mathcal{T}(F, v)$

to $A$ that extends$\alpha$,$\alpha(t)$if$f_{A}([\alpha]\langle t1)\ldots.,$ $[\alpha](t_{n}))$

if $t=f(t_{1}, \ldots,t_{n})$ .

$[\alpha](t)=\{$$t\in \mathcal{V}$, i.e.,

The above takes care of the semantical content of semantic labelling. We now describe thelabelling part. We label function symbols from $F$ with elements of . Formally, we consider thehas the same arity as . For
and $a\in A$ } where eachlabelled signature
{
to
from
functionalabelling
inductively
defineevery assignment we
as follows:
$A$

$f$

$f_{a}$$f_{(I}|f\in \mathcal{F}$$\mathcal{F}_{lab}=$$lob_{\alpha}$$\alpha$if$t$$lab_{\alpha}(t)=\{$$f_{[\llcorner\backslash ](}t)(lclb_{\circ}(t1), \ldots , lab_{\mathrm{Q}}(tn))$$t\in \mathcal{V}$$T(\mathcal{F}, \mathcal{V})$$\tau(\tau_{la\iota}, v)$,

if $t=f(t_{1}, \ldots,t_{n})$ .

are simply labelled by the value (under the assignment ) of theasover the signatureandcorresponding subterms. We define the TRSs
follows:

So function symbols in$\alpha$$t$$dec(\mathcal{F}, \succ)$$\mathcal{P}\sim lab$$\mathcal{R}_{lab}$$=$$dec(\mathcal{F}, \succ)$

$=$

{
{

$l_{\mathrm{f}l}b_{C}(\backslash l)arrow lob_{\mathfrak{a}}(r)|larrow r\in \mathcal{R}$$f_{C1}(X_{1},$$\ldots$, $x_{n})arrow f_{b}(x_{1},$$\ldots,$and$\alpha:\mathcal{V}arrow A$$x_{n})|f\in \mathcal{F}$$\mathcal{F}_{lab}$},

and $a,b\in A$ with $a\succ b$ }.

The following theorem is a special case of the main result of Zantema [7].
be a $TRS,$
THEOREM 2.1. Let-modelcarrier of A. If $(A, \succ)$ is a.
of$(F, \mathcal{P}\iota)$$q_{1\partial S}i$

an
en

$A$
$tl_{1}$$\mathcal{F}$-alge , andtion of$t\mathrm{e}r\ln i\mathrm{n}\mathrm{a}$$\mathrm{b}r\mathrm{a}$$\succ$a well-foun $ded$ order on this uival en to termina tion$(\mathcal{F}, \mathcal{R})$

$e$

$t$

$\mathrm{e}q$$\square$$(\mathcal{F}_{lab}, \mathcal{R}lab\cup dec(\mathcal{F}, \succ))$

Observe that in the above approach the labelling part of semantic labelling is completely
determined bv the semantics. This is not the case for semantic labelling as defined in [7]. Theof [7] results in some quite impressive termination proofs. In thisadditional expressive )clear
that the special case of semantic labelling presented above is quite
paper we hope to makesuccessful as well.
$0\backslash \mathrm{Y}^{\tau}\mathrm{e}\Gamma$$\mathrm{I}$3.

Self-Labellingthat every terminating TRS can be transformed by semantic labelling
In this section we
into a TRS whose termination is very easily established. The proof of this result forms the basisof a powerful technique for proving the correctness of transformation techniques for establishing$\mathrm{s}\mathrm{l}_{1}\mathrm{o}\mathrm{W}$termination.
is called precedence terminating if there exists a well-founded
DEFINITION 3.1. A TRS
$F$
$(l)$
and every function symbol
such that root コ for every rewrite ruleorder コ on$(\mathcal{F}, \mathcal{P}_{1})$$f$$f\in Fun(r)$.

$larrow r\in \mathcal{R}$88

LEMMA 3.2. Every preceden ce terln ting $TRS$ is termi nating.
be a precedence terminating TRS. So there exists a well-founded order コ
PROO . Leton that satisfies the condition of Definition 3.1. An easy induction argument on the structure
is a reduction order, termination of. Sinceof reveals that コ rp0 for every
follows.
$i\mathit{1}1\mathrm{a}$$(\mathcal{F}, \mathcal{P}_{\mathrm{t}})$$\Gamma$$\mathcal{F}$

$l$

$r$

$larrow r\in \mathcal{P}_{1}$$r$$\text{コ_{}rpo}$$\square$$(\mathcal{F}, \mathcal{R})$The next result states any terninating TRS can be transformed by semantic labelling intoa precedence ternuinating TRS.
THEOREM 3.3. For every term tingis receden ce rmina ting.
$i\mathrm{n}\mathrm{a}$$(\mathcal{F}_{lab}, \mathcal{R}_{lb}a\cup dec(\mathcal{F}, \succ))$$TRS(\mathcal{F},\mathcal{R})tl_{1}e\mathrm{r}e$exists a qua si-model $(A, \succ)sucl_{1}$ that

$te$

$p$

with the well. We equip
we take the term algebra
PROOF. As -algebra. (Well-foundedness is an immediate consequence of termination of 72.)
founded order
Because rewriting is closed under contexts, all algebra operations are (strictly) monotone inare substitutions andall their coordinates. Because assignments in the term algebra. It remains to show
rewriting is closed under substitutions, $(A, \succ)$ is a quasi-model foris precedence terminating. To this end we define a well-foundedthat. Let $larrow r$ be a rewrite rule ofコ
if and only if
as follows:order on$A$$\mathcal{F}$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$\succ=arrow r_{\backslash }+$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$(\mathcal{F}, \mathcal{R})$$(\mathcal{F}_{lab}, \mathcal{P}\iota lab\cup cleC(F, \succ))$.
.

$f_{s}$$\mathcal{F}_{lc\iota b}$$\text{コ}$$\mathcal{P}\sim lab\cup deC(\mathcal{F}, \succ)$$s(arrow n\cup\triangleright)^{+}t$$\mathit{9}t$.

and a rewrite rulethen there exist an assignmentIf$(l)$$r=lab_{\alpha}(r’)$$l=lab_{\alpha}(l’)$. Let be the
is
of
root
. The label
andsuch thatlabel of a function symbol in . By construction $\ell=[\alpha](t)=ta$ for some subterm of .
?
. So root $(l)$ コ for every $f\in Fun(r)$ .
Hence. Clearly
If $larrow r\in c/eC(F, \succ)$ then $l=f_{s}(x_{1}, \ldots, x_{n})$ and $r=f_{t}(x_{1}, \ldots, x_{n})$ with$larrow r\in \mathcal{P}\iota_{lab}$$l’arrow r’\in \mathcal{R}$$\alpha:\mathcal{V}\neg \mathcal{T}(\mathcal{F}, \mathcal{V})$$[\alpha](l^{J})=l’\alpha$

$l$

$t$

$r$

$l’aarrow\tau\backslash ’$

$r’$

$f$

$\prime a\underline{\triangleright}\ell$$sarrow \mathcal{R}+t$$root(l)=f_{S}$ コ$f_{t}$.

$\square$

The particular use of semantic labelling in the above proof (i.e., choosing the term algebra as
semantics and thus labelling function symbols with ternus) is what we will call self-labelling. One
may argue that Theorem 3.3 is completely useless, since the construction of the quasi-model inis terminating. Nevertheless, in the following sections wethe proof relies on the fact thatwill see how self-labelling gives rise to many new results and significant simplifications of existing
results on the correctness of transformation techniques for establishing termination. Below wesketch the general framework.
on TRSs, designed to make the task of proving termination
be aLeteasier. The question is how to prove correctness of the transformation, i.e., does termination of? Let
be theimply termination of the given TRS
the transformed TRS. This is achieved. The basic idea is to label the TRS
with terms of
TRS
by executing the following steps:
into an -algebra by choosing suitable interpretations forturn the term algebra(and taking term construction as interpretation of the function
the function symbols in),symbols in$(i^{\Gamma}, \mathcal{P}_{1})$$\Phi$$\mathrm{t}1\mathrm{a}11\mathrm{s}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$$(\mathcal{F}, \mathcal{R})$$\Phi(\mathcal{F}.\mathcal{P}_{\mathrm{t}})$.

$(\mathcal{F}, \mathcal{R})$$(\mathcal{F}’, r_{\mathrm{t}}’)$$T(F^{\prime,v)}$$F\backslash \mathcal{F}’$$\mathcal{F}\cap \mathcal{F}’$$\mathcal{F}$$A$$(\mathcal{F}’, \mathcal{R}’)$$\Phi(F,\mathcal{R})$

89

..
..

, and
equip the -algebra with the well-founded.
コ
if and only if
as follows:
define the well-founded order onNow, if we can show that$(A, \succ)$ is a quasi-model for, andis precedence terminating with respect to ,the TRSand thus the correctness of the transformation is a consequencethen termination ofof Theorem 2.1.
only creative step in this scheme is the choice of the interWe would like to stress thatpretations for the function symbols that disappear during the transformation . All our proofs
will follow the above scheme, except that in Section 7 we have to consider a slight refinement of
the well-founded order on the labelled signature in order to conclude precedence termination.
$A$$\mathcal{F}$$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\succ=arrow \mathcal{R}+,$$\text{コ}$$f_{s}$$\mathcal{F}_{lab}$$s(arrow\pi^{r}\cup\triangleright)^{+}t$$g_{t}$$(F,\mathcal{P}_{1})$$(\mathcal{F}lab, \mathcal{P}\iota lab\cup dec(\mathcal{F}, \succ))$$\text{コ}$$\Phi$$(\mathcal{F}, \mathcal{P}_{7}\vee)$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$$\Phi$

4.

Distribution Elimination

Our first application of self-labelling is the proof of a conjecture of Zantema [8] concerning
distribution elimination.
be a designated function symbol whose arity is at least
be a TRS and letLetone. A rewrite rule $larrow r\in R$ is called a distribution rule for if $l=C[e(X_{1}, \ldots,x_{n})]$ and$r=e(C[X_{1}], \ldots, c[x_{n}])$ for some non-empty context
in which doesn’t occur and pairwise
is a technique that transforms,
elimination. Distributiondifferent variables
by eliminating all distribution rules for and removing the symbol from the right-hand sides
that assigns to every term inof the other rules. First we inductively define a mapping,
as follows:
subset ofa$e\in \mathcal{F}$$(\mathcal{F},\mathcal{P}_{1})$

$e$

$C$

$x_{1},$ $\ldots$$e$$(\mathcal{F}, \mathcal{R})$$x_{n}$$e$$e$$E_{distr}$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$T(\mathcal{F}\backslash \{e\}, \mathcal{V})$$\mathrm{n}\mathrm{o}\mathrm{n}- \mathrm{e}\mathrm{m}_{1)}\mathrm{t}\mathrm{y}$if$\{t\}$$E_{distr}(t)=$,if $t=e(t_{1}, \ldots,t_{n})$ ,$i=1\cup E_{diStr}(t_{i})n$$\{f(s_{1}, \ldots .

$t\in \mathcal{V}$s_{n})|s:\in E_{dis1r}(t_{i})\}$

if $t=f(t_{1}, \ldots,t_{n})$ with $f\neq e$ .

$\mathrm{Y}$is illustrated in Figure 1, where we assume that the numbered contexts do
The mapping
not contain any occurrences of . It is extended to rewrite systems as folIows:$E_{distr}$$e$$E_{distr}(\mathcal{P}_{\vee})=${$l-r’|larrow r\in \mathcal{P}_{1}$is not a distribution rule for$e$and $r’\in E_{disir}(r)$ }.

if and only if does not occur in the left-hand sides
Observe that does not occur in
not
rules
of
are
distribution
rules for .
of rewrite
One of the main result of Zantema [8] is stated below.
$E_{distr}(\mathcal{P}\sim)$

$e$

$e$

$\mathcal{P}_{1}\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{a}\mathrm{t}$$e$be a $TRS$ 11 let $e\in F$ be a on-const ant symbol which does not
THEOREM 4.1. Let {adistribu tion rules for .
rules ofoccur in $tl1e$ left,-l] $al1dsi(l$ es ofis terlila
and righ t-li
tllen is termin ating.
(1) Ifis simply terminating.
is SiJJlterm ting andear(2) Iftotallyerminating.
isterminaenis(3) Ifting
72.
$\mathcal{F},$$a$$\mathcal{P}\iota)$$d$$\mathrm{n}$$\cdot$$\mathcal{R}tl_{1}\mathrm{a}t$$re1\prime \mathrm{V}\mathit{1}i\mathrm{r}.e$$E_{diStr}(\mathcal{P}_{1})$$ne\mathrm{a}r$$ti1\mathit{1}g$$E_{dis\{}r(\mathcal{P}_{\mathrm{t}})$$pl_{\mathrm{V}}$$E_{d}\cdot tr(|S\mathcal{P}_{1})$$totall_{1^{f}}$$i11\partial$$rigl_{1}t- li\mathrm{n}$$tl_{1}$$re\mathit{1}1ot$$\mathcal{R}$$tl_{1}en\mathcal{R}$

$t$

$e$

90

$t=$

FIGURE 1.
$\square$

The following example from [8] shows that right-linearity is essential in parts (1) and (2).
EXAMPLE 4.2.

$(_{\mathrm{o}\mathrm{n}\mathrm{S}}^{-\{},- \mathrm{i}\mathrm{d}\mathrm{e}\mathrm{r}$the TRS$\mathcal{P}_{1}=$ .
The last two rules are distribution rules forfirst rule. The TRS

$e$

and

$e$

$=–$
$E_{distr}(\mathcal{P}\mathrm{t})=\{f(\mathrm{f}f(a_{l},’ b,\cdot X,’.\cdot.\cdot \mathrm{t}f(\mathrm{f}l.b.?f(a.b,x,\mathrm{t}.\cdot.))b,x_{\backslash }j’\iota\tau\cdot))$

is easily shown to betermination andan infinite reduction in$f(\backslash \cdot.\cdot xf(\mathrm{t}.,’ x,b,’ a)f(\mathrm{t},X,af(X,X,a,a)\backslash x,b,bb))\}$

does not occur in the left-hand side of the.

. It is even simply terminating since for length-preserving TRSs
ation coincide. Nevertheless, the term $f(a,b, e(a, b), e(a, b))$ has$\mathrm{t}\mathrm{e}\mathrm{l}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}_{1}1\mathrm{g}$$\mathrm{s}\mathrm{i}\mathrm{n}\mathrm{l}\mathrm{p}\mathrm{l}\mathrm{e}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{n}\mathrm{l}\mathrm{i}_{11}$$\mathcal{P}_{1}$.

In [8] it is conjectured that in the absence of distribution rules for the right-linearity
assumption in part (1) of Theorem 4.1 can be omitted. Before proving this conjecture with the)technique of. wethat a similar statement for simple termination doesn’t hold,i.e., right-linearity is essential ill part (2) of Theorem 4.1 even in the absence of distribution rules
for .
$e$

$\mathrm{s}\mathrm{e}\mathrm{l}\mathrm{f}- \mathrm{l}\mathrm{a}\mathrm{l}$$‘ \mathrm{s}11\mathrm{O}\backslash \backslash$$\mathrm{c}\mathrm{l}\mathrm{l}\mathrm{i}\mathrm{l}\mathrm{l}\mathrm{g}$$e$EXAMPLE 4.3. Let
consist of the first rule of the TRS of Example 4.2. Simple terminationof
was established in Example 4.2, but
fails to be simply terminatingas $s=f(a, b, e(a, b).c(a, b))arrow\Gamma_{\vee}’f(e(c\iota,b),$ $e(a, b),$ $e(a, b),$ $e(a, b))=t$ with embedded in .
(Ternlination offollows from Theorem 4.4 below.)$\mathcal{P}_{1}’$$\mathcal{R}$$E_{diStr}(’\mathcal{R}’)=E_{di_{S}t?}.(\mathcal{P}\mathrm{t})$$\mathcal{P}_{1}’$$s$$\mathcal{P}_{1}’$

$t$

91

be a non-constant symbol which does
be a $TRS$ 11 let
THEOREM 4.4. Letisis terminating then.
Ifand sides of re write les of
not occur interm in a ting.
into an -algebra $A$ by defining
PROOF. We turn the term algebra$a$$(\mathcal{F}, \mathcal{P}_{\mathrm{t}})$$tl_{1}eleft- l_{1}$$d$$e\in \mathcal{F}$$\mathcal{T}\{F\backslash \{c\},$$\mathcal{R}$$E_{distr}(\mathcal{R})$$\mathcal{R}$$\mathrm{r}u$$\mathcal{F}$$\mathcal{V})$$e_{A}(t_{1}, \ldots, \dagger_{n})=f_{\pi}$. Here is an arbitrary but fixed element of $\{1, \ldots, n\}$ .
for all terms
is simply projection onto the -th coordinate. We equip $A$ with the well-founded orderSo
if and only if
as follows:
and we define a well-founded order コ on
and that the. We have to show that $(A, \succ)$ is a quasi-model foris precedence terminating with respect to コ.
TRS$(A,\succ)$
iseasy to see that
. It isis a quasi-model forFirst we show thatweakly monotone in all its coordinates. All other operations are strictly monotone in all theiris closed under contexts). Let be the identity assignment fromcoordinates (asfor all terms. An eas.v induction proof shows thatto . We denote. Also the following two properties are easily
and a signlllent,\o:thenand (2) if: (1)ofshown by induction on the$t’\inE_{/istr}‘(t)$
.
that
such
a
term
existsthere
and $E_{tl}iStr(f)=\{t\}$ . For the induction step we distinguish two cases.
then(1) If. We have
and
then
If
. If $t=f(t_{1}, \ldots,t_{n})$ with $f\neq e$according to the induction hypothesis. Henceancl $E_{(Tislr}(t)=\{.f(s_{1}, .. , , s_{n})|s_{i}\in E_{distr}(ti)\}$ . The induction
thenfor all $i=1,$ . . . Hence also in this case we obtain the
hypothesis vields.
desired.
the statenlent follows from property (1) because we can take(2) Observe that for.
$t=f(t_{1},\ldots,t_{n})$takes care of the base of the induction. Suppose
This. observation)))of . so is a subterm of for some $k\in\{1, \ldots, n\}$ . Fromaand let be). Again wesuch that
we obtain a term
the induction
and thus we can take $t’=t_{k}’$ .
distinguish two cases. If.
then $E_{distt}.(t)=\{f(s_{1}, \ldots , s_{n})|s_{i}\in E_{distr}(t_{i})\}$. Let
If.
Clearly
Using propertv (1) . infer that$larrowr$
an arbitrary assignment.
rewrite rule ofbe an
Now let.
and henceinoccur
doesn’t.
andSince
We haveand, the rule
. Therefore
belongs to
Because.
thus also
is precedence terminating with respect tothat
It remains to. We distinguish two cases. If $larrow r\in R_{lab}$
rule inコ. Let $larrow r$ be asuch thatand a rewrite rule
an assignment
then there$(l)$$l=lab_{\alpha}(l’)$ andthelabel of a
.
Let
be
is
. The label of root
for some subterm of . According toin . By construction
function. By construction $l’arrow r”\in E_{distr}(\mathcal{R})$ .
of ,
is a
property (2) above,for every $f\in Fvn(r)$ . If $larrow r\in dec(\mathcal{F}, \succ)$ then
. So rootHence)$t_{1},$$t_{n}\in \mathcal{T}(\mathcal{F}\backslash \{e\}, \mathcal{V})$$\pi$$\ldots,$$\tau_{1}$$e_{A}$$f_{S}\text{コ}gt$$\mathcal{F}_{lab}$$\succ=arrow E_{d_{ts}\iota r^{(\mathcal{P}\backslash )}}+$$s(arrow_{E_{di_{St}r}}(r\backslash )\cup\triangleright)^{+}t$$(.\mathcal{F},\mathcal{R})$$(\tau_{lab}, \mathcal{P}\iota lab\cup dec(:F, \succ))$$\mathrm{v}\mathrm{e}\mathrm{r}\dot{\mathrm{y}}$$(\mathcal{F}, \mathcal{R})$$e_{A}$$\mathcal{V}$$\epsilon$$-_{E_{di_{\vee}}}\mathrm{S}i^{-\mathrm{t})}’ \mathcal{P}\iota$$\mathcal{V}$$[\alpha](t)=\langle t\rangle\alpha$$[^{c}.](\dagger)\dagger)\^{r}\langle t\rangle$$t\in \mathcal{T}(\mathcal{F}, v)$$\mathcal{V}-\tau_{(}\mathcal{F}\backslash \{e\},$$‘\backslash$$\mathcal{V})$$t\in \mathcal{T}(\mathcal{F},$$‘\backslash \mathrm{t}\mathrm{l}\cdot \mathrm{t}\mathrm{l}\mathrm{c}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{e}$$\langle t\rangle\in E_{distr}(t)$$v\mathrm{I}$$s\underline{\triangleleft}t$$\langle.\underline{\mathrm{q}}\rangle\underline{\triangleleft}t’$$t\in \mathcal{V}$$\langle t\rangle=t$$t=e(t_{1}, \ldots, t_{\mathrm{t}},)$$E_{dis\dagger}r(t)= \bigcup_{i=1}^{n}E_{d}istr(t_{i})$$\langle t\rangle=\langle t_{\pi}\rangle$$\langle t_{\pi}\rangle\in E_{distr}(t_{\pi})$$\langle t\rangle\in E_{distr}(t)$$\langle t\rangle=f(\langle t_{1}\rangle\ldots , , \langle t_{n}\rangle)$$\langle t_{i}\rangle\in E_{diS}tr(f_{i})$

$n$

$,$

$,$

$\langle t\rangle\in E_{lj_{Sf}\uparrow}‘.(t)$$t’=’\langle t\rangle$$\backslash =t$$\mathrm{a}\mathrm{J}\mathrm{s}\mathrm{o}$$\mathrm{e}\Gamma \mathrm{s}\iota 11$

$s$

$1$

$\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{l}\mathrm{l}\mathrm{l}$

$t$

$s$

$\mathrm{r}\mathrm{o}_{1}$$t_{k}$$t_{k}’\in E_{disi\gamma}(t_{k})$$\mathrm{o}\mathrm{t}\mathrm{l}\mathrm{I}\mathrm{e},\backslash \mathrm{i}‘\backslash$$\mathrm{h}\mathrm{y}\mathrm{l}$$\langle s\rangle\underline{\triangleleft}t_{k}’$$f= \epsilon \mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{n}E_{distr}(t)=\bigcup_{i=1}^{n}E_{di}Str(t_{i})$$t’=f(\langle t_{1}\rangle, .

$f\neq C^{\lrcorner}$$t’\in E_{distr}(t\mathrm{I}\cdot$$\backslash \backslash ’ \mathrm{e}$$\mathcal{P}\sim \mathrm{a}\mathrm{l}\mathrm{l}\mathrm{d}\alpha:varrow \mathcal{T}(\mathcal{F}\backslash \{e\}, \mathcal{V})$$\mathrm{a}\mathrm{r}\mathrm{b}\mathrm{i}\mathrm{t}\Gamma \mathrm{a}\mathrm{r}\mathrm{V}\backslash$$[\mathfrak{a}](l)=\langle l\rangle\alpha$, ., t_{k}’, \ldots, \langle t_{n}\rangle)$$\langle s\rangle\underline{\triangleleft}t’$$\langle r\rangle\in E_{d?str}.(r)$

$l,$

$e$

$[\mathfrak{a}](\uparrow\cdot)=\langle r\rangle\alpha$$larrow\langle r\rangle$$[\alpha](l)=l\alpha$$\langle l\rangle=l$$E_{distr}(\mathcal{P}\iota)$$l\alphaarrow Edistr(\mathcal{R})\langle r\rangle\alpha$$[\mathfrak{a}](/)\succ_{\Gamma}[\zeta)](?\cdot)$$(\mathcal{F}_{/ab}.\mathcal{P}_{\mathrm{t}/}t\iota t)\cup\prime l_{CC}(\mathcal{F}, \succ))$$\mathrm{s}1\tau 0\backslash \backslash$$\mathcal{P}\mathrm{t}l‘ 1b\cup clcc(\tau, \succ)$$\mathrm{r}\mathrm{e}\backslash \backslash ’ \mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}$$l’arrow r’\in \mathcal{R}$$\cap:\mathcal{V}-\mathcal{T}(\mathcal{F}\backslash \{e\}, \mathcal{V})$$\mathrm{e}_{A}\mathrm{x}\mathrm{i}\mathrm{S}\mathrm{t}$$[\alpha](l’)=\langle l’\rangle\alpha=l’\alpha$$7^{\cdot}=lab_{\llcorner\backslash }(r’)$$\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{l}\mathrm{b}_{\mathrm{o}1}$$p=[\alpha](t)=\langle t\rangle\alpha$$r$$\langle t\rangle$$\mathrm{s}\iota 11_{\mathrm{J}}\mathrm{t}\mathrm{e}\Gamma\ln$$\gamma’’G\underline{\triangleright}p$$l’o!arrow E_{d\mathrm{i}St},$$\mathrm{t}\mathcal{P}\mathrm{c}$$\backslash \mathrm{o}\mathrm{n}\tau \mathrm{e}r\prime\prime\in E_{disuparrow}.(r)$$(l)\text{コ}f$$\ell$

$t$

$r’$

92

and $r=f_{t}(x_{1}, \ldots , x_{n})$ with

$l=f_{s}(x_{1}, \ldots, x_{n})$root $(l)=fs$ コ$f_{t}$.

$f\in \mathcal{F}$and $s\succ t$ . In this case we clearly have$\square$

The only creative element in the above proof is the choice ofverification of the two )obligations of self-labelling.

$e_{A}$. The rest is a routine$\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{f}$

$1$

5.

Distribution Elimination Revisited

In the proof of Theorem 4.4 we saw that we can take any projection function as semantics for .
)This freedom makes it possible to
distribution elimination (in the absence of distribution)
rules) by reducing theof rewrite rules inwhile preserving correctness of thetransformation.
What are the esselltialofthat make the proof of Theorem 4.4 work? A
careful inspection reveals, apart from the obvious termination requirement for, thefollowing two properties:
, and
(1)
(2) ifthenexists a terlllsuch that,for every. Below we define a new transformationthat satisfies these two
properties. The transformation is parallleterized by the
positions of the function$F$
symbol . The definition relies
the -algebra defined in the proof of Theorem 4.4 in that we$e$$\mathrm{i}\mathrm{m}_{1}$$\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}$$\mathrm{n}\iota\ln\urcorner 1$$E_{dis1}r(\mathcal{P}\iota)$$\mathrm{e}\mathrm{r}$$E_{di_{S}1r}$$\mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{I}^{)}}\mathrm{e}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{e}\mathrm{s}$$E_{diStr}(\mathcal{R})$$\langle t\rangle\in E_{dis\mathfrak{j}r}(t)$$t’\in E_{d?s\dagger r}(t)$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{r}\mathrm{e}$$s\underline{\triangleleft}t$$\langle s\rangle\underline{\triangleleft}t’$$t\in T(\mathcal{F}, \mathcal{V})$$E_{distr}^{\pi}$$\pi$$\mathrm{a}1^{\backslash }\mathrm{g}_{\mathrm{U}\mathrm{m}}\mathrm{e}\mathrm{n}\mathrm{t}$

$011$

$e$

use

$\langle t\rangle$.

DEFINITION 5.1. Let
least one. Fix{
to every term in$1,$$\pi\in$be a TRS and let
be a function symbol whose arity is at, arity $(c)$ } . ; inductively define mappings
andthat assigns
a subset of, as follows:$e\in \mathcal{F}$$(\mathcal{F}, \mathcal{P}_{1})$$\backslash t\backslash$$\phi$$\ldots$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$E_{dis1r}^{\pi}$$\mathcal{T}(\mathcal{F}\backslash \{e\}, \mathcal{V})$if$\emptyset$$\emptyset(t_{t\Gamma})\cup?.\neq\pi(\cup E_{distr}^{\pi}(t_{i}f\rangle)$$t\in \mathcal{V}$,

if $t=e(t_{1}, \ldots,t_{n})$ ,$\phi(t)=$if $t=f(t_{1}, \ldots,t_{n})$ with $f\neq e$ ,$\backslash \bigcup_{i=1}^{n}\varphi^{}(ii)$$E_{diS1r}^{\pi}(t)=\phi(\dagger)\cup\{\langle t\rangle\}$We extend the mapping$E_{di_{S}tr}^{\pi}(\mathcal{P}_{\mathrm{t}})=$

{

.

.

$E_{dstr}^{\pi}|$to$\mathcal{P}_{1}$as follows:$larrow r’|l-r\in \mathcal{P}_{1}$is not a distribution rule for

$e$

and

$r’\in E_{dis r}^{\pi}(r)$}.

Figure 2 shows the effect ofon the term of Figure 1. Observe that each
. andnunlbered context
exactly once in each set. The following lemma states thathas)
the two required.
$E_{distr}^{2}$$E_{dis\dagger?}^{1}$$t$$\mathrm{o}\mathrm{c}\mathrm{c}\mathrm{t}\mathrm{l}\mathrm{r}‘\backslash$$E_{distr}^{\pi}$$\mathrm{e}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{e}\mathrm{s}$$1^{)\mathrm{r}\mathrm{o}}1$

LEMMA 5.2. Let$(\mathcal{F}, \mathcal{P}_{\mathrm{t}})$be a$TRS_{C\tau 11}(l$

let

$e$

and

$\pi$

be as above. For every$t\in \mathcal{T}(F, v)$

we a $ve$$h$93$\triangle 5$$\triangle 7\}$$\triangle 2$$\triangle 4$$\triangle 6\}$

FIGU
(1)
(2) if$\langle t\rangle\in E_{dis\mathfrak{j}r}^{\pi}(f)$$\mathrm{R}\mathrm{E}2$

.

, and

.
exists a term $1lt’\in E^{\pi}(\{iiStrt)$ sncll aten
PROOF. The first statenlent holds by definition. The second statement we prove by induction. Ifthen the result follows from the first statement. Henceon the structure of. There. This is only possible if is a non-variable term
we may assume that
. The induction hypothesis yields a termsnchexists a. XVe distinguish two cases. Suppose $f=e$ . In this case we havesuch that$tl\iota$$tlle\mathrm{r}\mathrm{e}$$s\underline{\triangleleft}ttl1$$t\in \mathcal{T}(\mathcal{F}, \nu)$$\mathrm{c}\mathrm{v}=t$$\phi(t_{k})\cup\{\langle t_{k}\rangle\}$$f(t_{1}, \ldots,t_{n})$$t$$s\triangleleft t$$k\in\{1, \ldots, \uparrow?\}$$\langle s\rangle\underline{\triangleleft}t’$$t_{k}’\in E_{di_{St}r}^{\pi}(t_{k})=$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}.\sigma\underline{\triangleleft}t_{k}$$\langle.\underline{\sigma}\rangle\underline{\triangleleft}t_{k}’.$$E_{(;i}^{\pi} \mathrm{t}Str\dagger)=\mathrm{e}"(\dagger)\cup \mathrm{t}\langle t\rangle.\}=o(t_{\mathrm{T}}, )\cup\{\langle t\rangle\}\cup\bigcup_{i\neq\pi}E_{d}^{\pi}i\wedge str(ti)$.

. If $k\neq\pi$ thenIf $k=\pi$ then. Hence ill both cases we can take $t’=t_{k}’$ . Suppose $f\neq e$ . We have$t_{k}’\in\phi(t_{\pi}\rangle\cup\{\langle t_{k}.\rangle\}=\mathrm{c})(t_{\pi})\cup\{\langle t\rangle\}\subseteq E_{di_{S}}^{\pi}(t_{T}t)$$t_{k}’\in E_{di_{S1}r}^{\pi}(t_{k})\subseteq$$E_{dir}^{\pi}(stt)$.

$E_{d?s\iota}^{\pi}r1t)= \phi(t)\cup\{\langle t\rangle\}=\bigcup_{i=1}^{n}\emptyset(t_{i}.)\cup\{f(\langle t_{1}\rangle, \ldots, \langle t_{n}\rangle)\}$If$t_{k}’..\in \mathrm{c}\rho(t_{k}.)$thcll clearly$t_{\mathrm{A}}’\in F_{/iSt}^{\pi}‘.,.(t)$and hence we can take $t’=t_{k}’$ . If.

$t’=f(\langle t_{1}\rangle, \ldots, \langle t_{n}\rangle)\backslash \backslash r11\mathrm{i}_{\mathrm{C}}11,\backslash \mathrm{a}\mathrm{t}\mathrm{i}|\mathrm{s}\mathrm{f}\mathrm{i}\mathrm{e}\mathrm{S}\langle\underline{.\sigma}\rangle\underline{\triangleleft}i_{k}’\underline{\triangleleft}t’$

Hence we obtain the following resulta
THEOREM 5.3. Let { $F,$inleft-ll
and
sides
of
not occuristhen$\prime l^{\urcorner}RS$$\mathcal{P}\backslash .)|)\mathrm{e}$$tl_{1}e$$\pi\in\{1, \ldots, c\ell rity(\epsilon)\}$$\mathcal{P}_{1}$$\iota\cdot e$$\mathrm{r}\mathrm{e}\mathrm{r}\mathit{1}\mathfrak{n}\mathrm{j}_{\mathit{1}1}\mathrm{a}$EXAMPLE 5.4. Collsider the TRS
theTRS

The termination of$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$$\neg-$

the lines of the proof of Theorem 4.4.
$e\in \mathcal{F}$$\mathit{1}1(l$$\mathrm{r}$

$g$

TRS

$E_{disi}^{2}r(\mathcal{R})=$.

$a$

11 on-constant symbol$E_{distr}^{\pi}(\mathcal{R})$$\mathrm{w}h\mathrm{i}_{Ch}$is ermina ting for
$t$

does
$so\mathrm{m}e$$\square$$\mathcal{P}_{\mathrm{t}}=\{f(a)arrow f(e(a, b))\}$$f(a)f(l))\}$

then we take$\square$aletbewrite ules of 72. Iftin .

$\mathrm{n}\mathrm{o}\mathrm{n}- \mathrm{t}\mathrm{e}\mathrm{r}\mathrm{l}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}_{1\mathrm{l}}\mathrm{g}$$E_{dist\prime}(\mathcal{P}_{1})=\{f\langle af(\mathrm{r}\iota))$$\mathrm{a}1_{01\mathrm{l}}\mathrm{g}$$t_{k}’=\langle t_{k}\rangle$. Distribution elimination results in94

can be verified
of follows from$\mathrm{u}\mathrm{s}\mathrm{i}_{1\iota}\mathrm{g}$$\mathcal{R}$, e.g., the recursive path order with precedence $a\succ b$ . Hence termination. Observe that$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{l}\cdot \mathrm{e}\mathrm{l}\mathrm{l}\mathrm{l}5.3$$E_{dist}^{1}(r\mathcal{P}_{1})$fails to be terminating.

An obvious question is whether. works in combination with distribution rules, i.e., does
? The following example shows that the answer is negative.
Theorem 4.1 hold for$E_{dist?}^{\pi}$$F_{-dis\dagger}^{\pi}r$

EXAMPLE 5.5. Consider the non-terminating TRS$\mathcal{P}_{\mathrm{L}}=$ .
The TRSFor instance,$E_{dis1\}}^{\pi}.(\mathcal{P}\iota)$

is right-linear and$(\mathrm{s}\mathrm{i}\mathrm{n}\mathrm{l}])\mathrm{l}\mathrm{y}$$E_{dit}^{1}(sr\mathcal{P}_{\mathrm{t}})=$and totally) terminating for both choices of .
$\pi$

.

A natural question to ask is whether we need the as
in Theorems 4.4 and 5.3 that
does not occur in the left-hand sides of the rewrite rules in . In the proof of Theorem 4.4 thisassumption is only used to conclude thatthe left-hand side of a rewrite rule in
R). We need this identitv beca
thesides of rewrite rules inandare of therather than. Thisthat we can completely remove the restriction that
does not occur inleft-hand sides of rules in , provided we change
accordingly:$e$$\mathrm{s}\mathrm{u}\mathrm{m}_{1)}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$$\mathcal{P}_{\mathrm{t}}$$\langle l\rangle=\mathit{1}(\backslash \mathrm{v}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}/\mathrm{i}\mathrm{s}$$1\mathrm{e}\mathrm{f}\mathrm{t}- 1_{1}\mathrm{a}\mathrm{n}\mathrm{d}$$E_{distr}(\mathcal{R})$$11,\backslash \mathrm{e}$$E_{distr}^{\pi}(\mathcal{R})$$\mathrm{f}_{0}\mathrm{r}\mathrm{n}\mathrm{u}\mathit{1}$$\langle \mathit{1}\rangle$$\mathrm{i}\mathrm{m}_{1^{)}}1\mathrm{i}\mathrm{e}\mathrm{s}$$\mathrm{t}1_{1}\mathrm{e}$$e$$E_{d?st}^{\pi}(\mathcal{P}1)r=${$\mathcal{R}$$\langle l\rangle-t^{J}|l-\uparrow\cdot\in \mathcal{P}_{\vee}$and$E_{distr}^{\pi}(\mathcal{R})$$r’\in E_{di_{S}t}^{\pi},.(r)$}.

This extension is useful since it enables us to conclude the termination of a non-simply terminating TRS
by transforming it into the TRS$\mathrm{l}\mathrm{i}\mathrm{l}\backslash \mathrm{e}\mathcal{P}_{\mathrm{t}}=\{f(e(a.b), a)-f(e(a, b), e(a, b))\}$$E_{distr}^{2}(\mathcal{R})=$

whose termination can be verified using, e.g., the recursive )$\mathrm{a}\mathrm{t}\mathrm{h}$

$1$

6.

order with precedence$b\succ a$.

Dummy Elimination

In this section wethat the recent dummy elimination technique of Ferreira and Zantema[3] is also amenable to a self-labelling treatnlent. Let
be a TRS and let $e\in F$ be adesignated function symbol.
elimination transforms
into a TRS
over the signature $F_{O}=(\mathcal{F}-\{c\})\cup\{0\}$ . Here is a fresh. First we inductively define
a mapping cap that assigns to every term ina term in, as follows:$\mathrm{s}\mathrm{l}_{\mathrm{l}\mathrm{O}}1$$(\mathcal{F}, \mathcal{P}_{1})$$\mathrm{D}_{\mathrm{U}}\mathrm{n}\mathrm{l}\mathrm{n}\mathrm{l}\mathrm{y}$$(\mathcal{F}, \mathcal{P}_{\mathrm{L}})$$0$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{t}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{t}$$T(\mathcal{F}, \mathcal{V})$$c_{Z}o_{l)(t)}=\{$$\mathcal{T}(\mathcal{F}\circ’ \mathcal{V})$

$t$

if

$<>$

if $t=e(t_{1}, .. , , t_{n})$ ,$f(c\mathrm{t}\iota_{l}’(t_{1}), \ldots, cop(t_{r\mathrm{L}}))$

if $t=f(t_{1}, \ldots, t_{n})$ with $f\neq e$ .

$t\in \mathcal{V}$,$E_{dumm}(y\mathcal{R})$95

Next we associate with every term
if$\emptyset$$i=1\cup E_{du}mmy(ti)n$$t$

in $T(F, v)$ subsets$t\in \mathcal{V}$$\psi(t)$and $E_{dumm}(yt)$ of$\mathcal{T}(\mathcal{F}, v)$:,

if $t=e(t_{1}, \ldots,t_{n})$ ,$\psi(t)=\{$

if $t=f(t_{1}, \ldots,t_{n})$ with $f\neq e$ ,$\bigcup_{i=1}^{n}\mathrm{v}’(t_{i})$$E_{dummy(}t)=\psi(t)\cup\{_{C}ap(t)\}$

The mapping$E_{d\cdot\iota y}u\eta\prime l$$E_{dy}u7|lm(\mathcal{P}_{\mathrm{t}})=${.

is extended to$\mathcal{P}_{\mathrm{t}}$$larrow r’|l-r\in \mathcal{P}_{1}$by defining
and $r’\in E_{dummy}(r)$ }.

of Definition 5.1 and the mappings andNote the similaritv between the mappings and$E_{dummy}$ . Figure 3 shows the effect ofon the term of Figure 1. Observe that $E_{dummy}(t)$the characteristic that each numbered contexts occurs exactly once.
shares with$\phi$$\psi$$E_{ditr}^{\pi}s$$t$$E_{du7’\iota}7?\iota y$$E_{dis\prime}^{\pi}(rt)$$\triangle_{2}$$\triangle_{6}$$\triangle_{5}$$\triangle 4$$\triangle 3<\rangle$$\triangle 7\}$$\Gamma\dashv 1\mathrm{G}\mathrm{U}\mathrm{R}\mathrm{E}3$.

The main result of erreira and Zantema [3] states that dummy elimination is a correcttransformation technique for establishing termination.
$\mathrm{F}^{\mathrm{a}}$THEOREM 6.1. Let
left-ha 11
11 $ot$ occur interminating.

$(F, \mathcal{P}_{1})$$tl_{1}e$be a $TRS$
of$dSi\mathfrak{c}leS$$a$

11 $d$$1^{\cdot}\mathrm{e}w\iota\cdot ite$letrules of

be a
. If

$e\in \mathcal{F}$$\mathcal{R}$$n$ich doeson-c on lstall symbolisting tllell) is term$\mathrm{v}vl_{1}$$t$$E_{dy(}m7’ 1\mathcal{P}u\iota$$in\mathrm{a}$$\mathcal{R}$$\square$

It is easy to prove this result along the lines of the proof of Theorem 4.4, because the two:
key properties identifiecl earlier hold for $E_{dummy}$ as well, i.e., for all
, and
(1)
.
then there exists a term $t’\in E_{du7nm}(yt)$ such that cap(2) if)clefmition and the second property is easily proved by induction.
The first propertv holds
augmented with the operation) in thealgebraObserve that cap$t\in \mathcal{T}(\mathcal{F}, v)$$co_{l}J(t)\in E_{d,n}‘ 7l?\mathit{1}y(t)$$(S)\underline{\triangleleft}t’$$s\underline{\triangleleft}t$$1$$\mathrm{v}$$(t)=\langle t$$\mathcal{T}(\mathcal{F}\backslash \{e\}, v)$$\mathrm{t}\mathrm{e}\Gamma 111$$e_{A}(t_{1}, \ldots, t_{n})=$ ’.
for all
Theorem 6.1 by dropping the restriction that does not occur
It is possible torules in : simply replace every left-hand side of a rule inin the left-hand sides of. This enables us to conclude the termination of a non-simply terminatingby$\mathcal{P}_{\mathrm{t}}=\{f(e(a),b, .?\cdot)-f(c(x), e(x), e(x))\}$ by transforming it into the TRS
TRS like$t_{1},$$t_{n}\in T(\mathcal{F}\backslash \{\epsilon\}, \mathcal{V})$$\ldots,$$e$$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{e}\mathrm{l}\iota \mathrm{g}\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{n}$$\mathrm{r}\mathrm{e}\backslash \mathrm{L}^{r}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}$$E_{d?\iota?}t\iota?71y(\mathcal{P}_{1}1$$\mathcal{P}_{1}$$c\mathrm{r}\prime_{\mathit{1}^{J(l)}}$$E_{dun\iota r\}\iota}y(\mathcal{P}_{1})=\{f(\theta f(\mathit{0}|_{b_{\backslash }}b, \backslash \tau X))$

$xf(0,0, <\rangle)\}$

$l$

96

whose terlninatioll can be verified using any standard technique.
relative strength of (variants of) distribution elimination andA thorough investigation ofdummy elimination will be detailed elsewhere. Here we only remark that for left-linear TRSs
dummy elimination is to be preferred above distribution elimination.
$\mathrm{t}1_{1}\mathrm{e}$7.

Currying

In this final section we show that the main result of Kennaway, Klop, Sleep, and De Vries $[4]-$the preservation of termination under currying–is easily proved by self-labelling. Currying is
on TRSs defined below.
the$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{S}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{l}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$. lVith every TRS
we associate a TRS
as follows: the signature
contains all function symbols of together withfunction symbols of arity for everyof arity with $0\leq\dot{i}<n$ ,)@, called application,a binary functionis the extension of with all rewrite rules
and
DE

..

$\Gamma 1\mathrm{N}\mathrm{l}\mathrm{T}\mathrm{I}\mathrm{o}\mathrm{N}7.1$$(\mathcal{F}.

\Gamma\backslash ,)$$(\mathcal{F}_{@}, \mathcal{P}_{\mathrm{t}}@)$$\mathcal{F}$$\mathcal{F}_{\copyright}$$i$$f_{i}$$\mathrm{S}\}^{\prime \mathrm{n}}11$$\copyright(f_{i}(_{X_{1}}, \ldots, x_{i}),$$f_{i+1}$$n$$\mathcal{P}_{\mathrm{t}}$$\mathcal{R}_{\copyright}$

with$f\in \mathcal{F}$$01$$y\rangle$$f_{i+1}(X_{1}, \ldots, xi, y)$–of arity $n\geq 1$ and $0\leq i<n$ . Heredenotes if $?+1=n$ .
$f\in \mathcal{F}$$x_{1},$$\ldots,$$x_{i},$$y$are pairwise different$\mathrm{v}\mathrm{a}1^{\backslash }\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}$

and

$f$

Clearly termination of)$\mathcal{P}\iota_{@}\mathrm{i}_{111}1^{1}$$\mathrm{i}_{\mathrm{C}}\mathrm{s}$termination of

THEOREM 7.2 (Kennaway et al. [4]). If$\mathcal{P}_{\mathrm{t}}$$\mathcal{P}_{\mathrm{t}}$.

is a termina ting $TRS$ then$\mathcal{R}_{\copyright}$

is termina ting.

$\square$

The proof in [4] is rather involved. We present a self-labelling proof.

PROOF. Let. Using the well-known fact that termination is preserved underfollows e.g. from modularity considerations, see $[6]$ –we infer the tersignature). So the question is how termination of (mination of the TRS
I follows from$@_{A}(s,t)$ by induc. We turntermination of
into an-algebra by defining
tion on the structure of , as follows:$\mathcal{F}’=\mathcal{F}_{(@}\backslash \{(\underline{(}\backslash \mathrm{i})\}’$$\mathrm{e}\mathrm{x}\mathrm{t}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{i}\mathrm{o}11-\mathrm{t}\mathrm{h}\mathrm{i}_{\mathrm{S}}$$1\mathcal{F}’.\mathcal{P}\iota$$\mathcal{F}_{\copyright},$$\mathcal{T}(\mathcal{F}’, v)$$(\mathcal{F}’, \mathcal{P}_{\mathrm{t}})$$\mathcal{R}_{\copyright}$$A$$\mathcal{F}_{@}$$s$$@_{A}(s, t)=$

$t$

if

$f_{i+1}(s_{1}, \ldots, .-\vee i, t)$

if $s=f_{i}$ ($f(@_{A}(_{- 1}.\backslash , t),$if $s=f(s_{1,\ldots n}, \mathit{8})$ .

$\ldots,$$@A(_{-}.\backslash _{n}, t))$As well-founded order on
wetlle well-founded order コ defined asanel either . g\neq @ or $f,$$f=[egg0]$ and.

..

$\tau_{(}\mathcal{F}^{\prime,v_{)}}$$\mathrm{t}\mathrm{a}\mathrm{k}\mathrm{e}arrow \mathcal{P}\backslash +$$\mathrm{f}\mathrm{o}11_{0}\iota\dagger\cdot \mathrm{s}:f_{s}$$s(arrow \mathcal{P}\backslash \cup\triangleright)^{+}\dagger$$g\neq(\underline{\overline{\mathrm{Q}}}_{l}$$f$$s\in \mathcal{V}$,$s_{1,\ldots,}$s ) with $i<arity(f)$ ,. We equip the labelled signatureコ

if and only if, or$g_{t}$$/\mathrm{r}=(\mathrm{Q}\gamma.$$(\mathcal{F}_{@})_{lab}$

with

97

It is easy to see that コ is indeed a well-founded order. We have to show that $(A, arrow)+\pi$ is a
is precedence terminating
alld that the TRS
quasi-model forwith respect to .
. We claim that every algebra) is a quasi-model forFirst we show
operation is strictly monotone in all its coordinates. Here we consider only the first coordinate
which is the most interesting case. Before proceeding we mention the following fact,ofon the structure of :which is easily proved bv$(\mathcal{R}_{@})_{l}ab\cup dec(\mathcal{F}@, arrow)\mathcal{P}\backslash +$$(\mathcal{F}_{\mathrm{C}\mathrm{Q}}, \mathcal{P}_{\mathrm{t}}@)$$\text{コ}$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{a}\mathrm{t}\mathfrak{l}A,$$@_{A}$$arrow$$(\mathcal{F}_{@}, \mathcal{R}_{\copyright})$$+\mathcal{P}\backslash$.

$\mathrm{i}_{11}\mathrm{d}_{\mathrm{U}\mathrm{C}}\mathrm{t}\mathrm{i}_{0}11$

if $s\in T(F, \mathcal{V}),$$t\in \mathcal{T}(\tau^{J}, \mathcal{V})$

$s$

, and

$\sigma\in\underline{\nabla}(\mathcal{F}’, \mathcal{V})$then $@_{A}(s\sigma,t)=s@_{A}(\sigma,t)$ .

is defined as the mapping that assigns to every variable
Here the substitution$u\in T(F’, \mathcal{V})$ with. We show thatthe termin its first coordistructure of . Strict monotonicity of
bv induction on
)
all
this
argument. Since cannot be a variable, we
nate follows
or $s=f(s_{1}, \ldots, s_{n})$ . In the former casewithhave either$@_{A}(S,\dagger)=f_{i+1}(s_{1},\ldots,s_{i},t)$. Moreover, as is root-stable, must be of the form
we have.
. Hencewith.ystep from to takes place in one of the arguments
Suppose $s=f(S_{1}\ldots..s_{n})$ . If the. From the induction hypothesis we obtainof then$@_{A}(Sn’ t)$ )$t\vee 1),$
alld therefore@A(si, $t),$. If the rewrite step from to takes place.
$s=/\sigma$$n=r\sigma$
alld
for some rewrite rule $l=r\in \mathcal{R}$ and substituat the root of thcll, we obtain. Because 1 and do not contain function symbols fromtion$@_{A(S},t)=l@_{A}(\sigma, t)$ andfrom the above fact. Therefore also in this)is a quasi-model for. In order to conclude thatcase we haves.
for every rewrite ruleand, it remains to sh
tllat
fron]
. Otherwise
to
. If
then
assignment$i<arity(f)$, ), ), in whichandfor some
by definition.
case we have
we show thatis precedence terminating with
To conclude our ). The rewrite rules inrespect to コ. Clearlyaretaken care of ]) the first clause ofdefinition of , just as in the proof of Theorem 3.3. For
we usethe rules insecond clause.
$x$$(\underline{\mathrm{c}_{1^{1}}^{\backslash }}A(\sigma,t)$$((\overline{\mathrm{j}})\sim A(.\sigma, t)-n@_{A}(u, t)\mathrm{w}1_{1\mathrm{e}\mathrm{n}}\mathrm{e}\mathrm{v}\mathrm{e}\mathrm{r}s,t,$$\mathrm{C}\mathrm{t}\mathrm{l}\mathrm{I}A(X\sigma,t)$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$$\mathrm{f}\mathrm{r}\mathrm{o}\ln$$01$$1_{1}\mathrm{y}$$@_{A}$$s$$sarrow\Gamma\backslash u$$\mathrm{V}\mathrm{i}\mathrm{o}11.\backslash \mathrm{i}_{11(}111\mathrm{C}\mathrm{t}\mathrm{j}\mathrm{o}\mathrm{n}$$s=f_{i}(_{-1}.\backslash , \ldots, s_{i})$$s$$i<\mathit{0}\uparrow\cdot ity(f)$

$u$

$s$

$f_{i}(s_{1}, \ldots , u_{j}, \ldots,s_{i})$$\mathrm{c}\mathrm{c}1_{A}(_{\mathrm{c}}\mathrm{S}, t)arrow\Gamma \mathrm{c}f_{i+1}(s_{1}, \ldots,u_{j}, \ldots,s_{i},t)=@_{A}(u,t)$$-r_{\backslash }u_{j}$$\mathrm{r}\mathrm{e}\backslash \iota’ \mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}$

$s$

$u$

$v=f(.\sigma_{1}, \ldots , u_{j,\ldots,-\backslash _{n}}.)\backslash \mathrm{v}\mathrm{i}\mathrm{t}\mathrm{h}s_{j}-r_{\mathrm{c}}u_{j}$$s$( $(\mathrm{j},\}A\mathrm{t}S,t)=f(\mathrm{C}\cap\iota_{A(s},$$@_{A}(s_{i}, t)arrow r_{\backslash }@_{A(u_{j},t})$$f(^{\mathrm{Q}|}\mathrm{C}A(s_{1}, t),$$\ldots.(\underline{\mathrm{t}\dot{1})}(A1_{j}\iota, f)\ldots$.

$arrow n$$\ldots,$$\ldots,$$@_{A}(_{-}.\backslash _{\mathrm{t}},.\dagger))=@_{A}(u,t)$

$s$

$u$

$s$

$\sigma\in\Sigma(\mathcal{F}’, \mathcal{V})$$F’\backslash \mathcal{F}$$r$$(\mathrm{e}\mathrm{t}arrow|A(u.t)=r^{(\underline{C\mathrm{t}}1}A(\sigma,t)$$(\overline{\mathrm{o}})\sim A$$\langle$$t$$(\mathcal{F}_{@}, \mathcal{P}1@)$$l=0\mathfrak{a}_{(fi(X}1,$ $\ldots$$y$$x_{i}$$larrow r\in \mathcal{R}_{@}$$[\alpha](/)-_{\Gamma_{\mathrm{t}}}*[\mathit{0}’](r)$$o\mathrm{w}$$l-r\in \mathcal{P}_{1}$$\mathcal{T}(F’, \mathcal{V})$$\mathcal{V}$$\alpha$$(A, -_{\mathcal{P}_{\backslash }}+)$$-r_{\backslash }((\dot{\mathrm{J}}^{)}\sim A\mathrm{t}\iota/, f)$$[\alpha](l)=l\alphaarrow \mathcal{P}_{\mathrm{t}}r\alpha=[\alpha](r)$$t\backslash 11\mathrm{d}r=fj+1(X_{1}, \ldots, x_{i}, y)$$f\in \mathcal{F}$$[\mathfrak{a}](l)=f_{i+1}(x_{1}, \ldots , !_{i,y)\mathfrak{a}}=[\alpha]\{r)$$\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{f}$$(\mathcal{P}\mathrm{t}_{(\gamma,\sim}\mathrm{c})_{lab}\cup dec(\mathcal{F}_{@,r}arrow)+\mathrm{t}$$1$$\mathcal{R}la\iota\cup deC(\tau@, arrow \mathcal{R}+)$$(\mathcal{P}\iota_{@})_{Tb}‘’=\dot{\mathcal{P}}\iota_{l_{l\iota}}\iota\cup(\mathcal{P}_{1(}\overline{\langle}\mathrm{J}\backslash \mathcal{P}\iota)_{lb}a$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$$\text{コ}$$\iota^{r}$$\mathrm{t}1_{1}\mathrm{e}$$(\mathcal{P}\iota_{\mathrm{C}!}(\backslash \mathcal{P}\backslash ,);ab$$\square$

The reacler is invited to compare our proof with the one of$\mathrm{I}^{-}\acute{\mathrm{c}}\mathrm{e}\mathrm{n}\mathrm{n}\mathrm{a}\mathrm{w}\mathrm{a}\mathrm{y}$et al. [4].

References
1.

F. Bellegarde and P.
neering,N.
116, 1987.

$\mathrm{C}\mathrm{o}\mathrm{m}\mathrm{l}11\iota 111\mathrm{i}\mathrm{c}\mathrm{a}\uparrow \mathrm{i}_{0}\mathrm{l}1$2.

$\mathrm{D}\mathrm{e}\mathrm{r}\mathrm{s}\mathrm{h}\mathrm{o}\backslash \backslash ’ \mathrm{i}\mathrm{t}_{\mathrm{Z}},$

Termi 11 a tion by Completion, Applicable Algebra in Engiand Computing 1, pp. 79-96. 1990.
ot.
ting. Journal of Symbolic Computation 3(1), pp. 69-$\mathrm{L}\mathrm{e}\mathrm{s}\mathrm{c}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{l}\tau \mathrm{e}$$Te\iota\cdot 111jn\partial tio1$,$R\mathrm{e}\mathrm{w}\mathit{1}^{\cdot}\mathrm{i}$

98

3.

M.C.F. Ferreira and lI. Zantema, Dummy Elinl in a tion: Making Termina tion Easier, technical report UU-CS-1994-47, Utrecht University, 1994. To appear in the Proceedings ofthe 10th Conference onof Computation Theory, Dresden, Lecture Notes in
Computer Science, 1995.
J.R. Kennawav, J.W. Klop, R. Sleep, and F.-J. de Vries, On Comparing Curried and Uncu rried Rewrite System s, report CS-R9350, CWI, Amsterdam, 1993. To appear in the Journal)of Symbolic.
1]
J.W. Klop, Terl Rewriting S.vstems, in: Handbook of Logic in Computer Science, Vol. II(eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, pp. 1-116, 1992.
A.
A Suffi cientforTermination of $tl_{1}eDi$ rect Sum of Term
Rewriting S.vstems, Proceedings of the 4th IEEE Symposium on Logic in Computer Science,
Pacific Grove, PI). .39t)-401,.
H. Zantema, Term ination ofaRewritingLabelli , technical report RUUCS-92-3S,
University, 1992. To appear in Fundanienta Informaticae, 1995.
$\mathrm{F}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{a}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{a}1_{\mathrm{S}}$4.

$\mathrm{c}^{\mathrm{t}}\mathrm{o}\mathrm{m}_{1}$5.

6.

$\iota 1\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$Conditi_{\mathit{0}}l1$$\mathrm{M}\mathrm{i}\mathrm{d}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{d}\mathrm{o}\mathrm{r}_{1)},$$tl_{1}e$$19\aleph 9$

7.

$T\mathrm{e}1^{\cdot}\mathit{1}1$$b_{V}.s_{e}m$$\iota 1tj_{C}$$\iota 1g$$\mathrm{I}\mathrm{T}\mathrm{f}\mathrm{r}\mathrm{e}\mathrm{c}1_{11}$8.

H. Zantema,of Symbolic$\Gamma \mathit{1}^{\urcorner}\mathrm{e}l\cdot \mathrm{J}??\mathrm{i}_{1}1\mathrm{a}lion$

of.

Rewriting: In). 23-50, 1994.

$T\mathrm{e}1^{\cdot}m$$\mathrm{C}\mathrm{o}\mathrm{m}_{1^{)\mathrm{u}}}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}17.1^{)}1$$te\mathrm{r}_{l^{)}}\mathrm{f}et\mathrm{a}$tion and Type Elimination, Journal