%MASSIMO MARCHIORI

\documentstyle[11pt,lcscover,QED]{article}

\coverauthor{Massimo Marchiori}
\covertitle{On Deterministic Conditional Rewriting}
\coverdate{December 9, 1997}
\trnumber{Computation Structures Group Memo 405}

%%% \def\qedsymbol{\blacklozenge}

% %widelayout file 
% \input{widelayout}
% \setlength{\textheight}{228mm} %(widelayout is 235mm)

\input{amssym.def}
\input{amssym}

\include{BASIC}

%%
%% Install the euler script font (use \euler{} IN MATH MODE)
%%
\font\teneusm=eusm10
\font\seveneusm=eusm7
\font\fiveeusm=eusm5
\newfam\eusmfam
\textfont\eusmfam=\teneusm
\scriptfont\eusmfam=\seveneusm
\scriptscriptfont\eusmfam=\fiveeusm
\def\euler#1{{\fam\eusmfam\relax#1}}

\newcommand{\PROOFEND}{%%%%%%%%%%%%%%%%%% it's the old HB... :-)
{\unskip\nobreak\hfil\penalty50
\hskip2em\vadjust{}\nobreak\hfil$\Box$
\parfillskip=0pt \finalhyphendemerits=0 \par}}



%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Local Commands

%Bold Math Italic Family Font
\font\tencmmib=cmmib10    \skewchar\tencmmib='60
\font\sevencmmib=cmmib10  \skewchar\sevencmmib='60
\font\fivecmmib=cmmib10   \skewchar\fivecmmib='60
\newfam\cmmibfam
\textfont\cmmibfam=\tencmmib
\scriptfont\cmmibfam=\sevencmmib
\scriptscriptfont\cmmibfam=\fivecmmib
\newcommand{\bmit}[1]{{\fam\cmmibfam\relax#1}}

\def\AMShexnumber#1{\ifcase#1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or 8\or
 9\or A\or B\or C\or D\or E\or F\fi}
\newcommand{\ASEM}[2]{\MATH{\mathchar"0\AMShexnumber\cmmibfam0B}_{#1}(#2)}

\newenvironment{program}{\smallskip\em}{\rm\smallskip\noindent} 
   %%% ^^^ BAD command, with side effects and assumptions
   %%% about indentation (left to the user)
   %%% (could be used with \newcommand{\myprog}[2]{{#1}{\la}{#2}} )


%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%
%%%%%%%%%% 
%%%%%%% Grabbed from the vaccines paper
\newcommand{\op}{\MATH{\mathop{\odot}}}
\newcommand{\VACC}[1]{\MATH{{\bf V}_{\!\!#1}}}
\newcommand{\FULLVACC}[3]{\MATH{{\bf V}_{\!\!#1}^{#2}(#3)}}
\newcommand{\PEQ}{\MATH{\:\sim_{\calP}\:}}
\newcommand{\mto}{\rightarrow^*}
\newcommand{\kmto}{\rightarrow\!\!\!\!\!\rightarrow}
\newcommand{\kkto}[1]{{\displaystyle\mathop{\rightarrow}_{#1}}\!\!\!\!\!\!\mathop{\rig
htarrow}_{\phantom{#1}}\!\!\!}%%% BEWARE: kkmto does not uses rightarrowfill...
\newcommand{\kmot}{\mbox{$\leftarrow\!\!\!\!\!\leftarrow$}}
\newcommand{\pto}{\rightarrow^+}
\newcommand{\mmto}[1]{{\displaystyle\mathop{\mbox{\rightarrowfill}}_{#1}}^*}
\newcommand{\ppto}[1]{{\displaystyle\mathop{\mbox{\rightarrowfill}}_{#1}}^+}
\newcommand{\tto}[1]{{\displaystyle\mathop{\mbox{\rightarrowfill}}_{#1}}}
\newcommand{\DOUBLE}[2]{{#1 \atop {#2}}}
\newcommand{\ToyONE}{\MATH{\{F(0,1,X)\to F(X,X,X)\}}}
\newcommand{\ToyTWO}{\MATH{\{or(X,Y)\to X, or(X,Y)\to Y\}}}
\newcommand{\prettyToyTWO}{\MATH{%
\left\{\begin{array}{l}
or(X,Y)\to X\\
or(X,Y)\to Y
\end{array}
\right\}
}}

%%%%%%%%% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ New commands

\newcommand{\ultra}[1]{\mbox{\it ultra-{#1}}}
\newcommand{\join}{\MATH{\downarrow}}
\newcommand{\Nto}{\MATH{\to^*_!}}
\newcommand{\VAR}{{\rm VAR}}
\newcommand{\Var}{{\em Var}}
\newcommand{\GUNR}{{\bf U}}
%% \newcommand{\UNR}{\MATH{\Bbb U}}
%% \newcommand{\BUNR}{\MATH{{\Bbb U}^{\flat}}}
\newcommand{\NUNR}{\MATH{{\Bbb U}_n}}
\newcommand{\DUNR}{\MATH{{\Bbb U}_D}}
%% \newcommand{\INFINITYNUNR}{\MATH{\widetilde{\Bbb U}_n}}
%% \newcommand{\BNUNR}{\MATH{{\Bbb U}_n^{\flat}}}

\newcommand{\UUU}{\calU}

\newcommand{\CE}{\MATH{\calC_{\calE}}}


\newcommand{\CON}{{\rm CON}\MATH{^{\to}}}
\newcommand{\EQCON}{{\rm CON}}
%% \newcommand{\UN}{{\rm UN}\MATH{^{\to}}}
%% \newcommand{\EQUN}{{\rm UN}}
%% \newcommand{\NF}{{\rm NF}}

\newcommand{\SN}{{\rm SN}} %BEWARE: defined in the text..?

\newcommand{\joinrule}{\MATH{t_0\to s_{k+1}\Leftarrow s_1\join t_1,\LL,s_k\join t_k}}
%% \newcommand{\semieqrule}{\MATH{\displaystyle l\to r\Leftarrow s_1\mathop{\leftrightarrow}^* t_1,\LL,s_k\mathop{\leftrightarrow}^* t_k}}
%% \newcommand{\FULLjoinrule}{\MATH{\rho:\:\joinrule}}
%%% \newcommand{\normalrule}{\MATH{l\to r\Leftarrow s_1\Nto n_1,\LL,s_k\Nto n_k}}
\newcommand{\FULLnormalrule}{\MATH{\rho:\:\normalrule}}
\newcommand{\detrule}{\MATH{t_0\to s_{k+1}\Leftarrow \allowbreak s_1\to^* t_1, \allowbreak \LL, \allowbreak s_k\to^* t_k}}
\newcommand{\FULLdetrule}{\MATH{\rho:\:\detrule}}


\newcommand{\TERMS}{\mbox{\sc Terms}}
\newcommand{\ETERMS}{\mbox{\sc Terms$^+$}}

\newcommand{\csplus}{\MATH{\:{\displaystyle\mathop{\oplus}_{cs}}\:}}
\newcommand{\compplus}{\MATH{\:{\displaystyle\mathop{\oplus}_{comp}}\:}}
\newcommand{\hierplus}{\MATH{\:{\displaystyle\mathop{\oplus}_{hier}}\:}}

\newcommand{\PROOFOF}[1]{%
\par\NI
\dotfill
\par\NI
{\bf [Proof of {#1}]}\\}
%%%%%\newcommand{\OLDRESULT}{{\bf ($\star$)}\ \ }
\newcommand{\OLDRESULT}{}

\newcommand{\REVOLUTION}{\MATH{\euler{R}}}
\newcommand{\URANK}{\mbox{{\it \UUU-rank}}}
\newcommand{\UDEPTH}{\mbox{{\it \UUU-depth}}}

\newcommand{\TOP}[1]{\MATH{\blacktriangle_{#1}}}
\newcommand{\BOT}[1]{\MATH{\blacktriangledown_{\!#1}}}

%% \newcommand{\STRICTWN}{{\rm SWN}}

\newcommand{\nop}[1]{}

%% \newcommand{\SUBSUMES}{\MATH{\lhd}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TITLE...  
\title{\bf On Deterministic Conditional Rewriting}
\author{Massimo Marchiori\\
MIT Laboratory for Computer Science\\
545 Technology Square, Rm.\ NE43-257\\
Cambridge, MA 02139\\
{\tt max@lcs.mit.edu}}
\date{}

\begin{document}
\maketitle
%% \thispagestyle{empty}
%% \pagestyle{empty}

\begin{abstract}
The class of Deterministic Conditional Term Rewriting Systems (\mbox{DCTRSs}) is 
of utmost importance for the tight relationships exhibited with functional 
programming, logic programming and inductive reasoning. However, its 
analysis is extremely difficult, and to date there are only very few 
works on the subject, each analyzing a particular aspect of DCTRSs. 
In this paper, we perform a thorough analysis of DCTRSs, ranging from 
the study of termination criteria, to new verification methods for the 
major properties of DCTRSs like termination and confluence, to the 
identification of subclasses of DTCRSs 
that exhibit a particularly nice behaviour. Moreover, 
we also address the study of {\em modularity\/} of DCTRSs, providing a 
number of new powerful results. This is particularly important, since 
to the best of our knowledge there is so far {\em not a single result\/} 
on the modularity of DCTRSs, and of 3-CTRSs in general. Finally, 
most of the analysis of the paper is performed relying on the recent tool 
of unravelings, that 
allows to automatically lift results from the much simpler unconditional 
rewriting systems to DCTRSs. This way, we clarify what are the links 
between TRSs and DCTRSs, providing better intuitions on how the gained 
experience on TRSs can be profitably reused to understand the 
much more complicated world of DCTRSs.
\smallskip

\NI
{\em Keywords:\/} oriented and deterministic CTRSs, modularity, verification, unraveling.
\end{abstract}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
Conditional rewriting, besides being a primary field of interest for the 
rewriting community, is nowadays assuming an increasingly greater importance 
in view of the tight connections with the functional and logic programming 
paradigms. To this extent, the basic forms of conditional rewriting 
(so called ``1-CTRSs''), where the conditions to be evaluated are 
merely tests, and 
do not allow parameter passing and creation of new computed values, 
are no longer sufficient, since to reach the 
power of the functional and logic programming paradigms one has to go 
beyond. One of the most powerful classes of CTRSs so far object of research is 
that of so-called ``3-CTRSs'', where this creation of new computed values 
by the conditions is allowed. In particular, the class of deterministic 
CTRSs (cf.\ \cite{BG89,Gan91b,Han94}) has shown to be of utmost importance, 
since it is sufficiently flexible to capture 
the power of local definitions proper of functional languages. 
However, flexibility has a cost: the analysis of deterministic 
CTRSs (briefly, DCTRSs) 
is extremely difficult when compared to simpler forms of rewriting 
like unconditional TRSs or even conditional rewriting systems like 1-CTRSs 
or 2-CTRSs. As a result, there are to date only very few works that 
deal with the analysis 3-CTRSs 
(cf.\ \cite{BG89,Gan91b,GW92,AL94b,SMI95}). 
In this paper, 
we perform a thorough analysis of DCTRSs (and, en passant, 
of oriented CTRSs), studying their major properties like termination 
and confluence. First, we perform an abstract study of termination for 
oriented and deterministic CTRSs, presenting new criteria for their 
(effective) termination, and carefully analyzing their 
relative strength. Next, we proceed in the analysis of DCTRSs 
using the recent tool of unravelings (cf.\ \cite{mALP96}. 
Unravelings allow to automatically infer properties 
of conditional rewriting systems by lifting existing results for 
unconditional rewriting, and to provide better intuitions on the new 
phenomena occurring in conditional rewriting resorting on the familiar 
concepts proper of TRSs. Here we develop an unraveling tailored for 
deterministic CTRSs, that allows to analyze the major properties 
of DCTRSs like (effective) termination and confluence. We also 
identify a distinguished subclass of DCTRS, called semilinear DCTRSs 
(SCTRSs), which are in a sense what left-linear TRSs are for TRSs. 
For this class, the analysis becomes particularly precise, allowing to 
develop new powerful results, and also providing intuitions on the 
intimate reasons motivating the results of previous works on DCTRSs. 
Moreover, using the developed unraveling, we are able to provide a bunch of 
new modularity results for DCTRSs. Besided the practical relevance of 
these results, they are particularly important since, 
to the best of our knowledge, there are so far no results at all on the 
modularity of 3-CTRSs. Finally, we hint at other relevant results on 
DCTRSs that can be inferred from our analysis.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Preliminaries}
We assume knowledge of the basic notions regarding conditional term 
rewriting systems and term rewriting systems (cf.\ \cite{DJ90,Klo92}). 
\smallskip

Given a sequence of terms $S$, $\Var(S)$ denotes the set of its variables. 
Two sequences $S_1$ and $S_2$ are said to be {\em disjoint\/} if they 
have no variables in common, i.e.\ $\Var(S_1)\cap\Var(S_2)=\ES$. 
A sequence is said to be {\em linear\/} if every variable occurs in it 
at most once. Also, given a sequence $S$ and a variable $X$, we denote 
with $|S|_X$ the number of occurrences of $X$ in $S$. 
Sequences in formulae 
should be seen just as abbreviations: for example, 
if $S$ is the sequence $t_1,t_2$, then $f(S)$ 
denotes the term $f(t_1,t_2)$. 

A term $s$ {\em overlaps\/} a term $t$ 
if there is a renaming 
$s'$ of $s$ that is disjoint with $t$ and unifiable with a non-variable 
subterm of $t$. If $s'$ is unifiable with $t$, then 
$s$ {\em overlays\/} $t$.

As usual, a partial ordering $\succ$ on terms is said: 
to be {\em closed under substitutions\/} if for every substitution 
$\sigma$, $s\succ t\Ra s\sigma\succ t\sigma$; to be {\em closed under 
contexts\/} if $s\succ t\Ra C[s]\succ C[t]$ for every context $C$; 
to have the 
{\em subterm property\/} if $C[t]\succ t$ for every context $C\neq\Box$. Also, 
$\succ_{\em st}$ denotes the smallest ordering that contains $\succ$ and 
has the subterm property.


Finally, we will use the 
acronyms \CON\ and \EQCON\ to denote respectively the properties of 
{\em consistency w.r.t.\ reduction\/} (a term cannot rewrite to two different 
variables) and {\em consistency\/} (two variables cannot be convertible).

\subsection{Oriented and Deterministic CTRSs}\label{subsec:ODCTRSs}

In this paper, we will mainly deal with so-called {\em oriented CTRSs\/} 
(briefly {\em OCTRSs\/}), that is to say CTRSs where the rules have the 
form
$$\detrule$$
(that is to say, the conditions are not symmetric, like 
in join CTRSs where they are of the form $s\downarrow t$, but they are 
oriented since one of the terms is required to rewrite to the other).
The term $t_0$, as usual, is said the {\em left-hand side\/} of the rule, 
$s_{k+1}$ the {\em right-hand side\/}, and the other terms make up the 
{\em conditions\/}.


In general, CTRSs are divided into four categories, according to the 
way variables are distributed in each rewrite rule (cf.\ \cite{MH94}). 
In the class of {\em 1-CTRSs\/}, the variables of the right-hand side 
and of the conditions are contained in the variables of the left-hand side 
(i.e., there are no ``extra variables'' w.r.t.\ the left-hand side). 
In the class of {\em 2-CTRSs\/}, 
the variables of the right-hand side are contained in those of the 
right-hand side (i.e., extra variables can be present in the conditions). 
In the class of {\em 3-CTRSs\/}, the variables of the right-hand side 
must be contained in union of the variables of the left-hand side with 
those of the conditions (i.e., extra variables are also admitted in the 
right-hand side, provided they appear in the conditions). Finally, 
the class of {\em 4-CTRSs\/} has no restrictions.

Deterministic CTRSs, introduced in \cite{BG89} (see also \cite{Gan91b}), are a 
particularly important class of 3-CTRSs:

\begin{definition}
A rule 
$$\detrule$$
is said to be {\em deterministic\/} if 
$\forall i\in[1,k+1].\:\Var(s_i)\subseteq\cup_{j<i}\Var(t_j)$. 
A CTRS is {\em deterministic\/} (briefly, a {\em DCTRS\/}), 
if each its rule is deterministic.
\end{definition}

As well known (and, indeed, this was one of the main stimuli to the 
study of 2- and 3-CTRSs), 
DCTRSs are tightly linked with functional programming, 
since every rule \detrule\ can be seen in a functional language as 

\begin{tabbing}
\hspace*{3.5cm}$t_0$ = {\tt let} \=$t_1=s_1$ {\tt in}\\
                   \>$\ddots$\=\\
 		   \>\>{\tt let} $t_k=s_k$ {\tt in} $s_{k+1}$
\end{tabbing}

That is to say, DCTRSs allows to capture the power of the functional 
{\em local definitions\/} provided by the 
{\tt let} constructs (or, equivalently, by the {\tt where} declarations).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SECTION
\subsection{Unravelings}\label{subsec:unravelings}

Unravelings have been introduced in \cite{mALP96}. Here we will only 
sketch the basic notions that will be needed in the sequel.

An unraveling is 
a map \GUNR\ associating to every CTRS an approximating TRS, in the sense 
that for every CTRS $R$, $\join_{R}\subseteq\join_{\GUNR(R)}$, and 
$\GUNR(T\cup R)=T\cup\GUNR(R)$ ($T$ a TRS). 
The first condition requires that the join relation of the 
unraveled CTRS is an extension of the original CTRS: informally, it means 
that the TRS does not compute `less' than its original CTRS; more formally, 
it states that the unraveled CTRS does not have less logical strength 
(cf.\ \cite{DOS88,DO90}) than the original CTRS. 
The second condition says that 
if we are unraveling a CTRS, we can extract from it the part that is 
already a TRS, and then go on computing the unraveling.
An unraveling is said to be {\em tidy\/} if it 
satisfies the following properties: 1) Compositionality: $\GUNR(T_1\cup T_2)=\GUNR(T_1)\cup\GUNR(T_2)$ \ 2) Finiteness: $R$ finite $\Ra$ $\GUNR(R)$ finite 
\ 3) The unraveling of the empty TRS is the empty TRS. 
The first 
condition expresses the fact that the unraveling is 
compositional, i.e.\ that we can incrementally build up the unraveling 
of a CTRS by computing the unravelings of its parts. The second 
says that finite objects are mapped into finite objects, and the third 
condition implies that the unraveling of a TRS $T$ is just $T$. 
By compositionality, tidy unravelings only need to be defined on single rules. 
Moreover, they are the identity function when restricted to TRSs. 
So, when defining a tidy unraveling we can only define it 
for rules with a non-void conditional part.
\smallskip

Unravelings allow to study properties of a CTRS by studying a corresponding 
property on the unraveled TRSs, the so-called ultra-property:

\begin{definition}\label{def:ultraproperty}
Let \calP\ be a property and \GUNR\ be an unraveling. 
The property \ultra{\calP}\ (w.r.t.\ \GUNR), briefly $\GUNR(\calP)$, is 
defined as follows: 
$ T\in \ultra{\calP} \Leftrightarrow \GUNR(T)\in\calP$. 
An unraveling is said to be {\em sound\/} (resp.\ {\em complete\/}) 
for a property \calP\ if $\ultra{\calP}\Ra\calP$ 
(resp.\ $\ultra{\calP}\Leftrightarrow\calP$). 
Moreover, we say that an unraveling {\em preserves\/} the 
property \calP\ if $\calP\Ra\ultra{\calP}$.
\end{definition}

Soundness allows to infer the property \calP\ of a CTRSs just by studying 
\calP\ for the corresponding unraveled TRS, this way enabling to 
automatically lift every result on \calP\ for TRSs to CTRSs. 
In addition, preservation allows to extend a property of TRSs (\calP) to 
CTRSs ($\ultra{\calP}$). 
For instance, consider the duplication property: while this 
syntactic property makes sense for TRSs, it is rather awkward to say what 
is the proper extension of this concept to 3-CTRSs. Soundness and preservation 
allows to use ultra-duplication as a suitable extension. 
So far, the 
standard approach was to pass from \calP\ to ``\calP\ for CTRSs'' 
simply by forgetting about the conditional part of each 
rule, and applying \calP\ to the obtained ``unconditional'' TRS. This 
approach stays within the unraveling methodology,, since it is 
nothing but $\ultra{\calP}$ w.r.t.\ the so-called trivial unraveling 
{\em u\/}, that translates each conditional rule $l\to r\La\LL$ into 
$l\to r$ (it is easy to check {\em u\/} is indeed an unraveling). 
However, the problem is that {\em u\/} may not be sound for \calP, or 
if it is so $\ultra{\calP}$ may be too weak to be of great interest 
({\em u\/} gives very lossy approximant TRSs, since it just discards 
all the conditional part). Using better approximants (better unravelings), 
we can thus get better approximants of the right extension property.
\smallskip

Unravelings also provide a tool to automatically transfer modularity 
results obtained in the TRSs field to CTRSs. 
Recall that a map $\mu$ is said to be {\em compositional\/} 
w.r.t.\ an operator 
$\op$ ($\op$-compositional for short) if 
$\forall R,S.\:\mu(R\op S)=\mu(R)\op \mu(S)$.  
The following fundamental result explains why unravelings are 
so useful for the study of modularity:

\begin{theorem}\label{teo:modularity}
Suppose an unraveling is $\op$-compositional. 
Then \calP\ is \op-modular for TRSs $\Ra$ \ultra{\calP}\ is $\op$-modular 
for CTRSs. Moreover, if the unraveling is complete for \calP, 
then \calP\ is \op-modular for TRSs $\Leftrightarrow$ \calP\ is 
\op-modular for CTRSs.
\end{theorem}

\section{Termination}\label{sec:termination}

As well known, for finite 
CTRSs the termination of the rewrite relation does not 
imply its decidability (cf.\ \cite{Kap84}). What we need in order to 
ensure that a finite CTRS is computationally feasible is 
{\em effective termination\/} 
(\cite{mALP96,Kap87,JW86,DOS88,DO90}): a CTRS $R$ is effectively terminating 
if $\tto{R}$ is terminating 
and it is decidable whether $s\tto{R}t$, $s\mmto{R}t$, $s\join_R t$, and 
if a term is in normal form. From now on, within this section we assume 
every CTRS to be finite.
\smallskip

As far as 1-CTRSs are concerned, three criteria that guarantee effective 
termination have been developed: 
{\em simplifyingness\/} (\cite{Kap87}), {\em reductivity\/} 
(\cite{JW86}) and {\em decreasingness\/} (\cite{DOS88}). We recall here 
these basic notions:

\begin{definition}
A CTRS is {\em simplifying\/} if there is a simplification 
ordering $\succ$ such that for each its rewrite rule \joinrule, we have 
$s_i\prec t_0\succ t_i$ ($i\in[1,k+1]$).
\end{definition}

\begin{definition}\label{def:decreasing} 
A CTRS $R$ is {\em decreasing\/} if there is a partial order $\succ$ that is 
well-founded, has the subterm property, extends the rewrite relation of $R$ 
(i.e.\ $\tto{R}\subseteq \succ$), and such that for each rule \joinrule\ of 
$R$, and substitution $\sigma$, we have 
$s_i\sigma\prec t_0\sigma \succ t_i\sigma$ for every $i\in[1,k]$.
\end{definition}

Reductivity is like decreasingness, but for the fact that $\succ$ 
is required to be closed under contexts instead of having the subterm property.
\smallskip

We have that 
simplifyingness $\Ra$ reductivity $\Ra$ decreasingness, and all the 
implications are strict. 

The interest in simplifyingness lies in the fact 
that it is easily automatizable, for instance via RPO's. 
\smallskip

These criteria have been developed for join CTRSs; however, it is trivial 
to see that they also also hold for OCTRSs. 

Nevertheless, when dealing with OCTRSs, we can further refine these notions 
by taking advantage of the orientation of the conditions. So, we introduce 
these two new concepts:

\begin{definition}
An oriented CTRS is {\em o-simplifying\/} if there is a simplification 
ordering $\succ$ such that for each its rewrite rule 
$t_0\to s_{k+1}\Leftarrow s_1\to^* t_1, \LL,$ $s_k\to^* t_k$, %% break...
we have 
$t_0\succ s_i$ ($i\in[1,k+1]$).
\end{definition}

\begin{definition}
An oriented CTRS $R$ is {\em o-decreasing\/} if there is a partial ordering 
$\succ$ that is well-founded, has the subterm property, 
$\tto{R}\subseteq\succ$, and such that for each rule of $R$, 
\detrule, and substitution $\sigma$, we have 
$t_0\sigma\succ s_i\sigma$ ($i\in[1,k]$).
\end{definition}

The following results justify the introduction of these concepts, showing 
they behave analogously to the simplifyingness and reductivity criteria:

\begin{theorem}
Every o-decreasing OCTRS is effectively terminating.
\end{theorem}

\begin{theorem}
For OCTRSs, o-simplifying $\Rightarrow$ o-decreasing, and 
o-simplifying $\not\Leftarrow$ o-decreasing.
\end{theorem}

\begin{corollary}
Every o-simplifying OCTRS is effectively terminating.
\end{corollary}

As far as the power of these criteria is concerned, we have:

\begin{theorem}
For DCTRSs, decreasing $\Rightarrow$ o-decreasing and 
simplifying $\Rightarrow$ o-simplifying. For normal CTRSs, 
decreasing $\not\Leftarrow$ o-decreasing, and 
simplifying $\not\Leftarrow$ o-simplifying.
\end{theorem}

That is to say, o-decreasingness is strictly more powerful than 
decreasingness, even when restricting to normal CTRSs, and the same 
holds for o-simplifyingness w.r.t.\ simplifyingness.
\medskip

We now focus on DCTRSs. For these class of 3-CTRSs, the criterion 
of {\em quasi-reductivity\/} has been developed (cf.\ \cite{BG89,Gan91b,GW92}):

\begin{definition}
A DCTRS $R$ is {\em quasi-reductive\/} if there is a partial ordering 
$\succ$ that is well-founded, closed under contexts and substitutions, 
and such that for every rule of $R$, 
\detrule, and substitution $\sigma$, we have that 
$$
\left(\bigwedge_{1\leq j\leq i}\sigma(s_i)\succeq\sigma(t_j)\right) \Ra 
\sigma(t_0)\succ_{\em st}\sigma(s_{i+1})\qquad\qquad (i\in[0,k])
$$
and that 
$$
\left(\bigwedge_{1\leq j\leq k}\sigma(s_i)\succeq\sigma(t_j)\right) \Ra 
\sigma(s_0)\succ\sigma(s_{k+1})
$$
\end{definition}

It has been proved in \cite{Gan91b} that quasi-reductivity implies 
effective termination. 

Compared to reductivity and decreasingness, the following result holds:

\begin{theorem}
For DCTRSs, quasi-reductive $\not\Rightarrow$ decreasing, and 
quasi-reductive $\not\Leftarrow$ reductive. 
\end{theorem}

This means that quasi-reductivity is not more powerful than 
reductivity or decreasingness, and vice versa. However, the interest 
in quasi-reductivity lies in the fact that while the latter criteria 
only cope with 1-CTRSs, quasi-reductivity allows to deal with DCTRSs 
that are not 1-CTRSs.

We will now introduce a new concept, which can be seen as the extension 
of (o-)decreasingness to DCTRSs:

\begin{definition}
A DCTRS $R$ is {\em d-decreasing\/} if there is a partial ordering 
$\succ$ that is well-founded, has the subterm property, 
$\tto{R}\subseteq\succ$, and such that for each rule of $R$, 
\detrule, and substitution $\sigma$, we have 
$$
\left(\bigwedge_{1\leq j\leq i}\sigma(s_j)\succeq\sigma(t_j)\right)
\Ra \sigma(t_0)\succ\sigma(s_{i+1})\qquad(i\in[0,k])
$$
\end{definition}

As expected, we have the following result:

\begin{theorem}
Every d-decreasing DCTRS is effectively terminating.
\end{theorem}

As far as the power of this criterion w.r.t.\ the others is concerned, we have:

\begin{theorem}
For DCTRSs, o-decreasing $\Rightarrow$ d-decreasing. 
For normal CTRSs, o-decreasing $\not\Leftarrow$ d-decreasing.
\end{theorem}

That is, d-decreasingness is strictly more powerful than 
o-decreasingness (and thus than decreasingness), even when 
restricting to normal CTRSs.

\begin{theorem}\label{teo:qrVSdd}
For DCTRSs, quasi-reductive $\Rightarrow$ d-decreasing, and 
quasi-reductive $\not\Leftarrow$ d-decreasing.
\end{theorem}

So, d-decreasingness is more powerful than quasi-reductivity as well.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SECTION
\section{The Unraveling}\label{sec:DUNR}

In this section we will develop an unraveling for DCTRSs.

We assume that CTRSs are composed of terms from a certain set \TERMS, built up 
from variables \calV\ and function symbols \calF. Also, 
when unraveling a CTRS into a TRS we will need some extra symbols: for 
every conditional rule $\rho$ we take new fresh symbol $\calU_{\rho}^i$ 
($i\in\Nat$): 
thus, we consider a set \ETERMS\ of `extended terms' to be the terms obtained 
from the variables \calV\ and the terms \calF\ plus these new symbols 
$\calU_{\rho}^i$.

Finally, we employ an operator $\VAR$ that, once applied to a term, 
gives the sequence of its variables in some fixed order 
(e.g.\ left-to-right writing order): for example, $\VAR(f(X,g(Y,Z),Y))$ gives the sequence $X,Y,Z,Y$.

\begin{definition}\label{def:DUNR}{\bf (Unraveling \DUNR)}\\
Take a rule \FULLdetrule\ ($k\geq 1$). 
Its (tidy) unraveling $\DUNR(\rho)$ is equal to 
$$
\begin{array}{l}
t_0\to \UUU_{\rho}^1(s_1,\VAR(t_0))\\
\UUU_{\rho}^j(t_j,\VAR(t_0,\LL,t_{j-1}))\to \UUU_{\rho}^{j+1}(s_{j+1},\VAR(t_0,\LL,t_j))
\qquad (1\leq j\leq k)\\
\UUU_{\rho}^k(t_k,\VAR(t_0,\LL,t_k-1))\to s_{k+1}
\end{array}
$$
\end{definition}

This mapping can be explained as follows. The first rule starts the 
verification of the conditions, beginning from the first one 
($s_1\to^*t_1$). If this condition is verified, the subsequent rule 
$\UUU_{\rho}^0(t_0))\to \UUU_{\rho}^{1}(s_{1},\VAR(t_0,t_1))$ can be 
applied, and the second condition ($s_2\to^*t_2$) is tested. This 
process goes on until, if all the conditions are satisfied, the last 
rule $\UUU_{\rho}^k(t_k,\VAR(t_0,\LL,t_k-1))\to s_{k+1}$ is applied, 
thus completing the simulation of the original conditional rewrite rule. 
We also need some form of parameter passing in order to transfer the 
computed results from one rule to another, and this is accomplished 
by the occurrences of $\VAR$ that store the (content of) the variables 
of the $t_i$'s.

\begin{example}\label{exa:fib}
Consider the following classic DCTRS computing Fibonacci numbers:
$$
\begin{array}{l}
\rho1:\:0+X\to X\\
\rho2:\:s(X)+Y\to X+s(Y)\\
\rho3:\:{\em fib\/}(0)\to {\em pair\/}(s(0),0)\\
\rho4:\:
{\em fib\/}(s(X))\to {\em pair\/}(W,Y)\La {\em fib\/}(X)\to^*{\em pair}(Y,Z), 
Y+Z\to^*W
\end{array}
$$
Its unraveled TRS using \DUNR\ consists of the unconditional rules $\rho1$, 
$\rho2$ and $\rho3$, plus the rules 
$$
\begin{array}{l}
{\em fib\/}(s(X))\to\UUU_{\rho4}^1(fib(X),X)\\
\UUU_{\rho4}^1({\em pair}(Y,Z),X)\to \UUU_{\rho4}^2(Y+Z,X,Y,Z)\\
\UUU_{\rho4}^2(W,X,Y,Z)\to {\em pair\/}(W,Y)
\end{array}
$$
\end{example}

The mapping \DUNR\ safely approximates the structure of a DCTRS, since:

\begin{theorem}\label{teo:DUNR-unraveling}
\DUNR\ is a (tidy) unraveling for DCTRSs.
\end{theorem}

The following soundness results allow to use \DUNR\ for the study of 
the corresponding properties:

\begin{theorem}\label{teo:DUNR-sound-termination}\label{teo:DUNR-sound-ISN}
For DCTRSs, \DUNR\ is sound for termination and innermost termination.
\end{theorem}

\begin{theorem}\label{teo:DUNR_sound-CON}\label{teo:DUNR-sound-EQCON}
For DCTRSs, \DUNR\ is sound for \CON\ and \EQCON.
\end{theorem}

In the next two subsections, we will first focus on the effective 
termination analysis, 
and then on the extension of syntactical properties of TRSs to DCTRS.

\subsection{Effective Termination}\label{subsec:E-SN}

In order to face the problem of effective termination, the 
obvious approach is to use ultra-termination. 
Comparing ultra-termination and d-decreasingness, we have that 

\begin{lemma}\label{lem:NOdecreasing}
For DCTRSs, Ultra-termination $\Ra$ d-decreasingness
\end{lemma}

Hence, ultra-termination guarantees effective termination:

\begin{corollary}
Ultra-terminating finite DCTRSs are effectively terminating.
\end{corollary}

As far as the power of ultra-termination is concerned, we have the following 
result:

\begin{theorem}
For DCTRSs, 
\begin{center}
quasi-reductivity $\not\Rightarrow$ ultra-termination $\not\Rightarrow$ o-decreasingness\end{center}
and
\begin{center}
quasi-reductivity $\not\Leftarrow$ ultra-termination $\not\Leftarrow$ o-decreasingness.
\end{center}
\end{theorem}

That is to say, quasi-reductivity 
and o-decreasingness are not more powerful than ultra-termination, and 
vice versa.

On the other hand, note that ultra-termination is of great practical 
importance since it can be checked by utilizing all the existing (and 
future) techniques to prove termination of TRSs. 

For instance, let us consider one of the most successful techniques developed 
for TRSs: simplification orderings. We have already provided in Section 
\ref{sec:termination} the criterion of o-simplifyingness, which is the 
natural extension of Kaplan's simplifyingness criterion developed for 
1-CTRSs. What about, instead, verifying ultra-termination 
using simplification orderings on the unraveled TRS, i.e.\ using 
{\em ultra-simplifyingness\/}? On the practical side, 
ultra-simplifyingness is particularly appealing, since one does not have 
to develop from the scratch a checker (like in the 
Kaplan's simplifyingness and o-simplifyingness cases), but can directly 
employ all the numerous existing implementations for TRSs. 
On the theoretical side, the power of the approach is clarified 
by the following result:

\begin{lemma}\label{lem:morepowerful}
For DCTRSs, 
ultra-simplifyingness is strictly more powerful than o-simplifyingness.
\end{lemma}

\subsection{Syntactical Properties}

We now turn to the problem of extending the major syntactical 
properties from TRSs to DCTRSs.

\begin{lemma}\label{lem:preservation}
For DCTRSs, \DUNR\ is complete for the following properties: 
being non-collapsing, non-erasing, an overlay system.
\end{lemma}

It turns out that all the ultra-properties of the above three properties 
are just the standard properties ``for CTRSs'' (cf.\ Subsection 
\ref{subsec:unravelings}), thus giving an indication that the standard 
extensions are the correct ones.

Two other major syntactical 
properties remain: non-duplication and left-linearity. This time, \DUNR\ 
is not complete (more precisely, the above two properties are not 
preserved), thus indicating that the standard extensions of these 
properties are not the right ones. We will so investigate the corresponding 
ultra-properties. The case of left-linearity is so important that we 
will face it in the next section. As far as non-duplication 
is concerned, \DUNR\ is complete for ultra-nonduplication, as it is easy 
to see (note that in general this is not automatically true, since 
only the preservation of $\ultra{\calP}$ is guaranteed, but not the 
soundness). Therefore, we can safely employ ultra-nonduplication. 
The definition of this ultra-property can be also expressed in a 
more expressive, syntactic way, that is independent from the 
unraveling \DUNR:

\begin{lemma}\label{lem:non-ultraduplicating}
A DCTRS is ultra-non-duplicating 
if and only if for each of its rules $t_0\to s_{k+1}\Leftarrow s_1\to^* t_1,\LL,$ $s_k\to^* t_k$
the terms $s_1,\LL,s_k$ are ground, and for every variable 
$X$, $|s_{k+1}|_X\leq|t_0,\LL,t_k|_X$.
\end{lemma}

We will see the applications of ultra-nonduplication in Section 
\ref{sec:det-modularity}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SECTION
\section{Semilinear DCTRSs}\label{sec:SCTRSs}

For TRSs, left-linearity is such an important property that it is 
of utmost relevance to try to see what is its correct extension for (3-)CTRSs. 
Like in the non-duplication case, we are lucky since \DUNR\ is complete 
for ultra-left-linearity, and so we can safely employ this notion. 
Analogously, we can reformulate it in a completely syntactic way 
without mentioning the unraveling \DUNR. Since also the adjective 
``ultra-left-linear'' is a bit verbose (and refers implicitly to \DUNR), 
we use an alternative acronym: semilinear.

\begin{definition}
A DCTRS is said to be {\em semilinear\/} (briefly, an {\em SCTRS\/}), 
if for each its rewrite rule 
\detrule\ the sequence $t_0,\LL,t_k$ is linear.
\end{definition}

It is easy to verify that semilinearity coincides with ultra-left-linearity.
\smallskip

Semilinearity has also a significance when recalling the importance 
of DCTRSs for functional programming. Indeed, most 
of functional languages (eg ML, CLEAN, Haskell etc.) require the defining 
patterns to be left-linear: this, recalling the parallelism between 
DCTRSs and functional programs seen in Subsection \ref{subsec:ODCTRSs}, is tantamount to 
requiring semiliinearity of the DCTRS.
\smallskip

The key result that distinguishes semilinear DCTRSs is that their 
structure is completely preserved by the unraveling \DUNR:

\begin{theorem}\label{teo:NORMALfundamental}
For every SCTRS $R$, 
$\forall s,t\in\TERMS.\: s\mmto{R}t \Leftrightarrow s\mmto{\DUNR(R)}t$
\end{theorem}

That is to say, when restricted to \TERMS, an SCTRS $R$ and its 
unraveled TRS $\DUNR(R)$ have the same rewrite relation $\mmto{R}$.

This, in turn, implies that we can obtain a more precise analysis of 
an SCTRS using ultra-properties, as we will see in the next subsections.

\subsection{Effective Termination for SCTRSs}
We face again the problem of effective termination, this time for 
SCTRSs. We have seen that ultra-termination for 
DCTRSs provides a powerful criterion for effective termination. Yet, it is 
not as powerful as d-decreasingness. Quite surprisingly, in the 
SCTRSs case we manage to reach d-decreasingness, since the 
following result holds:

\begin{theorem}\label{teo:NORMALdecreasing}
For SCTRSs, ultra-termination = d-decreasingness.
\end{theorem}

Hence, the 
notion of d-decreasingness is provided with a much more 
meaningful justification, 
being just the termination of the unraveled CTRS. 

Note that all the difficulties and possible objections 
in expressing what the `right notion' of 
effective termination is, are nicely coped with using ultra-termination: 
the leading intuition was that things for effectively terminating DCTRSs 
should be like for terminating TRSs; and ultratermination is just the 
concept that the TRS corresponding to a DCTRS terminates.

\subsection{Confluence for SCTRSs}

\begin{theorem}\label{teo:DUNR-sound-CR}
For SCTRSs, \DUNR\ is sound for confluence.
\end{theorem}

An immediate corollary of the above result and of Theorem 
\ref{teo:DUNR-sound-termination} is that also completeness can be coped with:

\begin{corollary}\label{cor:DUNR-sound-COMP}
For SCTRSs, \DUNR\ is sound for completeness.
\end{corollary}

Theorem \ref{teo:DUNR-sound-CR} 
enables us to lift every result on the confluence of left-linear TRSs, 
giving new insights on the reasons and failures of existing criteria for 
confluence. 

So far, there are two recent powerful results on the confluence of DCTRSs. 
The first is that of \cite{AL94b}, where Avenhaus and Lor\'{\i}a-S\'aenz 
proved that a DCTRS is confluent if it is ``strongly deterministic'', 
quasi-reductive and with convergent conditional critical pairs. 
The other one is that of \cite{SMI95}, where Suzuki, Middeldorp and Ida 
proved that every orthogonal ``properly oriented'' and ``right stable'' 
3-CTRS is (level-)confluent.

These two results resemble the two well-known major criteria for 
confluence of TRSs, namely respectively the fact that a terminating 
TRSs with convergent critical pair is convergent, and the result that 
orthogonal TRSs are confluent. However, the authors had to face a number 
of new problems and phenomena occurring in the 3-CTRSs realm, as 
is well-illustrated in \cite{AL94b,SMI95}. 
For instance, consider these two SCTRS after \cite{AL94b}:
$$
\begin{array}{l}
\calR_1=\left\{
\begin{array}{l}
0+X\to X\\
s(X)+Y\to X+s(Y)\\
f(X,Y)\to Z\La X+Y\to^*Z+Z'
\end{array}
\right.
\\
\mbox{ }\\
\calR_2=\left\{
\begin{array}{l}
a\to c\\
g(a)\to h(b)\\
h(b)\to g(c)\\
f(X)\to Z\La g(X)\to^* h(Z)
\end{array}
\right.
\end{array}
$$
These two SCTRSs are both orthogonal and terminating (even quasi-reductive). 
Nevertheless, they are not confluent. 
$\calR_1$ is not confluent, since $f(s(0),0)$ reduces both to 
$s(0)$ and to $0$. 
Here the problem is with the overlapping of a rule with itself (at root 
level): this new phenomenon is called {\em improper critical pair\/} in 
\cite{AL94b}. 
Also, $\calR_2$ is not confluent, since $f(a)$ reduces both to $f(c)$ and to 
$b$. The problem here is called {\em variable overlappingness\/} in 
\cite{AL94b}.
\smallskip

All of these apparent different and weird new phenomena, clashing with 
the intuitions developed for TRSs, can be better 
comprehended and unified using ultra-confluence. 
Indeed, when unraveling the two above SCTRSs we have that: 
in $\calR_1$, $Z+Z'$ overlaps with the lhs's of 
the other non conditional rules; in $\calR_2$, 
$h(Z)$ overlaps with the lhs of the second rule, $h(b)$.

Thus, orthogonality is only apparent: indeed, what we are lead to 
consider is just orthogonality ``for CTRSs'' (cf.\ Subsection 
\ref{subsec:unravelings}), which is not the correct notion, since \DUNR\ is 
not complete for this property. The correct notion is obtained by 
using ultra-orthogonality, which gives the following major result:

\begin{theorem}
Ultra-orthogonal SCTRSs are confluent.
\end{theorem}
\begin{proof} By lifting 
the well-known fact that orthogonal TRSs are confluent (being \DUNR\ 
sound for confluence and complete for ultra-orthogonality).
\end{proof}

Ultra-orthogonality can be syntactically expressed without mentioning 
\DUNR:

\begin{lemma}
An SCTRS $R$ is ultra-orthogonal if and only if for each its rule 
\FULLdetrule\ 
there is not a left-hand side of a rule 
in $R$ that overlaps a $t_i$ ($i\in[0,k]$), 
but for the trivial overlay of the left-hand side of $\rho$.
\end{lemma}

Note that ultra-orthogonality (like orthogonality) is a decidable 
criterion. 
The problem with the criterion given in \cite{AL94b}, even assuming 
quasi-decreasingness of the DCTRS, being ``strongly deterministic'' 
is undecidable. Thus, in the same paper the authors also give a powerful 
decidable criterion for being strongly deterministic, namely being 
{\em absolutely deterministic\/}.  
Interestingly, it is easy to see that for orthogonal SCTRSs, 
{\em being absolutely deterministic is the same as being ultra-orthogonal\/}: 
thus, we are able to automatically reconstruct the right notions ensuring 
confluence of a DCTRS (also, the more general, and undecidable, notion 
of being ``strongly deterministic'' is, rather reasonably, obtained by 
loosening the non-overlapping condition of the $t_i$'s requiring that 
all their instances are irreducible). However, note the fundamental 
difference, that in our case we {\em do not require\/} not only 
quasi-reductivity, but termination at all (on the other hand, we cope 
only with SCTRSs). For instance, the Fibonacci SCTRS of Example 
\ref{exa:fib} can be immediately proved confluent, since it is readily 
ultra-orthogonal, without having to prove its quasi-reductivity.


To this extent, a similar result is that obtained in the other aforementioned 
paper, \cite{SMI95}, which can be seen as an attempt to lift the 
orthogonality criterion of TRSs to 3-CTRSs. Again, the obtained 
conditions, when restricted to SCTRSs, are also very similar (while 
``properly orientedness'' is a condition alike to determinism, their 
other condition, ``right stability'', is extremely similar to 
ultra-orthogonality). 
As far as the relative strength of the approaches is concerned, 
their criterion is not more powerful than ultra-orthogonality, 
and vice versa (although it should be noticed that their criterion is 
able to prove not only confluence, but level-confluence).
\smallskip

Finally, another criterion that we can automatically obtain is the 
lifting of the other major criterion for TRSs previously mentioned:

\begin{theorem}
A d-decreasing SCTRS $R$ is confluent if every critical pair 
of $\DUNR(R)$ is convergent.
\end{theorem}
\begin{proof}
By the fact that for terminating TRSs convergence of critical pairs implies 
confluence (being d-decreasingness equivalent to ultra-termination, and 
\DUNR\ sound for termination and confluence).
\end{proof}

Again, note the similarity with the criterion of \cite{AL94b}. 
Regarding the power, again, the two criteria are uncomparable each other.
\smallskip

In a nutshell, although in this case we showed that we can automatically 
obtain results not subsumed by the other works, we do not claim that 
unravelings necessarily provide each time such powerful solutions. 
Rather, we claim that they should be seen as 
a tool to provide a better understanding of the new phenomena occurring 
with 3-CTRSs, resorting on the familiar experience gained for TRSs: 
unravelings can provide right away new criteria for free, lifting old 
ones of TRSs, and thus providing the correct intuitions on how to 
get better criteria.

\subsection{Consistency w.r.t.\ reduction for SCTRSs}

Finally, \DUNR\ allows to fully grasp the property of 
consistency w.r.t.\ reduction:

\begin{theorem}\label{teo:DUNR-complete-CON}
For SCTRSs, \DUNR\ is complete for \CON.
\end{theorem}

This means there is no loss of precision when studying \CON\ of a SCTRS $R$  
using \DUNR: we can simply use the corresponding TRS $\DUNR(R)$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SECTION
\section{Modularity}\label{sec:det-modularity}
As said in the introduction, so far, to the best of our knowledge, 
{\em there are no results on the 
modularity of 3-CTRSs\/}. Using unravelings, we can get for free a bunch 
of new powerful results, simply lifting to DCTRSs the existing results 
on the modularity of TRSs.

In order to do this, the unraveling must be compositional w.r.t.\ the 
composition operator (cf.\ Subsection \ref{subsec:unravelings}). 
The main 
modularity operators so far introduced 
(cf.\ e.g.\ \cite{Ohl95,Klo92,mALP96}), 
are: {\em disjoint union\/} 
$\oplus$ (disjoint signatures); {\em constructor-sharing union\/} $\csplus$ 
(sharing only of constructor symbols); 
{\em composable union\/} $\compplus$ (alike $\csplus$ but, in addition, 
rules defining shared defined symbols are shared); and 
{\em hierarchical union\/} $\hierplus$: 
two OCTRSs $R_1$ and $R_2$ can be composed via $\hierplus$ if 
$R_1$ does not have defined symbols of $R_2$, and for every rule 
\detrule\ 
of $R_2$ no defined symbol of $R_1$ appears in $t_0,\LL,t_k$. 

The next result shows that all of these operators can be coped with:

\begin{theorem}\label{teo:compositional-laws} 
\DUNR\ is compositional w.r.t.\ the operators $\oplus$, $\csplus$, 
$\compplus$ and $\hierplus$.
\end{theorem}

Hence, by this result we can use Theorem \ref{teo:modularity} 
to lift every modularity result for TRSs to DCTRSs. 
In order to save space and enhance readability, in the subsequent proofs 
we will usually consider usage of the aforementioned 
method to be understood, and just name the original modularity property 
of TRSs that is lifted.

\subsection{Modularity of DCTRSs}

\subsubsection*{Termination}

\begin{theorem}
Ultra-termination is modular for non-collapsing composable DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for 
non-collapsing composable TRSs (\cite{Ohl95}).
\end{proof}

\begin{theorem}
Ultra-termination is modular for ultra-non-overlapping composable DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for 
non-overlapping composable TRSs (\cite{Der94,Ohl95}).
\end{proof}

\begin{theorem}
Ultra-termination is modular for non-ultraduplicating composable DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for 
non-duplicating composable TRSs (\cite{Gra94,Ohl95}).
\end{proof}

The modularity of 
\CE-termination	(cf.\ \cite{Ohl94tcs,Gra94}) is one of the most powerful 
results ever obtained for TRSs. Recall that a TRS $T$ 
is said to be \CE-terminating if $T\oplus\ToyTWO$ is terminating 
(cf.\ \cite{Ohl94tcs}). The 
lifted ultraproperty can be expressed in a similar way: it can be 
proved that {\em $T$ is \ultra{\CE-terminating} iff 
$T\oplus\ToyTWO$ is ultra-terminating\/}. Thus we get:

\begin{theorem}\label{teo:ultra-CE-modular}
Ultra-\CE-termination is modular for DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of \CE-termination for TRSs (\cite{Gra94,Ohl94tcs}).
\end{proof}

This result is particularly relevant in view of the practical importance 
of ultra-simplifyingness (cf.\ Subsection \ref{subsec:E-SN} and Lemma 
\ref{lem:morepowerful}):

\begin{theorem}
Ultra-simplifyingness is modular for composable DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of simplifyingness for 
composable TRSs (\cite{KO90}).
\end{proof}

\begin{theorem}
Ultra simple termination is modular for DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of simple termination for 
composable TRSs (\cite{KO90}).
\end{proof}

As far as hierarchical union is concerned, Krishna Rao in 
\cite{Rao94} proved that simplifyingness is modular 
for hierarchical TRSs forming a `proper extension'. 
From his result we obtain: 

\begin{theorem}\label{teo:hier-SIMP}
Ultra-simplifyingness is modular for hierarchical DCTRSs 
forming a `ultra proper extension'.
\end{theorem}

Unravelings allow to lift not only ``classic'' modularity results, but 
also ``hybrid'' results like the ones obtained by Middeldorp and 
Ohlebusch: Middeldorp in \cite{Mid89b} proved that if one of two 
terminating TRSs is both non-collapsing and non-duplicating, then their 
disjoint sum is terminating as well. Later, Ohlebusch (\cite{Ohl95}) 
managed to extend this result to 
composable union of TRSs. 

\begin{theorem}
If one of two ultra-terminating DCTRSs is both non-collapsing and 
non-ultraduplicating, then their composable union is ultra-terminating.
\end{theorem}
\begin{proof}
Take two ultra-terminating DCTRSs $R$ and $R'$, with 
$R$ non-collapsing and non-ultraduplicating. We have that 
$\DUNR(R)$ is terminating, non-collapsing (by Lemma \ref{lem:preservation}) 
and non-duplicating. Hence, by the aforementioned result of \cite{Ohl95}, 
the composable union of $\DUNR(R')$ and $\DUNR(R)$ is terminating, 
which implies by Theorem \ref{teo:compositional-laws} that 
the composable union of $R$ and $R'$ is ultra-terminating.
\end{proof}

\subsubsection*{Other Properties}

Last but not least, we consider innermost termination and the consistency 
property:

\begin{theorem}
Ultra innermost termination is modular for composable DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of innermost termination for composable TRSs 
(\cite{Gra92,Ohl95}).
\end{proof}

\begin{theorem}
Ultra-\EQCON\ is modular for DCTRSs.
\end{theorem}
\begin{proof}
By the modularity of \EQCON\ for TRSs (\cite{SS89}).
\end{proof}

\subsection{Modularity of SCTRSs}\label{subsec:semilinear-modularity}
In the case of SCTRSs, several new powerful modularity results can be 
obtained. Here, in some proofs we will also implicitly use the 
fact that, for SCTRSs, \DUNR\ is (trivially) complete for left-linearity.

\subsubsection*{Termination}\label{subsec:mod-DCTRS-termination}

\begin{theorem}\label{teo:NORMAL-dec-nc-modular}
d-decreasingness is modular for non-collapsing composable SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for 
non-collapsing composable TRSs (\cite{Ohl95}).
\end{proof}

\begin{theorem}
d-decreasingness is modular for non-overlapping composable SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for 
non-overlapping composable TRSs (\cite{Der94,Ohl95}).
\end{proof}

\begin{theorem}
d-decreasingness is modular for non-ultraduplicating composable SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for 
non-duplicating composable TRSs (\cite{Gra94,Ohl95}).
\end{proof}

\begin{corollary}\label{cor:NORMAL-decr-modular-CE}
d-decreasingness is modular for ultra-\CE-terminating SCTRSs.
\end{corollary}
\begin{proof}
By Theorem \ref{teo:ultra-CE-modular}, 
since ultra-\CE-termination implies d-decreasingness.
\end{proof}

Regarding ultra-\CE-termination, note that 
it can be nicely expressed without using \DUNR, since it can be 
proved that {\em $T$ is \ultra{\CE-terminating} (for SCTRSs) iff 
$T\oplus\ToyTWO$ is d-decreasing\/}.

\begin{theorem}\label{teo:NORMAL-decr-modular-CON}
d-decreasingness is modular for \CON\ SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of termination for left-linear \CON\ 
TRSs (\cite{mJSC96,SSMP95}).
\end{proof}

\begin{theorem}\label{teo:NORMAL-dcriterion}
If one of two d-decreasing SCTRSs is both \CON\ and 
ultra-\CE-terminating, then their disjoint union is d-decreasing.
\end{theorem}
\begin{proof}
Take two d-decreasing left-linear normal CTRSs $R$ and $R'$, with 
$R$ \CON\ and 
ultra-\CE-terminating. 
$\DUNR(R)$ is both \CON\ (by Theorem \ref{teo:DUNR-complete-CON}) 
and \CE-terminating. Moreover, 
both $\DUNR(R)$ and $\DUNR(R')$ are readily left-linear. 
By the result proved in 
\cite{mTCS98} for TRSs, the disjoint union of 
$\DUNR(R)$ 
and $\DUNR(R')$ is terminating, which implies by Theorems 
\ref{teo:compositional-laws} and \ref{teo:NORMALdecreasing} that 
the disjoint union of $R$ and $R'$ is d-decreasing.
\end{proof}

\subsubsection*{Confluence}

\begin{theorem}\label{teo:CR-modular-COMP-CR}
Ultra-confluence is modular for non-collapsing composable SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of confluence for non-collapsing composable TRSs 
(\cite{Ohl95}).
\end{proof}

\begin{theorem}
Ultra-confluence is modular for constructor-sharing SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of confluence for left-linear constructor-sharing 
TRSs (\cite{RV80}).
\end{proof}

\begin{theorem}
Ultra-confluence is modular for hierarchical SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of confluence for hierarchical left-linear 
TRSs (cf.\ \cite{RV80}).
\end{proof}

Finally, we mention that we can also lift 
the recent result of Verma 
(\cite{Ver95}) on the modularity of confluence for 
{\sl {\it lr}-combinations\/} (a rather flexible and powerful kind of 
combination): without entering into details, we just mention that 
being \DUNR\ composable w.r.t.\ {\em lr\/}-combinations, we can lift this 
result obtaining a sufficient criterion for the confluence of 
{\em lr}-combinations of SCTRSs.

\subsubsection*{Other Properties}

As far as consistency w.r.t.\ reduction is concerned, we can obtain the 
following important result:

\begin{theorem}
\CON\ is modular for SCTRSs.
\end{theorem}
\begin{proof}
By the modularity of \CON\ for left-linear 
TRSs (see \cite{mJSC96,SSMP95,mTCS98}).
\end{proof}

Finally, we hint at the fact that, by Corollary \ref{cor:DUNR-sound-COMP}, 
we can lift by unravelings also all the results obtained 
for the completeness of hierarchical combinations of TRSs, namely those of 
Dershowitz (\cite{Der94}) and Rao (\cite{Rao93}).

\section{Further Applications}

In this final section we hint at 
other further powerful results that can be derived from the 
presented approach.

\subsection{Power of the Analysis}
We have seen that the better the approximant TRS (i.e., the better the 
unraveling), the more precise the analysis becomes. It is therefore 
natural to ask what is the intrinsic limit of the unraveling approach that 
we have successfully used in this paper. The best situation is when we 
manage to reach {\em completeness\/} of the unraveling for the given 
property: this means we are not losing information when passing from 
DCTRSs to TRSs. We have performed an abstract study of the unraveling 
approach for DCTRSs (along the same lines as done in \cite{mFSTTCS97} for 
TRSs and CTRSs), and shown that not only this is not possible 
for all the major properties of DCTRSs (termination, confluence, 
completeness etc.), but it is even impossible to faithfully translate a 
3-CTRS into a 2-CTRS, and a 2-CTRS into a 1-CTRS (the gap 
from 1-CTRSs to TRss is already known from \cite{mALP96}). 
In other words, there are expressive gaps inbetween each couple of 
classes, so we have no hope to be able to fully analyze one of these 
classes when resorting on a more limited one: the analysis will always 
be approximate.

\subsection{Logic Programming}
DCTRSs have tight connections with logic programs, as shown in a nice paper 
(\cite{GW92}) by Ganzinger and Waldmann. Without entering into too much 
details, the idea is that a relevant class of logic programs (so-called 
well moded logic programs) can be elegantly translated in a natural way 
into DCTRSs, in such a way that proving quasi-reductivity of the obtained 
CTRS implies termination of the original logic program. This approach 
is extremely neat, the only disadvantage being that one has to prove 
quasi-reductivity of a DCTRSs, which may not be easy. On the other hand, 
another approach is to develop such a transformation of logic programs 
into TRSs, like done in \cite{RKS92} and further 
investigated in \cite{AM93,mLPTRS94,AZ96}. This methodology, conversely, 
is rather powerful, since proving termination of a TRS is generally 
much simpler than proving termination of CTRS, but not very elegant, 
since the transformations have the form of a low-level compilation. 
Using the results presented in this paper, we can combine the advantages 
of both approaches: first, the elegant transformation of \cite{GW92} 
is employed. Then, the obtained CTRSs is transformed into a TRSs using 
\DUNR, and analyzed for termination (i.e., we employ  
ultra-termination). Thus, we gather together the simplicity of the 
approach of \cite{GW92} with the effectiveness of the alternative 
approach of \cite{RKS92,AM93,mLPTRS94,AZ96}. Note that, in order for 
this approach to work, we had to extend the original result in 
\cite{GW92}, by proving that d-decreasingness of the corresponding CTRS 
implies termination of the original logic program.

\subsection{Other Properties}
In this paper we have analyzed DCTRSs for the 
properties of termination, innermost termination, confluence, and the 
consistency properties. 
Similarly, it is possible to use unravelings to study all the other 
main properties of DCTRSs, 
namely completeness, the normal form properties 
(uniqueness of normal forms w.r.t.\ reduction, uniqueness of normal 
forms, normal form property) and the normalization properties 
(weak normalization, innermost weak normalization, semicompleteness). 
In particular, \DUNR\ suffices to prove the normal forms properties, 
while for the normalization ones a slight variation is needed.

\subsection{$\pi$-CTRSs}

\begin{definition}
An OCTRS $R$ is {\em of type $\pi$\/} (briefly, a {\em $\pi$-OCTRS\/}) 
if for each rule $\detrule$ of $R$ the conditions are disjoint, that is to 
say $\forall i,j\in[1,k],i\neq j.\:\Var(s_i,t_i)\cap\Var(s_j,t_j)=\ES$
\end{definition}


The class of $\pi$-OCTRSs is of distinguished practical importance because 
of the following fact: when applying a rule, the conditions can be 
checked {\em in full parallel\/}, being completely independent one another. 
We consider now the class of $\pi$-SCTRSs. 
Being SCTRSs, $\pi$-CTRSs inherit all the good properties seen 
for this class. Also, it is not difficult to see that every o-simplifying 
SCTRS is a $\pi$-SCTRS. Moreover, we can develop some nice further results on 
their modularity, in view of the following fact. In \cite{mALP96} 
the unraveling \NUNR\ has been introduced for the study of normal CTRSs. 
Its definition is simply that each rule \FULLdetrule\ is translated into 
the two rules $t_0\to\UUU_{\rho}(s_1,\LL,s_k,\VAR(t_0))$ and 
$\UUU_{\rho}(t_1,\LL,t_k,\VAR(t_0))\to s_{k+1}$. Now, we have proved that 
all the results developed in \cite{mALP96} for normal CTRSs do extend to 
$\pi$-SCTRSs, thus when analyzing $\pi$-SCTRSs the simpler TRSs produced 
by $\NUNR$ can be used, in place of those produced by \DUNR\ (the 
drawback is a loss of power, since it can be proved that $\DUNR$ is 
strictly more powerful than $\NUNR$ for every major property). Moreover, 
an important new fact can be proved:

\begin{theorem}
For $\pi$-SCTRSs, 
\begin{center}
ultra-termination (w.r.t.\ \NUNR) = o-decreasingness.
\end{center}
\end{theorem}

Besides being important on its own, this theorem enables us to state a 
new bunch of results on the modularity of o-decreasingness: 
briefly, 
{\em all of the results\/} that we have proved for (the modularity of) 
d-decreasingness for SCTRSs (Subsection \ref{subsec:mod-DCTRS-termination})  
hold true for o-decreasingness, when considering $\pi$-SCTRSs.

%% \small
%% \input{alpbib.tex}
\bibliographystyle{plain}
\bibliography{TRS,MAX,FP,LP}

\end{document}
