数理解析研究所講究録
918 巻 1995 年 268-276

268

Eliminating Selectors from Term Rewriting Systems
Kikuchi, Yutaka*
Tokyo Institute of Technology
95/07/26

Abstract
Function symbols of term rewriting systems (TRSs) can be classified into three categories, namely,
constructors, selectors, and defined operators in terms of functional programming. The selectors arefor convenience of programming and efficient execution of programs, so the constructors and thedefined operators are sufficient to construct data structures and to manipulate them.
We give a transformation method to eliminate selectors from a TRS. We also introduce a newmodel of TRSs from the viewpoint of functional programming, and show that an original TRS andthe transformed TRS have the almost same model except trivial differences.
The transformation method preserves strong termination property. Although the methods do notpreserve weak terminating and confluency, we turn out sufficient conditions to keep those properties.

1

Introduction

We can divide function symbols into some categories when we consider TRSs as functional programs.
Huet et al make a completion algorithm more efficient by dividing functions into two categories suchthat constructor and.
We proceed to observe the role of functions in TRSs, non-constructor can be divide into further two
categories, one is a set of selectors that access elements in a data structure constructed by constructors,
the other is a set of defined operators that are the rest of functions.
$\mathrm{n}\mathrm{o}\mathrm{n}- \mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{o}\mathrm{r}[\mathrm{H}\mathrm{H}82]$

non defined-operators–
constructors

selectors

defined-operators

non constructor
Only constructors of a TRS derives any data structure on the TRS. Selectors corresponds to theconstructors, which make programming convenient and make its execution efficient. Therefore there
exists a TRS that has no selectors and has the same meaning intuitionally.
For example, assume a TRS whose constructors and rules are cons, nil and car $(ConS(X, y))\triangleright x$ ,$cdr(conS(x,y))\triangleright y$ , respectively.
Eitherorworks asa function that picks up the second element of a list.
It is interesting to transform a set of rules including selectors into that of rules that have no selectors.
There are major two interests; one is how we can do that for any case of rules, the other is how to judge
two TRSs have the same specification if the first interest is satisfied.
We will describe the concept of categorizing function symbols more precisely in the section 2. Next wewill show a method to eliminate selectors from TRSs. In the section4 we will introduce a new model to$\mathit{2}nd(x)\triangleright car(Cdr(x))$-mail:$*\mathrm{E}$$\mathrm{k}\mathrm{i}\mathrm{k}\mathrm{u}\mathrm{c}\mathrm{h}\mathrm{i}\Phi_{\mathrm{C}}\mathrm{s}.\mathrm{t}\mathrm{i}\mathrm{t}\mathrm{e}\mathrm{c}\mathrm{h}.\mathrm{a}\mathrm{c}.\mathrm{j}\mathrm{p}$$\mathit{2}nd(conS(x, conS(y, \mathcal{Z})))\triangleright y$269

denote specifications of TRSs as functional programs. In the section 5, we will show some characteristicof the method. It turns out that the method does not preserve weak termination and confluency, so wewill give some sufficient conditions of TRS to preserve the properties.
is inspired from
This paper is briefly translated from the technical paper [Kik95]. The[BK86] [GM87].
We use the same terminology of [DJ90] in this paper.
$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\mathrm{I}$2Constructors and Selectors

We regard a selector as a function that picks up an element from a data structure constructed byconstructors. A constructor defines a set of selectors corresponding to the arity of the constructor
therefore there is neither ambiguity nor voluntariness to define selectors. A set of rules is defined at thesame time that specifies the relationship between the constructor and the selectors. There is no otherrule that has a selector on the left hand side in the TRS.

Definition 2.1 Let
terms on .

$C$

is a set of constructors. A set of ground constructor terms $T(C)$ is a set of ground$C$

Notation 2.2$c_{n}$

is a constructor with arity $n(\geq 0)$ . Constants are constructors whose arity are .
$0$

Definition 2.3 Corresponding to a constructor

defined as follows.
$r_{n}^{i}$:$c_{n},$$n$-selectors$s_{n}^{i}$,$s_{n}^{n}$

and

$n$

-rules$r_{n}^{1},$$\ldots,$$r_{n}^{n}$areappears on the left hand side.

Notation 2.4 We distinguish constructors by using a label$diffe\dot{r}ent$
constructors that have the same arity.
$s_{n}$$\ldots$$S_{n}^{i}(Cn(X_{1,)}\ldots X_{i}, \ldots, xn))\triangleright X_{i}$This is the only rule in a $TRS$, which a selector

Notation 2.5$s_{n}^{1},$$l$to express$\mathrm{t}^{C}n’ l^{S_{n}^{i}},$ $\iota r_{n}i$when there aredenotes one of $s_{n}^{i}(1\leq i\leq n)$ .

Definition 2.6 Defined functions are functions that are neither constructors nor selectors.
such that it has
to express explicitly a
Notation 2.7 We use a notation
the constructors , the selectors and the defined operators $D$ .
means that we do not care the variable set in the $TRS$.
or
The notation$TRS\langle R, F, V\rangle$$\langle R, \langle C, S, D\rangle, V\rangle$$C$$\langle R, F, -\rangle$$S$$\langle R, \langle C, S, D\rangle, -\rangle$

We discuss a role of functions in a sense of functional programming and define a category of function
symbols in this section according as the such role.
Huet et al showed that we could distinguish between constructors and selectors when a TRS was. All constructor terms should be irreducible in theconsidered as a computation
Huets’ classification. They call those constructors free.
A condition that the constructors of a TRS are free makes the data structure derived from the TRS
a strict well founded structure. The condition lets programming so inconvenient; for example, andare different values when we prepare the constructors , succ, pred to express integer numsucc
bers in a TRS. and $-(0)$ are different values even if , succ,–are the constructors.
We loose the condition so that we can define any constructors when we classify function symbols.
$\mathrm{m}\mathrm{e}\mathrm{c}\mathrm{h}\mathrm{a}\mathrm{n}\mathrm{i}\mathrm{s}\mathrm{m}[\mathrm{H}\mathrm{H}82]$

$0$

$0$

$(pred(\mathrm{O}))$

$0$

$0$

270

Eliminating selectors by rule transformations

3

We give a method to eliminate selectors from a given TRS by transforming rules of the TRS. We will
discuss effects of the method in section5.
First phase is to use the following three transformation rules to remove each selector on the right handside of a rule. The number of transforming operations is at most the number of selectors on the righthand side of the all rules in a TRS because each application of the transformations removes one or more
selectors. Next phase is to remove all rules that contain selectors on the left hand side.
Trans I Let
We can express

be a $TRS$ that the rule contains selectors on the right hand side.
as follows without loss of generality where is an arbitrary term.

$\langle R\cup\{p\}, \langle C, S, D\rangle, V\rangle$

$p$

$p$

$\gamma$$p:\gamma\triangleright\delta[_{\vee}s_{n}^{m}(1\mathcal{T}),,.\cdots,S(nmk\mathcal{T}S_{\mathfrak{n}}|i(\tau)), \sim\tau, \ldots, \tau ]$appearances ofTarget selectors are$s_{n}^{m:}\in S$$k(1\leq\dot{i}\leq k, 1\leq m_{i}\leq n)$.
Remove the rulethat have$\tau$

as those arguments. We assume the number of the targets isdoes notis all appearances of with which$\tau$. The rest of the context$\delta$$\tau$$s_{n}$$assoc\dot{i}ate$$q_{1}$:$p$and append two rules$q_{1},$ $q_{2}$to remove the targets.

$\gamma\triangleright h(\tau,y1, \ldots,y\vee\downarrow)$

1–variables$q_{2}$: $h(_{C}n(X1,$$...’ X\sim^{),y1,\ldots,y\iota)}x.\cdot n\triangleright\delta[_{\frac{x_{m_{1}},..x_{m_{k}}}{x_{\mathfrak{n}}}\frac{c_{n}(_{X_{1}},\ldots,Xn),\ldots C_{n}(x_{1,..\cdot\cdot n}X)}{appea\gamma anceSof_{C_{n}}’(_{X_{1\cdot n}},.,X)}}.\cdot\dot{.},,,]$$x_{m}$

:

and

in

$c_{n}(x_{1}, \ldots, x_{n})$transformed $TRS$ is$F’=\langle C, s, D’\rangle,$$q_{1},$

replaceassociation in respectively. The
and without
where $P=R\cup\{p\},$ $Q=R\cup\{q_{1}, q_{2}\},$ $F=\langle C, S, D\rangle,$ $D’=D\cup\{g\}$ ,$s_{n}^{m_{i}}(\tau)$$q_{2}$$\langle Q, F’, VJ\rangle$$V’=V\cup\{x_{1}, \ldots, x_{n}\}$$\tau$$p$$s_{n}$.

is a new defined operator called an auxiliary function symbol.
are the all appearances of variable in .
$h$$x_{1},$$\ldots$,$x_{n}$

does not exist in $P,$ $y1,$$\ldots,$$y\iota$$\delta$Trans II Let

be a $TRS$ that the rule$\langle R\cup\{p\}, \langle C, S, D\rangle, V\rangle$$p:\gamma$[$\ldots,$]$x$$\triangleright\delta$

is the following form.

$p$

,

[

$appe\sim x,$

appearances of$\ldots,$]$x$$appe\sim x,$$.,\cdot,$

appearances of

$x$

$x$

that have the same variable denoted by . We assume the number of the targets
Target selectors areis $k(1\leq i\leq k, 1\leq m_{i}\leq n)$ .
does not associate.
The rest of the context is all appearances of with which
Remove the rule and append a rule to remove the targets.
$s_{n}^{m^{:}}$

$x$

$x$

$\delta$$s_{n}$$q$$p$$q:\gamma[C_{n}(X1, \ldots,Xn), \ldots, C_{n}(_{XX)}1, \ldots,n]\triangleright\delta[xm1’\ldots, xmk’ C_{n}(x_{1}, \ldots, xn), \ldots, C_{n}(X_{1}, \ldots, x_{n})]$$x_{m}.\cdot$

andformed$c_{n}(x_{1}, \ldots , x_{n})$

$TRS$

is

Trans III Let

and without
association inin replace
where $P=R\cup\{p\},$ $Q=R\cup\{q\},$ $F=\langle C, S, D\rangle$ .
$s_{n}^{m_{i}}(x)$

$q$

$x$

$s_{n}$$p$respectively. The trans-$\langle Q, F, V\rangle$$\langle R\cup\{p\}, \langle C, S, D\rangle, V\rangle$

be a $TRS$ that the rule$p$is the following form.

$p:\gamma\triangleright\delta[s^{i}(n(c_{n}\mathcal{T}_{1}, \ldots, \tau_{i}, \ldots, \tau n))]$A target selector is
Remove the rule$s_{n}^{i}$$p$.

$\gamma,$$\tau_{1},$$\ldots,$$\tau_{n}$are arbitrary terms.
to remove the target.

and append a rule$q$$q:\gamma\triangleright\delta[\tau_{i}]$The transformed $TRS$ is$\langle Q, F, V\rangle$

where $P=R\cup\{p\},$ $Q=R\cup\{q\},$$F=\langle C, S, D\rangle$

.

271

Trans IV Let

transformed$\langle$$R\cup\{p\},$ $\langle C, S, D\rangle,$

$TRS$

is

$\langle R, F, -\rangle$-) be a $TRS$ that the rule

where

$p$

is the following form. Remove . The$p$$F=\langle C, S, D\rangle$$p:\gamma[s_{n}(\tau)]\triangleright\delta$

3.1

Examples of transformation to eliminating selectors

We show some examples of selector elimination. Although we defined the notation of function symbols
in the section2, conventional function names are used here to give much intuitionistic understanding.
Example 3.1 List manipulation
2nd picks up a second element of a list, duplast returns a list whose car and cdr are a last element of agiven list and the whole given list respectively. rev returns a reverse order list of a given list, and thedefinition of rev is omitted to describe the TRS simply.
The functions should be defined as $nil=c_{0}$ , $cons=c_{2}$ , $car=s_{2}^{1},$ $cdr=s_{2}^{2}$ in accordance with thenotation in the section2.

$[P=C=\{n\dot{i}l, ConS\},sD=\mathit{2}nev,d=upla\{CarSt’\}Cdr\},$$]$

The following is example reductions on the TRS.
$\mathit{2}nd$( $conS$ ($n\dot{i}l,$$cons$ ( $conS$ ($n\dot{i}l$, nil), $nil))$ ) $arrow!cons$ (duplast(cons(nil, $cons$ ( $cons$ (nil, nil),$n\dot{i}l))$$n\dot{i}l$, nil)) $arrow!conS(conS$ ($n\dot{i}l$, nil), $conS(nil,$ $cons$ ( $cons(nil$ , nil), nil)$\mathit{2}nd(n\dot{i}l)arrow!car(cdr(nil))$duplast $(n\dot{i}l)arrow!conS$ ($Car(n\dot{i}l)$, nil)

Note that there are normal ground terms that have selectors.
We get the following TRS from the previous TRS by the transformation method.

$[C=\{Q=n\dot{i}l, conS, S=\emptyset, D=\mathit{2}nd, rev, duplaSt, h\}]$Any normal ground term on the transformed TRS has no selectors, while the original TRS not.
$\mathit{2}nd(nil)arrow \mathit{2}nd(n\dot{i}l!)$h$ (, nil)
duplast $(nil)arrow$nil!$

Example 3.2 Natural number:-is a subtract function on natural numbers. The functions should be defined as $0=c_{0}$ , $succ=c_{1}$ ,$pred=s_{1}^{1}$ in accordance with the section 2.
$suCc,$ $s=\{pred\},$$[P=C=0,$$D=\{-\}]$

272

The following are examples on the $TRS$ . There is a normal constructor term including a selector in thelatter case.
$-(succ(SucC(\mathrm{O})), sucC(0))arrow!sucC(\mathrm{O})$$-(succ(\mathrm{o}), succ(SucC(0)))arrow pr!(ed\mathrm{O})$We get the following $TRS$ by application of the transformation method.

$D=\{-\}]$$[Q=c=\{0,$$Succ=\emptyset,$

Now we have the following reduction sequence: $-(suCC(\mathrm{O}), suCc(suCc(0)))arrow|-(0, sucC(\mathrm{o}))$4Constructive Model

We propose new concepts about TRSs constructive domain and constructive model.
An initial model of a TRS is differ from our intuitionistic model when functions are categorized into
three groups. For example in the introduction, we do not indicate that two rule sets describe the same
specification because their initial models are different. Moreover the initial model has irreducible terms. Because those terms correspond to execution exceptions e.g. unexpectedusing selectors such as car
segmentation violation, it is not suitable to use an initial model of a TRS when we use TRSs as functional
programs.
The meaning that computation results are proper corresponds to normal forms are constructed byonly constructors. The model of TRSs should exclude any term whose normal term has selectors andany term whose arbitrary subterm derives normal term with selectors.
Therefore we introduce a new concept about domain and model on TRSs. A constructive domain is
a set of ground terms whose every subterm has a reduction sequence toward a ground constructor termon the domain. A constructive model is a set of congruent closures on the constructive domain of the
TRS.
$(n\dot{i}l)$Definition 4.1 Let
is defined as follows.

$\langle R, \langle C, S, D\rangle, -\rangle$

is a $TRS$ where $F=C\cup S\cup D$ , a constructive domain of the $TRS$$T_{C}^{R}(F)$$\mathcal{T}\in T(C)$$\tau\in T_{C}R(F)^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}\{$$\tauarrow\sigma R$

Deflnition 4.2 A constructive model

Notation 4.3 We
instead$just\approx when$is obvious.
$use\approx R$$of\sim R$

where$\tau_{C}^{R}(F)/\sim R$

is quotient of$T_{C}^{R}(F)by\sim R^{\cdot}$

to distinguish the case on$T_{C}^{R}(F)$from the case on $T(F)$ , and use$R$

Definition 4.4 We say $M\subseteq M’$ where $M,$ $M’$ are constructive models if the following holds.
$M\models\tau=\sigma\Rightarrow M’\models\tau=\sigma$

Lemma 4.5 For every term in a constructive domain, there exists a reduction sequence from it towarda ground constructor term.

General speaking $T(C)\subseteq T_{C}^{R}(F)\subseteq T(F)$ holds. Note that a constructive domain of a TRS is a subsetof the restricted domain whose terms just have equivalent ground constructor terms. For example, thelatter domain has a term car $(conS(nil, Car(nil)))$ but the constructive domain does not.

273

Effects by transformation

5

We investigate properties of the transformation method in this section. First we prove that the method
preserve models. Second we prove the method holds strong terminating property of TRSs. Finally weshow that the method will break weak termination and confluency.

5.1

ModelsDefinition 5.1 Where there exist
the following holds.

$R$

and

$p$

such that $P=R\cup\{p\}$ and$Q\supseteq R$, we say$\langle Q, F, -\rangle$

simulates$\langle P, F, -\rangle\dot{i}f$$\forall\{\tau_{1}, \ldots, \tau_{n}, \sigma\}\subseteq\tau_{c}P(F),\forall\tau(\equiv f(\mathcal{T}_{1\cdot\cdot n},.,\mathcal{T}), f\in F)(\{\tau_{1}, \ldots, \tau_{n}, \sigma\}\subseteq\tau_{c^{(F)}}^{Qp}\wedge \mathcal{T}arrow\sigma)P\Rightarrow\tau\approx\sigma Q$

Lemma 5.2 if

is simulated by$\langle P, F, -\rangle$$\langle Q, F, -\rangle$then$\tau_{C}^{P}(F)/\approx P\subseteq\tau_{c}^{Q}(F)/_{Q}\approx$

and the congruency on

is also in
Proof We show that a term in.
by induction on the structure of the term in
obviously.
holdsbase case:induction step: We assume the property for$T_{C}^{Q}(F)$$T_{C}^{P}(F)$.
$T_{C}^{P}(F)$holds on

$T_{C}^{Q}(F)$$T_{C}^{P}(F)$$\tau\in T_{C}^{P}(F)\Rightarrow\tau\in T_{C}^{Q}(F)$$\{\tau_{1,)}\ldots\tau_{n}, \sigma\}\subseteq T_{C}^{P}(F)$

1. Case

2. Case$rPr\neq p$ :$\taurightarrow\sigma,$

As

$r$

is common for $P$ and $Q,$$\tauarrow\sigma:Pp\{\tau_{1}, \ldots, \tau_{n}, \sigma\}\subseteq T_{C}^{Q}(F)$$\tau\approx Q\sigma$

because$\langle Q, F, -\rangle$

simulates$\tauarrow\sigma Qr$. Let

that isbe$\tau$$\tau\approx Q\sigma$$f(\tau_{1}, \ldots, \tau_{n})$.

.

holds from the hypothesis of the induction. Here we have$\langle P, F-\rangle$.

Therefore the property holds for the all terms of$T_{C}^{Q}(F)$1.

Theorem 5.3 The constructive models of a $TRS$ and a transfomed one by the method are the same.

soandsimulate each other on theand { $Q,$ $F’,$
Proof (Brief)
simulate each other on the transformationIIandare isomorphic by lemma5.2.
are isomorphic by lemma5.2.
soand1
and on the$\langle P, F’, -\rangle$$T_{C}^{Q}(p’)$$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}\mathrm{I}\mathrm{I}\mathrm{I}$5.2$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{I}$$-\rangle$$\langle P, F, -\rangle$$T_{C}^{P}(F)$$T_{C}^{P’}(F’)$$\langle Q, F, -\rangle$$T_{C}^{Q}(F)$Strong termination

Theorem 5.4 A transformed $TRS$ is strongly terminating if the original $TRS$ is so.
Proof (Outline) If we assume a transformed TRS is not strongly terminating then we can make ainfinite reduction sequence in the original TRS. This is a contraposition of the theorem.
1

5.3

Weak termination

Theorem 5.5 A transformed $TRS$ may not be weakly terminating even if the original $TRS$ is so.

274

Proof (Brief) The following is a contradiction.
where $C=\{c_{1,0}c\},$ $s=\{s_{1}^{1}\},$ $D=\{a, b, d\}$ .

$\langle Q, \langle C, S, D\rangle, -\rangle$

is transformed from$\langle P, \langle C, S, D\rangle, -\rangle$$P:$ $Q:$$\langle$$P,$ $\langle C, S, D), -\rangle$

5.4

is weakly terminating but$\langle Q, \langle C, S, D\rangle, -\rangle$

1

is not.

Confluency

Theorem 5.6 A transformed $TRS$ may not be confluent even
Proof (Brief) The following is a contradiction.
where $C=\{c_{0}, c_{1}\},$ $S=\{s_{1}^{1}\},$ $D=\{a, b\}$ .

$P:\{a(X,C_{1}a(X,c0_{b})(y))b$$\langle P, (C, S, D\rangle,$ $-\rangle$$\triangleright\triangleright\triangleright\triangleright$$\dot{i}f$$\langle Q, \langle C, S, D\rangle, -\rangle$$a(_{C_{0}},C1(Ca(_{S(_{C}),C_{0})}a(s_{1}x111(x0),y)0))\}$$Q_{1}$:

the original $TRS$ is so.
is transformed from$\{a(X,C1(yh(C_{1}a(_{X}, \mathrm{o}_{b})(X))))b$$\triangleright\triangleright\triangleright\triangleright\triangleright$$xa(X,\mathrm{o})a(s_{1(x}^{1}a(C0,c1(h(_{C_{0}})),yC_{0})))\}$

is confluent because it is left linear, right linear and strongly closed, but

is not confluent.

6$\langle P, \langle C, S, D\rangle, -\rangle$$\langle Q_{1}, \langle C, S, D\rangle, -\rangle[$

Sufficient conditions for stable TRSs

We showed examples that the transformation method loosed weak termination and confluency in thesection5. In this section, we provide some sufficient conditions for TRSs whose weak termination andconfluency are not broken by the method.

6.1

Constructive TRSs

We have discussed about arbitrary TRSs. A constructive domain and a constructive model of any TRS
can be defined if we can separate functions into three groups. This means that we introduced only themodels that have a functional programming sense.
Now we deal with restricted TRSs, named constructive TRSs, that enjoy a manner of functional
programming.
Definition 6.1 we say a$T_{C}^{R}(F)$$TRS\langle R, \langle C, S, D\rangle, -\rangle$

is constructive$\dot{i}f$

for any$\tauarrow\sigma R$

both$\tau\in T_{C}^{R}(F)\Rightarrow\sigma\in$

and $\tau\in T(C)\Rightarrow\sigma\in T(C)$ hold.

Definition 6.2 A constructive kernel ofwhere $\sigma\in T(C)$ .

$\langle R, \langle C, S, D\rangle, -\rangle$

is a sub-TRS whose rewriting set are$\tauarrow\sigma$$\tau,$

Lemma 6.3 A constructive $TRS$ is weakly terminating if and only if the constructive kernel of the $TRS$
is weakly terminating

275

1

Proof (Exercise)

Theorem 6.4 The transformation method preserves weakly $terminat_{\dot{i}ng}$ in a $construct\dot{i}ve$ domain of a.

$construct\dot{i}veTRS$

Proof (Brief) The transformation method does not affect a constructive kernel of the constructive
so preserves weakly terminating.

$\mathrm{T}\mathrm{R}\mathrm{s}_{\mathrm{i}}$Regular TRSs

6.2

Regular TRSs are confluent[Hue80], but the transformation method can break regularity of a TRS.
We provide a syntactical condition called strong regularity, which is a little bit more constrained thanregularity. The transformation method preserves strong regularity of TRSs.

Definition 6.5 A
where$TRS\dot{i}S$$c_{n}(\tau_{1\cdot\cdot n},., \tau)\triangleright\sigma$

thea constructor andstrongly regular$c_{n}\dot{i}S$

Theorem 6.6 A transformed$\dot{i}f$$TRS_{\dot{i}}s$$\tau_{1},$$TRS\dot{i}S$$\ldots,$

strongly regular$\dot{i}t$$\tau_{n},$$\dot{i}f$regular and does not have a rule such thatare arbitrary terms.
$\sigma$the$or\dot{i}g\dot{i}nalTRS\dot{i}S$strongly regular.

Proof We show in the case of transformation I. In the case of transformation II is similar, and they
are obvious in the other cases.
is an transformed one
is an original TRS andLet
are the following.
where$\langle P=R\cup\{p\}, F, -\rangle$$\langle Q=R\cup\{q_{1}, q_{2}\}, F\cup\{h\}, -\rangle$$p,$ $q_{1},$ $q_{2}$$p:\gamma\triangleright\delta[s_{n}^{m}(_{\mathcal{T}),\ldots,(\tau),]}1Snm_{k}\tau,$$\ldots$$q_{1}$$q_{2}$:$\ldots,n’\ldots]$: $h(_{C_{n}}(X_{1,\ldots,n}X),$ $y_{1,\ldots,y)[C_{n}(x)}\iota\triangleright\delta X_{m’\cdots,m_{k}}1X,x_{1},$$\gamma\triangleright h(\tau,y_{1}, \ldots, y\iota)$

is linear because the lhs of is linear and the lhs of is linear by its syntax.
linearity: The lhs ofoverlapping: The all lhs of $R$ does not overlap that is the lhs of because the original TRS isstrongly regular. So they do not overlap the lhs of . The lhs of does not overlap because thefunction symbol does not appear in any rule of $P$ and any lhs of $P\cup\{q_{1}\}$ is not a term whose mainfunction is .
1
Therefore is strongly regular.
$p$$q_{1}$$q_{2}$$p$$\gamma$$q_{1}$$q_{2}$$h$$c_{n}$$Q$

Conclusion

7

We had observed a role of functions in the TRS and introduced a classification of them. The transformation method provided in this paper eliminates selectors of a TRS. The method does not effect toconstructive model while transformation, and preserves strong termination. Unfortunately the method
can break weak termination and confluency. We provided two sufficient conditions of TRSs; the firstpreserves weak termination in the constructive domains and the other preserves confluency. The tablelshows the properties of change in the transforming TRSs.
We must solve the following in the next step.

.

$0$

Define conservative extended models of constructive models. The discussion about preserving
models will be clear on conservative extended models when using the transformation I.
Theorem 6.4 will be a meaningful if the transformation preserves constructive property for an
arbitrary constructive TRS.

276

.

$\bullet$

The transformation method preserves confluency in a constructive domain of a constructive TRS.
Relax the definition of selectors. A function
it may be interpreted as a selector.

$\mathit{2}nl\ln$the example 3.1 is a defined operator here but

no constraint

TRS
property

Model

ST

TransI$[egg0] \mathrm{O}$TransII$[egg0] \mathrm{O}$TransIII
TransIV
The whole method: strong termination

WT$\triangle \mathrm{O}$CR$\cross \cross$$\mathrm{O}$$\cross \cross$$\mathrm{O} ---$$\mathrm{O}$$-$$\triangle \mathrm{O}$$\triangle \mathrm{O}$$\mathrm{W}\mathrm{T}$$\mathrm{S}\mathrm{T}$$[egg0]$$\triangle$$\mathrm{O}$$\cross$

constructive
WTCR

strongly regular
WTCR$\mathrm{O}$$— 0$$\mathrm{O}$$\mathrm{O}$$\mathrm{O}$$\mathrm{O}$$–$$\cross$$\cross$$–$$\mathrm{O}$: weak termination$\mathrm{O}$$\mathrm{C}\mathrm{R}$: confluency

the same model
the same extended model (not the same model)preserves
does not preserve
unknown
Table 1: Properties of transformed TRSs

References[BK86] J. A. Bergstra and J. W. Klop. Conditional rewrite rules: Confluence and termination. Journalof Computer and System Sciences, 32:323-362, 1986.
[DJ90]

Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor,
Handbook of Theoretical Computer Science, volume B, pages 243-320. Noth-Holland, Amsterdam, 1990.

[GM87] E. Giovannetti and C. Moiso. Notes on the elimination of conditions. In S.Kaplan and J.P.Jouannaud, editors, Lecture Notes in Computer Science, 308, pages 91-97. Springer-Verlag,

71987.

[HH82] G. Huet and J. M. Hullot. Proofs by induction in equational theories with constructors. Journalof Computer System Science, $25(2):239-266$ , 1982.
[Hue80] G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems.
Journal of the ACM, $27(4):797-821$ , 1980.
[Kik95] Yutaka Kikuchi. Eliminating selectors from term rewriting systems. Technical Report 95TR0014, Tokyo Institute of Technology, Ookayama, Meguro, Tokyo 152 Japan, 71995. ISSN 09182802, in Japanese.