%%\documentstyle[fullpage,11pt,amssymbols]{article}
\documentstyle[fullpage,11pt]{article} %%JRWG

%%
%% ENTCS style:
%%

%%JRWG \documentstyle[entcsmacro]{entcs}

% The following is enclosed to allow easy detection of differences in
% ascii coding.
% Upper-case    A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
% Lower-case    a b c d e f g h i j k l m n o p q r s t u v w x y z
% Digits        0 1 2 3 4 5 6 7 8 9
% Exclamation   !           Double quote "          Hash (number) #
% Dollar        $           Percent      %          Ampersand     &
% Acute accent  '           Left paren   (          Right paren   )
% Asterisk      *           Plus         +          Comma         ,
% Minus         -           Point        .          Solidus       /
% Colon         :           Semicolon    ;          Less than     <
% Equals        =           Greater than >          Question mark ?
% At            @           Left bracket [          Backslash     \
% Right bracket ]           Circumflex   ^          Underscore    _
% Grave accent  `           Left brace   {          Vertical bar  |
% Right brace   }           Tilde        ~

\def\english{0} 
%\input{amssym.def}
%\input{amssym}
%\input{diagrams} % Paul Taylor's Macro Package
\newcommand{\john}[1]{\{{\bf John:~\sf #1}\}} % Highlight text.
%\newcommand{\vin}[1]{\{{\bf Vincent:~\sf #1}\}} % Highlight text.
\newcommand{\vin}[1]{#1}
\newcommand{\elsevecho}[1]{}    %%JRWG Wanted for Elsevier
\newcommand{\elsevsupp}[1]{#1}  %%JRWG Suppressed for Elsevier
\newcommand{\zurab}[1]{\{{\bf Zurab:~\sf #1}\}} % Highlight text.
%\newcommand{\suppress}[1]{\{\{{\sf #1}\}\}} % Highlight text.
\newcommand{\suppress}[1]{} % Comment out text.
\newcommand{\delete}[1]{} % Comment out text.

% Vincent: definitions should go in preamble, i.e. here
\elsevsupp{%Vincent: already reserved by Elsevier: 
  \newtheorem{thm}{Theorem}[section]
  \newtheorem{lem}{Lemma}[section]
  \newtheorem{cor}{Corollary}[section]
  \newtheorem{rem}{Remark}[section]
  \newtheorem{prop}{Proposition}[section]
}
\suppress{%Vincent: Elsevier uses exmp:
  \newtheorem{ex}{Example}[section]
}
%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\suppress{%Vincent: Elsevier uses ack:
  \newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
}
\suppress{%Vincent: Elsevier uses pf:
  \newenvironment{proof}{\noindent{\bf Proof }}{}
}
\elsevsupp{%Vincent: Elsevier uses defn
  \newtheorem{deff}{Definition}[section]
  \newtheorem{defn}{Definition}[section]
}
\newcommand{\notation}{{\bf Notation }}
\suppress{%Vincent: reserved by Elsevier:
  \newcommand{\note}{{\bf Note }}
}
\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\impl}{\Rightarrow}
\def\doar{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\norm}[1]{\mbox{$\Vert #1 \Vert _{\mu}$}}
\newcommand \inputpic[1] {\begin{center} \input{#1} \end{center}} 
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\def\steq{\approx_{st}}
\def\leeq{\approx_L}
\def\equi{\approx}
\def\subt{\in}
\def\Mu{\Im}
\def\lleq{\triangleleft}
\def\lles{\triangleleft}
\def\leeqv{\approx_L}
\def\ind{\ddagger}
\newcommand{\sscl}[1]{\mbox{$\langle {#1}\rangle_s$}}
\newcommand{\ssc}[1]{\mbox{$\langle {#1}\rangle$}}
\def\Nset{N}
\suppress{vincent: don't abbreviate macros by macros says Elsevier
  \def\bd{\begin{deff}\em}
  \def\bdl{\begin{deff}\em\label}
  \def\bl{\begin{lem}\em}
  \def\bll{\begin{lem}\em\label}
  \def\bp{\begin{prop}\em}
  \def\bpl{\begin{prop}\em\label}
  \def\bt{\begin{thm}\em}
  \def\btl{\begin{thm}\em\label}
  \def\bel{\begin{ex}\em\label}
  \def\bc{\begin{cor}\em}
  \def\bcl{\begin{cor}\em\label}
  \def\bproof{\begin{proof}}
  \def\eproof{\end{proof}}
  \def\ed{\end{deff}}
  \def\el{\end{lem}}
  \def\ep{\end{prop}}
  \def\et{\end{thm}}
  \def\ee{\end{ex}}
  \def\ec{\end{cor}}
}

%%
%% ENTCS titlepage
%%

\def\lastname{Khasidashvili, Van Oostrom}
\begin{document}
\elsevecho{
\begin{frontmatter}
\title{Context-sensitive Conditional Expression Reduction Systems}
\author{Zurab Khasidashvili\thanksref{SUPPORT}}
\address{School of Information Systems \\
  University of East Anglia\\
  Norwich NR4 7TJ, England \\ 
  zurab@sys.uea.ac.uk}
\author{Vincent van Oostrom}
\address{Department of Mathematics and Computer Science\\
  Vrije Universiteit\\
  De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands\\
  oostrom@cs.vu.nl}
\thanks[SUPPORT]{Supported by the Engineering and 
  Physical Sciences Research Council of 
  Great Britain under grant GR/H 41300}
\begin{abstract}
  We introduce {\em Context-sensitive Conditional Expression Reduction Systems
  (CERS)\/} by extending and generalizing the notion of conditional TRS
  to the higher order case.

  We justify our framework in two ways. First, we define {\em orthogonality\/}
  for CERSs and show that the usual results for orthogonal systems
  (finiteness of developments, confluence, permutation equivalence) carry
  over immediately. This can be used e.g.\ to infer confluence from the
  subject reduction property in several typed $\lambda$-calculi
  possibly enriched with pattern-matching definitions.

  Second, we express several proof and transition systems
  as CERSs. In particular, we give encodings of Hilbert-style proof systems,
  Gentzen-style sequent-calculi, rewrite systems with rule priorities, and
  the $\pi$-calculus into CERSs. This last encoding is an (important) example
  of real context-sensitive rewriting.
\end{abstract}
\end{frontmatter}
}
\elsevsupp{%Vincent: obsolete, already done by Elsevier, see above:
  %\begin{titlepage}
  %\thispagestyle{empty} 

  %\date{}
  \title{Context-sensitive Conditional Expression Reduction Systems}
  \author{Zurab Khasidashvili \\
  School of Information Systems \\
  University of East Anglia\\
  Norwich NR4 7TJ England \\ 
   zurab@sys.uea.ac.uk\thanks{Supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300} 
  \and Vincent van Oostrom \\
  Department of Mathematics and Computer Science\\
  \suppress{Free University}
  Vrije Universiteit\\
  De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands\\
  oostrom@cs.vu.nl}
  
  \date{}
  \maketitle
  \begin{abstract}
  We introduce {\em Context-sensitive Conditional Expression Reduction Systems
  (CERS)\/} by extending and generalizing the notion of conditional TRS
  to the higher order case.

  We justify our framework in two ways. First, we define {\em orthogonality\/}
  for CERSs and show that the usual results for orthogonal systems
  (finiteness of developments, confluence, permutation equivalence) carry
  over immediately. This can be used e.g.\ to infer confluence from the
  subject reduction property in several typed $\lambda$-calculi
  possibly enriched with pattern-matching definitions.

  Second, we express several proof and transition systems
  as CERSs. In particular, we give encodings of Hilbert-style proof systems,
  Gentzen-style sequent-calculi, rewrite systems with rule priorities, and
  the $\pi$-calculus into CERSs. This last encoding is an (important) example
  of real context-sensitive rewriting.
  \end{abstract}
}

\section{Introduction}

A term rewriting system is a pair consisting of an alphabet and a set
of rewrite rules. The alphabet is used {\em freely\/} to generate the terms 
and the rewrite rules can be applied in any {\em surroundings\/}, generating
the rewrite relation. In the first order case (no variable binding)
one speaks of TRSs while in the higher order case (with variable binding)
there exist several conceptually similar, but notationaly often quite different
proposals. Long ago, the first general higher order format was introduced by
Klop~\cite{[Kl.CRS]} under the name of {\em Combinatory Reduction Systems\/}.
Since then, several other interesting formalisms have been 
introduced~\cite{[OCRS],[Nip.b],[Wol],[OR94],[Tak93]}.
This paper is based on the notion of {\em Expression Reduction System\/}
introduced by the first author~\cite{[OCRS]}, but our results also apply 
to the other higher order formats.

Often it is of interest to have the possibility to put restrictions on 
the generation of either the terms or the rewrite relation (or both).
For example, many typed lambda calculi can be viewed as untyped 
lambda calculus with restricted {\em term\/} formation.
Let's call them {\em sub\/}-ERSs (cf.\ \cite[Def.\ 12.9]{[kor]})
On the other hand, many rewrite strategies are naturally expressed by
restricting application of the {\em rewrite rules\/}.
For example, the call-by-value strategy in $\lambda$-calculus can be specified
by restricting the second {\em argument\/} of the $\beta$-rule to values.
In general, restricting arguments gives rise 
to so-called {\em conditional\/} ERSs (cf.\ \cite{[B.K.]}).
The leftmost-outermost strategy can be specified by restricting the
{\em context\/} in which the $\beta$-rule may be applied.
We will call the latter kind of rules in which contexts are restricted
{\em context-sensitive\/}.\footnote{
  The distinction between `conditional' and `context-sensitive' is more
  a historical than a conceptual one.} In Section~\ref{cers} we introduce {\em CERSs\/} 
  (conditional context-sensitive ERSs) which allow all
  three kinds of restriction.
\suppress{
  We allow all three kinds of restrictions and call such restricted
  ERSs, {\em CERSs\/} (short for: conditional context-sensitive ERSs).}

  In Section~\ref{ocers} we present a suitable notion of 
  orthogonality and prove the standard 
  results for orthogonal CERSs (OCERSs) like 
  the Finite Developments Theorem, confluence etc.\ 
  by adapting a method for unconditional higher order
  rewriting \cite{[Kl.CRS],[OCRS]}.

  In Section~\ref{coding} we show how some transition and 
  proof systems can be expressed in a natural way in CERSs.
  A very similar idea is present in the work of Meseguer~\cite{[Mes]}
  who encodes many systems in his
  Conditional Rewriting Logic~\cite{[Mes]}.
  Nevertheless, our encoding of calculi with bound variables
  seems to be more natural, since we don't need
  to `code the bindings away' into a first order framework.

\suppress{
The paper is structured as follows.
In Section~\ref{cers} we present our objects of study: CERSs.
Section~\ref{ocers} contains the definition of and 
main results for orthogonal CERSs, elucidated by some examples.
Some systems of interest are expressed as CERSs in
Section~\ref{coding}.}



\section{Conditional Expression Reduction Systems}  \label{cers}

We present CERSs in the style of ERSs \cite{[OCRS]}.
Terms are formed as usual from the
alphabet as in the first order case, but for symbols having
binding power (like $\lambda$ in $\lambda$-calculus or $\int$ in integrals)
which require some binding variables and terms as arguments 
(as specified by their arity). Scope indicators are used to specify
which variables have binding power in which arguments.
Note that one cannot substitute for binding variables.
The variables for which one can substitute are
called metavariables (like in Klop's CRSs).
\suppress{would contradict definition: Metavariables can be instantiated to contexts.}

\begin{defn} \label{D.1.}
  Let $\Sigma$ be an {\em alphabet} comprising 
  {\em variables\/}, denoted by $x$, $y$, $z$ and
  {\em symbols\/} ({\em signs\/}).
  A symbol $\sigma$ can be either a {\em function symbol\/}
  ({\em simple operator\/}) having an {\em arity\/} $n \in \Nset$,
  or an {\em operator sign\/} ({\em quantifier sign\/}) having
  {\em arity\/} $(m,n) \in \Nset \times \Nset$.
  In the latter case $\sigma$ needs to be supplied with $m$ 
  {\em binding\/} variables $x_1$,\ldots,$x_m$ to form the
  {\em quantifier\/} ({\em compound operator\/})
  $\sigma x_1\ldots x_m$.
  If $\sigma$ is an operator sign it also has a {\em scope indicator\/}
  which is a vector of length $m$ specifying for each
  variable in which of the $n$ arguments it has binding power.
  {\em Terms\/} $t$, $s$, $e$, $o$ are constructed from variables, 
  function symbols and quantifiers in the usual first order way
  respecting (the second component of the) arities.
  A predicate $AT$ on terms specifies which terms are {\em admissible\/}.
  
  {\em Metaterms\/} are constructed like terms, but also allowing as basic
  constructions {\em metavariables\/} $A$, $B$, \ldots
  and {\em metasubstitutions\/} $(t_1/x_1,\ldots,t_n/x_n)t_0$, 
  where each $t_i$ is an arbitrary metaterm and the $x_i$ have binding
  effect in $t_0$. An {\em assignment\/} 
  ({\em substitution\/}) $\theta$ maps each
  metavariable to some term. The application of the
  substitution $\theta$ to a term $t$ is written $t\theta$ and is
  obtained from $t$ by replacing metavariables with 
  their values under $\theta$,
  and by replacing metasubstitutions $(t_1/x_1,\ldots,t_n/x_n)t_0$,
  in right to left order, with the result of substitution of terms
  $t_1$,\ldots,$t_n$ for free occurrences of $x_1$,\ldots,$x_n$ in $t_0$
  (cf.\ Kahrs' notion of substitute \cite{[kor]}).
\end{defn}

\suppress{
\begin{defn}
\label{D.1.}
 Let $\Sigma$ be an {\em alphabet}, comprising {\em variables}, denoted by 
$x,y,z$; {\em function symbols}, also called {\em simple operators};
and {\em operator signs\/} or {\em quantifier signs}.  Each function symbol
has an {\em arity\/} $k\in N$, and each operator sign $\sigma$ has an {\em arity\/} $(m,n)$ with $m,n\neq 0$ such that, for any sequence $x_{1},\ldots ,x_{m}$ of pairwise distinct variables, $\sigma x_{1}\ldots x_{m}$ is a {\em compound operator\/} or a {\em quantifier\/} with {\em arity\/} $n$. Occurrences of $x_{1},\ldots,x_{m}$ in $\sigma x_{1}\ldots x_{m}$ are called {\em binding
variables}.  Each quantifier $\sigma x_{1}\ldots x_{m}$, as well as the
corresponding quantifier sign $\sigma$ and binding variables
$x_{1}\ldots x_{m}$, has a {\em scope indicator\/} $(k_{1},\ldots ,k_{l})$ to
specify the arguments in which $\sigma x_{1}\ldots x_{m}$ binds all free
occurrences of $x_{1},\ldots ,x_{m}$. {\em Terms\/} are constructed from
variables using functions and quantifiers in the usual way. Further, we assume that each $n$-ary operator symbol comes together with $n$ sets of {\em admissible} terms that are allowed in corresponding arguments of the symbol when {\em admissible terms} are constructed.  We use $t,s,e,o$ to denote (admissible) terms. 

{\em Metaterms\/} are constructed similarly from {\em terms\/}  and {\em
metavariables\/} $A, B,\ldots$, which range over terms. In addition, {\em
metasubstitutions}, expressions of the form $(t_1/x_1,\ldots,t_n/x_n)t_0$,
with $t_j$ arbitrary metaterms, are allowed, where the {\em scope\/} of
each $x_i$ is $t_0$. Metaterms without metasubstitutions are {\em simple metaterms}. An {\em assignment\/} maps each metavariable to a term over $\Sigma$. If $t$ is a metaterm and $\theta$ is an assignment, then the $\theta$-{\em instance\/} $t\theta$ of $t$ is the term obtained from $t$ by replacing metavariables with their values under $\theta$, and by replacing metasubstitutions ($t_{1}/x_{1},\ldots ,t_{n}/x_{n})t_0$, in right to left order, with the result of substitution of terms $t_{1},\ldots ,t_{n}$
for free occurrences of $x_{1},\ldots,x_{n}$ in~$t_0$.
\end{defn}
}

For example, a $\beta$-redex in the $\lambda$-calculus appears as
$Ap(\lambda x\;t,s)$, where $Ap$ is a function symbol of arity $2$, and
$\lambda$ is an operator sign of arity $(1,1)$ and scope indicator $(1)$.
Integrals such as $\int_{s}^{t}f(x)\,dx$ can be represented as $\mathord{\int}
x(s,t,f(x))$ using an operator sign $\int$ of arity $(1,3)$ and scope
indicator $(3)$.
The predicate $AT$ can be used to express sorting and typing constraints.
 
\suppress{
Sets of admissible terms allowed for arguments of an operator can be considered as terms of certain sorts or types, thereby allowing to express sort and type disciplines in term construction. Hence function symbols can play role of, e.g., predicate symbols, etc. When useful, we can assume that our alphabet contains function variables as well, but we disallow their binding.  
 }

The specification of a CERS consists of a (restricted) alphabet as
specified above and a set of (restricted) rules as specified below.

\begin{defn} \label{D.3.}
  A rewrite rule is a (named) pair of metaterms $r : t \ar s$,
  such that $t$ and $s$ do not contain free variables.
\delete{
subject to the following
  constraints:
  \begin{enumerate}
  \item $t$ and $s$ do not contain free variables, and
  \item each metavariable occurring in $s$ also occurs in $t$.
  \end{enumerate}
}
  We close the rules under assignments:
  $r\theta : t\theta \ar s\theta$ if $r : t \ar s$ and $\theta$ is a
  substitution. For reasons of hygiene this is restricted to assignments 
  $\theta$ such that each free variable occurring in a term $A\theta$
  assigned to a metavariable $A$ is either bound in 
  the $\theta$-instance of each occurrence of $A$
  in the rule or in none of them.  
  The term $t\theta$ is then called a {\em redex\/} and $s\theta$ its {\em contractum\/}.
  Next, we close under contexts
  $C[r\theta] : C[t\theta] \ar C[s\theta]$, if
  $r\theta : t\theta \ar s\theta$ and $C[\,]$ is a context
  (a term with one hole).

  The rewrite relation thus obtained is the usual (unconditional, context-free)
  ERS-rewrite relation. If restrictions are put on assignments,
  via a predicate $AA$ on rules and substitutions, the rewrite relation will
  be called {\em conditional\/}. If restrictions are put on contexts,
  via a predicate $AC$ on rules, substitutions and contexts, 
  the rewrite relation will be called {\em context-sensitive\/}.

  A {\em CERS\/} is a pair consisting of an alphabet and a
  set of rewrite rules, both possibly restricted.
\end{defn}

In the sequel when we speak about terms and redexes, we will always
mean admissible terms and admissible redexes, respectively.

\suppress{
\begin{defn}
\label{D.3.}  
A {\em Conditional (Context-sensitive) Expression Reduction System}  is a pair $(\Sigma,R)$, where $\Sigma$ is an {\em alphabet}, described in Definition~\ref{D.1.}, and $R$ is a (finite or infinite)  set of {\em rewrite rules} $r:t \ar s$, where $t$ and $s$ are closed metaterms (i.e., no free variables) such that $t$ is not a metavariable, and each metavariable that occurs in $s$ occurs also in~$t$. 
 
Each  rule $r$ has a set of {\em admissible assignments\/}
$AA(r)$ such that $t\theta$ and $s\theta$ are admissible terms and
which, in order to prevent undesirable confusion of variable
bindings, must satisfy the condition that: 

(a) for any  assignment  $\theta \in AA(r)$, any metavariable $A$ occurring
in $t$ or $s$, and any variable $x\in FV(A\theta)$, either every occurrence
of $A$ in $r$ is in the scope of some binding occurrence of $x$ in $r$, or
no occurrence is.

For any  rule $r:t \ar s$ in $R$  and $\theta \in AA(r)$, $t\theta$ is an $r$-{\em redex} or an $R$-{\em redex}, and $s\theta$ is the {\em contractum} of $t\theta$. We call two $R$-redexes $u$ and $v$ {\em weakly similar} if they are instances of the same rule (i.e., with the same set of admissible assignments).

Further, each pair $(r,\theta)$ with $r\in R$ and $\theta\in AA(r)$ has a set $AC(r,\theta)$ of {\em admissible contexts} such that, if a context $C[\,\,]$ is admissible for $(r,\theta)$ and $o$ is the contractum of $u=r\theta$ according to $r$, then  $C[u]\ar C[o]$ is an $R$-reduction step. In this case, $u$ is {\em admissible} for $r$ in the term $C[u]$. We require that the set of admissible terms be closed under reduction. We also require that admissibility of terms, assignments, and contexts be closed under renaming of bound variables.

We call a CERS {\em context-free} if every context
is admissible. An {\em (unconditional) Expression Reduction System} (ERS) is a CERS where all terms are admissible; an assignment $\theta$ is {\em admissible} for a rule $r:t\ar s$ iff the condition (a) is satisfied;  and all contexts are admissible for all redexes.
\end{defn}}

Our syntax is very close to the syntax of the $\lambda$-calculus and of First Order Logic. For example, the $\beta$-rule is written as $Ap(\lambda xA,B)\ar
(B/x)A,$ where $A$ and $B$ can be instantiated by any terms.
The $\eta$-rule is written as $\lambda xAp(A,x)\ar A$, where
it is required that $x \not\in A\theta$ for an assignment $\theta$, 
otherwise an $x$ occurring in $A\theta$ and therefore bound in $\lambda x(A\theta x)$ would become free. 
A rule like $f(A)\ar\exists x(A)$ is also allowed,
but in that case the assignment $\theta$ with $x\in A\theta$ is not. 
The recursor rule is written as $\mu(\lambda x A)\ar (\mu(\lambda x A)/x)A$.
 Note that we allow meta\-va\-ri\-able-rules like 
  $\eta^{-1}: A \ar \lambda xAp(Ax)$ and 
  meta\-va\-ri\-able-introduction-rules like 
  $f(A) \ar g(A,B)$, which are usually excluded a priori.
This is only useful when the system is conditional.

\suppress{
$\,\,\,\,\,\,\,\,\,\,\,\,S^{n+1}x_1\ldots x_nA_1\ldots
A_nA_0\ar(A_1/x_1,\ldots ,A_n/x_n) A_0,\,\,\,n=1,2,\ldots$,\\
where $S^{n+1}$ is an {\em operator sign of substitution\/} with
arity $(n,n+1)$ and scope indicator $(n+1)$, and $x_{1},\ldots ,x_{n}$ and
$A_{1},\ldots,A_{n}, A_0$ are pairwise distinct variables and metavariables.
Each assignment is admissible for any rule in $S$. 
Hence a CERS $R$ can be split into $R_{fS}=_{def}R_{f}\cup S$, 
where  $R_f$ is obtained from $R$ by adding symbols $S^{n+1}$ in the alphabet and by replacing in the right-hand sides of the rules all metasubstitutions of the form $(t_{1}/x_{1},\ldots ,t_{n}/x_{n})t_0$ by $S^{n+1} x_{1}\ldots x_{n}t_{1}\ldots t_{n}t_0$, respectively. After defining the induced admissibility relations for $R_{fS}$, we can associate to any $R$-reduction an $R_{fS}$-reduction. And   similarly to the case off ERSs~\cite{[OCRS]}, we can define the {\em descendant\/} relation on subterms allowing to trace all subterms, including contracted redexes, along reductions in any CERS $R$.
}

\delete{
For any ERS $R=\{r_i:t_i\ar s_i\,\vert\,i\in I\}$, $R_f=\{r_i':t_i\ar s'_i\,\vert\,i\in I\}$ is the CERS obtained from $R$ by adding symbols
$S^{n+1}$ in the alphabet and by replacing in right-hand sides $s_i$ of the rules all metasubstitutions of the form $(t_{1}/a_{1},\ldots ,t_{n}/a_{n})t$ by $S^{n+1} a_{1}\ldots a_{n}t_{1}\ldots t_{n}t$, respectively; If $R$ is simple, then $R_{fS}=_{def}R_{f}=_{def}R$. Otherwise $R_{fS}=_{def}R_{f}\cup
S$, where $S$-rules are obtained from $S$-rules by
underlining the $S$-symbols. All assignments and contexts are admissible for $S$-rules. An assignment $\theta$ is admissible for an $R_f$-rule $r'_i$ iff the assignment $\theta_{S}$, that to each term metavariable $A$ assigns the $S$-normal form of $A\theta$ and that coincides with $\theta$ on object metavariables, is admissible for the corresponding rule $r_i\in R$. A context $C[\,\,]$ is admissible for $(r'_{i},\theta)$ in $R_f$ iff it is admissible for $(r,\theta_{S})$ in $R$. $\underline{R}=\{\underline{r}_{i}:\underline{t}_{i} \ar s_{i} \vert i\in
I\}$, where $\underline{t}_{i}$ is obtained from $t_{i}$ by underlining its
head symbol.  {\em Admissible terms} in $\underline{R}$ are terms of $R$ where (only) head-symbols of redexes may be underlined. For each step $e=C[t_i\theta]\stackrel{u}{\ar} C[s_i\theta]=o$ in $R$ there is a reduction $P:e=C[t_i\theta]\ar C[s'_i\theta]\doar C[s\theta]=o$ in~$R_{fS}$,
where $C[s'\theta]\doar C[s\theta]$ is the rightmost innermost normalizing
$S$-reduction.  We call $P$ the {\em refinement} of $u$.  The notion of {\em refinement} generalizes to $R$-reductions with $0$ or more steps.


Let $t\stackrel{u}{\ar} s$ be an $R_f$-reduction step and let $e$ be the contractum of $u$ in $s$.  For each argument $o$ of $u$ there are $0$ or more arguments of $e$. We call them ($u$-){\em descendants} of $o$. Correspondingly, subterms of $o$ have $0$ or more {\em descendants}.  The {\em descendant} of each pattern-subterm (i.e., a subterm rooted at the pattern) of $u$ is $e$. It is clear what is to be meant by {\em descendants} of a subterm that is not in $u$. In an $S$-reduction step $C[S^{n+1}x_1\ldots x_n\,t_1\ldots t_nt_0]\red{u}C[(t_1/x_1,\ldots,t_n/x_n)t_0]$, the argument $t_i$ and subterms in $t_i$ have the same number of {\em descendants} as the number of free occurrences of $x_i$ in $t_0$. All subterms of $t_0$, including free occurrences of $x_1,\ldots,x_n$, have exactly one {\em descendant}. The {\em descendant}  of the contracted redex $u$ itself is its contractum. The notion of {\em descendant} extends by transitivity  to arbitrary $R_{fS}$-reductions. If $P$ is an $R$-reduction, then $P$-{\em descendants} are defined to be the descendants under the refinement of $P$. The {\em ancestor} relation is converse to that of descendant. We call the co-initial reductions $P:t\doar s$ and $Q:t\doar e$ {\em strictly equivalent} (written $P\steq Q$) if $s=e$ and $P$-descendants and
$Q$-descendants of any subterm of $t$ are the same in~$s$ and~$e$; $P$ and $Q$ are {\em equivalent} (written $P\equi Q$) if $s=e$.
}




\section{Orthogonal CERSs}
\label{ocers}

\suppress{\section{Confluence for Orthogonal Conditional ERSs}}

 We define orthogonal CERSs (OCERSs) and sketch our proof of Finite Developments
for them, implying confluence.
 The FD proof is based on Nederpelt \& Klop's method~\cite{[7],[Kl.CRS]} 
for reducing strong normalization to weak normalization. 
It is similar in structure to, but simpler than Klop's original confluence
proof for orthogonal CRSs~\cite{[Kl.CRS]} and we think not more difficult than
other existing confluence proofs~\cite{[vR.rta],[Nip.b],[OR94],[Mel]}.

The idea of orthogonality is that contraction of a redex does not destroy 
others (in whatever way), but rather leaves a number of their residuals. 
A prerequisite for the definition of residual is the
notion of {\em descendant\/} allowing to trace subterms
during a reduction. Whereas this is simple in the first order
case, ERSs may exhibit very complex behaviour due to the possibility
of nested metasubstitutions thereby complicating the definition of descendants.
Fortunately each rewrite step can be decomposed into two parts:
a {\em TRS\/}-part replacing the left-hand side by the right-hand side, but without 
evaluating the metasubstitutions, and a {\em substitution\/}-part 
evaluating the metasubstitutions.
This point of view is profitable\footnote{It even seems to be 
prerequisite for syntactical studies of higher order rewriting. }
since the descendant relation of a rewrite step can now be obtained by
composing the descendant relation of the TRS-step, which is trivial, 
and the descendant relations of the evaluation steps, 
which are a kind of $\beta$-steps (see~\cite{[OCRS]}).

\begin{defn}
\label{D.relaxed.orth.}
To an CERS $(\Sigma,R)$ we associate its {\em refined\/} version 
$(\Sigma_{fS},R_{fS})$, where $\Sigma_{fS}$ is obtained from $\Sigma$ 
by adding fresh symbols $S^{n+1}$ and $R_{fS}$ is 
obtained from $R$ by the following procedure
\begin{enumerate}
\item
  Replace each $R$-rule $r : t \ar s$ by the
  rule $r_f : t \ar s_f$, 
  where $s_f$ is $s$ with each `implicit'
  metasubstitution replaced by its `explicit' pendant $S$.
\item
  Add rules for $S^{n+1}$ (cf.\ polyadic $\lambda$-calculus \cite[p.\ 115]{[Klo90]})
  \[ S^{n+1}x_1\ldots x_n A_1\ldots A_n A \ar (A_1/x_1,\ldots,A_n/x_n)A \]
\end{enumerate}
Obviously, an $r$-step can be simulated by an $r_f$-step followed by
a number of $S$-steps. Via the corresponding
descendant relations of these steps, 
this induces a (unique) descendant relation for $r$.
Two (admissible) redexes with respect to the same rule are called {\em weakly similar\/}.
A descendant of a redex $u$ which is a redex weakly similar to $u$
is called a $u$-{\em residual\/}.

We call a CERS {\em orthogonal\/} (OCERS) if:
\begin{enumerate}
\item
  the left-hand side of a rule is not a single metavariable,
\item
   the left-hand side of a rule does not contain
  metasubstitutions and its metavariables contain
  those of the right-hand side,
\item
  in no term redex-patterns can overlap,
\item \label{stable}
  all the descendants of a redex $u$ in a term $t$ 
  under the contraction of any other redex $v \subt t$ are 
  residuals of $u$.
\end{enumerate} 
\end{defn}

 The second condition ensures that rules exhibit
deterministic behaviour when they can be applied.
The last condition can be thought of as imposing some
closure conditions on arguments and contexts of rules.
For example, consider the rules $a \ar b$ and $f(A) \ar A$ 
with admissible assignment $\theta A = a$. 
The descendant $f(b)$ of the redex $f(a)$ 
after contraction of $a$ is not a redex since the 
assignment $\theta A = b$ is not admissible, 
hence the system is not orthogonal
(it should not be, since it is not confluent).
Note that unconditional non-left-linear rules (almost) 
never satisfy~(\ref{stable}).


\suppress{
Now we define orthogonal CERSs (OCERSs) and sketch our confluence proof for them. Our proof is based on  Nederpelt-Klop's method~\cite{[7],[Kl.CRS]} of reducing strong normalization proofs to weak normalization proofs. The trick is to use the method for proving termination of developments (FD), and all what remains is to check for permutation of TRS-steps and substitution steps. Our proof is considerably simpler than Klop's~\cite{[Kl.CRS]} original confluence proof for orthogonal CRSs which also establishes first FD and deduces confluence from it, and not more difficult than recent confluence proofs~\cite{[vR.rta],[Nip.b],[OR94]}, which use Tait\&Martin-L\"of's method.  

\begin{defn}
\label{D.relaxed.orth.}
We call a CERS {\em orthogonal\/} (OCERS) if: (a) in no admissible term admissible redex-patterns can overlap; (b) all the descendants of an admissible redex $u$ in an admissible term $t$ under the contraction of any other admissible redex $v\subt t$ are again admissible redexes in the obtained term and are weakly similar to $u$; these redexes are {\em $v$-residuals\/} of $u$; and (c) no new metavariables are introduced in right-hand sides of rules. (Note that it follows from (b) that the familiar left-linearity condition is not needed any longer.)
\end{defn}
}
 
A {\em development\/} of a set of non-overlapping redexes
is a reduction in which only residuals of redexes in that set
are contracted. A development can be conveniently visualized by 
underlining the head-symbols of the redexes in the set, only 
allowing contraction of underlined redexes.
We will denote the corresponding underlined 
rewrite system by $\underline{R}$.

\begin{thm} \label{T.FD.}
  All developments in an OCERSs $R$ are finite (FD),
  that is, $\underline{R}$ is strongly normalizing.
\end{thm}


Because space is limited we will contend ourselves with presenting
the main ideas of the proof, which follows closely
the proof of FD for orthogonal ERSs as presented in \cite{[OCRS]}. 
The full proof can be found in the report version \cite{[KO95]}.


\suppress{
Actually this finiteness result can be directly obtained from
the same result for ERSs, since an OCERS development
is an ERS development. For this reason, we will not repeat the 
complete proof of FD as presented in \cite{[OCRS]} here but since
we think the proof-technique is interesting on its own, we will
try to present its main ideas.}

$\underline{R}$ can be refined into $\underline{R}_{fS}$ and 
surely strong normalisation of the latter implies strong
normalisation of the former. 
\suppress{
  $\underline{r}_{fS}$-steps and $S$-steps
  easily seen to be terminating on their own, 
  The former, because they
  don't do anything except for replacing the lefthand-side
  by the righthand-side of the rule possibly duplicating the
  subterms corresponding to the metavariables.
  The latter are terminating, since they correspond to developments of 
  $\beta$-steps which are known to be finite.
  We conclude that only their combination might destroy
  strong normalization of $\underline{R}_{fS}$.
}
To prove strong normalisation of $\underline{R}_{fS}$
the `memory' technique by Nederpelt
and Klop is useful. The idea is to transform the system $\underline{R}_{fS}$
into yet another orthogonal system $\underline{R}_{fS}^{\mu}$ 
where no erasure takes place, by `memorizing' metavariables which might be erased. We use a simplified version of Nederpelt \& Klop's technique, 
as developed in~\cite{[lfcs]}.
For example
  \[ \underline{f}(A,B) \ar f(A) \]
is transformed into
  \[ \underline{f}(A,B) \ar \mu(B,f(A)) \]
where the $B$ is `memorized' since it did not have descendants in $f(A)$.
This $\mu$-transformation is also applied to the $S$-rules.
From the definition we immediately have that every $\underline{R}_{fS}$-reduction
can be lifted to an $\underline{R}_{fS}^{\mu}$-reduction of the same length,
for which the number of $\mu$'s {\em increases\/} in each step.
Note that the presence of the `memory' ($\mu$) cannot prevent creation of redexes,
since there is no creation of redexes possible in $\underline{R}_{fS}$.
Moreover, $\underline{R}_{fS}^{\mu}$ is {\em weakly normalizing\/} as can be seen
by considering the rightmost-innermost strategy. To conclude strong normalization of $\underline{R}_{fS}^{\mu}$, 
we can apply the following lemma from~\cite{[Kl.CRS]}.

\begin{lem}
  A locally confluent, increasing, weakly normalizing abstract
  rewriting system is strongly normalizing (so confluent by
  Newman's Lemma).
\end{lem}

From the conditions on admissibility in the definition
(these conditions are needed for confluence as
 witnessed by the example above)
of orthogonality and finiteness of developments,
one can conclude confluence. 
Actually, most of L{\'e}vy's theory of {\em permutation
equivalence\/} can be reduced to FD, so is
applicable to OCERSs. This is properly addressed
in \cite{[KO95]}.

\begin{thm} \label{T.CCR.}
  Orthogonal CERSs are confluent.
\end{thm}



\suppress{  
The method of our proof is as  follows. Developments in an OERS $R$ can be represented as reductions in the OERS $\underline{R}$ the rules of which are obtained from $R$-rules by underlining their head-symbols. To prove termination of $\underline{R}$-reductions, we  split  $\underline{R}$ into $\underline{R}_{fS}$=$\underline{R}_{f} \cup S$ and define a {\em non-erasing\/} version $\underline{R}_{fS}^{\mu}$  of $\underline{R}_{fS}$. We prove that each term in $\underline{R}_{fS}^{\mu}$ has exactly one normal form (the proof consists of checking that TRS-steps and substitution steps commute).
\delete{
all elementary diagrams in the following diagram commute, which shows that any $\undl{R}_{fS}^{\mu}$-nf of $t_n$ of an admissible term $t_0$ coincides with $t_0\downarrow_{\undl{R}_{fS}^{\mu}}$, where $\underline{\downarrow}_{f}^{\mu}(t)$ (resp. $\downarrow_{S}^{\mu}(t)$) denotes the result of the rightmost innermost normalizing $\underline{R}_{f}^{\mu}$-reduction $S^{\mu}$-reduction starting from $t$,  and
$\underline{\downarrow}_{fS}^{\mu}(t)$ denotes
$\downarrow_{S}^{\mu}(\underline{\downarrow}_{f}^{\mu}(t))$.

\def\uSmu{S^{\mu}}
\def\uRmuf{\underline{R}_{f}^{\mu}}
\def\uRmufS{\underline{R}_{fS}^{\mu}}

  
\begin{diagram}[height=1.6em,width=1.6em]
  t_0  & \rTo^{\uSmu} & t_1 & \rTo^{\uRmuf} & t_2 & \rOnto^{\uRmufS} & t_n \\
 \dOnto^{\uRmuf} &  & \dOnto^{\uRmuf} &  & \dOnto^{\uRmuf} & & \dOnto^{\uRmuf}_{\emptyset} \\
 \underline{\downarrow}_{f}^{\mu}(t_{0}) & \rOnto^{\uSmu} & \underline{\downarrow}_{f}^{\mu}(t_{1}) & \rOnto^{\emptyset} & \underline{\downarrow}_{f}^{\mu}(t_{2}) & \rOnto^{\uSmu} & \underline{\downarrow}_{f}^{\mu}(t_{n}) \\
 \dOnto^{\uSmu}  &  & \dOnto^{\uSmu}  &  & \dOnto^{\uSmu} & & \dOnto^{\uSmu}_{\emptyset} \\
 \underline{\downarrow}_{fS}^{\mu}(t_{0})  & \rOnto^{\emptyset} & \underline{\downarrow}_{fS}^{\mu}(t_{1}) & \rOnto^{\emptyset} & \underline{\downarrow}_{fS}^{\mu}(t_{3}) & \rOnto^{\emptyset} & \underline{\downarrow}_{fS}^{\mu}(t_{n}) \\
\end{diagram} 
}
This implies that  $\underline{R}_{fS}^{\mu}$ is strongly normalizing. Since to each $\underline{R}_{fS}$-reduction we can associate an $\underline{R}_{fS}^{\mu}$-reduction of the same length, $\underline{R}_{fS}$ is also strongly normalizing.  As a corollary,  we have FD for OERSs. But developments in OCERSs can be simulated by developments in OERSs since residuals of admissible redexes in OCERSs are admissible redexes weakly similar to their ancestors, by orthogonality. Hence FD is valid for OCERSs too, and confluence follows. (In fact, FD implies the strong confluence.)

\begin{thm} \label{T.CCR.}
  Orthogonal conditional context-sensitive ERSs are confluent.
\end{thm}
}

 Untyped lambda calculus \cite{[Bar]} is the prime example
of an (unconditional) orthogonal higher-order term rewriting system.
If one restricts term formation in it, one arrives
at the large class of typed lambda calculi. Since the rewrite
relation in these calculi is not restricted in any way, and
typed terms are closed under $\beta$-reduction\footnote{
This so-called {\em Subject Reduction\/} property is sometimes non-trivial to prove.}
these sub-ERSs are orthogonal, hence confluent.

An interesting example of a CERS was recently
studied in \cite{[A.F.]}. Terms are ordinary $\lambda$-terms 
possibly containing {\sf let} expressions,
but the rewrite rules have conditions on them as follows.
Define the syntactic categories by the following grammar
\def\lamneed{\mbox{$\bflambda_{need}$}}
\def\letin#1#2{{\mbox{\sf{let\ }}#1 = #2\mbox{\sf{\ in\ }}}}
\def\backor{\,\mathrel{|}\,}
\def\rewll{\to_{\ell}}
\def\rewst{\to_{s}}
  \begin{eqnarray*}
    M & ::= & x \backor
              MM \backor
              \lambda x.M \backor
              \letin{x}{M}{M} \\
    V & ::= & \lambda x.M \\
    A & ::= & V \backor 
              \letin{x}{M}{A} \\
    E & ::= & [\;] \backor 
              EM \backor 
              \letin{x}{M}{E} \backor
              \letin{x}{E}{E[x]}
  \end{eqnarray*}
  The rules are
  \begin{eqnarray*}
    (\lambda x.M)M'                    & \to & \letin{x}{M'}{M}                 \\
    \letin{x}{V}{E[x]}                 & \to & \letin{x}{V}{E[V]}               \\
    (\letin{x}{M}{A})M'                & \to & \letin{x}{M}{AM'}                \\
    \letin{x}{(\letin{y}{M}{A})}{E[x]} & \to & \letin{y}{M}{\letin{x}{A}{E[x]}}
  \end{eqnarray*}
  the rewrite relation $\rewst$ is obtained from this by 
  allowing arbitrary contexts.
  By some case analysis, one shows that each of
  the syntactic categories is closed under $\rewst$ 
  and that there are no overlaps between rules, so
  the system is an orthogonal conditional ERS.
  Even stronger, the system is leftnormal in the
  sense of \cite{[Kl.CRS]}, hence standard reductions
  are normalizing.

 
  An emerging class of context-sensitive and conditional ERSs is the class
  of $\lambda$-calculi with restricted expansion rules like $\bar{\eta}$
  (see e.g.\ \cite{[Aka]}).
  These calculi are not quite orthogonal, nevertheless their
  confluence can be shown by tampering with the confluence 
  diagrams arising from FD for the corresponding 
  unconditional expansion rules.

\suppress{
  Interesting context-sensitive and conditional $\lambda$-calculi
  are the ones having expansion rules, for example as studied
  in~\cite{[Aka]}. These systems seem quite difficult to study,
  since they are non-orthogonal and most standard techniques fail for them.
}

\section{Expressive power of CERSs} \label{coding}

In~\cite{[Mes]}, Meseguer gives encodings of labeled transition systems, 
several functional programming languages, Chomsky grammars, 
and some concurrent languages (e.g.\ Chemical Abstract Machine and  CCS), 
into CTRSs. In this section, we give encodings of some other proof and 
computation systems, to show that CERSs are even more expressive 
programming languages. This is not always very useful to 
understand the original systems better (e.g, one doesn't gain any 
insight from encoded versions of Hilbert and Gentzen style proof systems), 
but it often helps to understand operational behaviour of a system 
(e.g., in the case of the $\pi$-calculus).



\subsection{Conditional TRSs}



   Conditional term rewriting systems (CTRSs) were introduced by 
  Bergstra \& Klop in~\cite{[B.K.]}.
  Their conditional rules have the form
  $t_1 = s_1 \wedge \cdots \wedge t_n = s_n \,\Rightarrow\, t \ar s$,
  where the $s_i$ and $t_i$ may contain variables in $t$ and $s$.
  According to such a rule $t\theta$ can be rewritten to $s\theta$ if all the equations 
  $s_i\theta = t_i\theta$ are satisfied. 
  CTRSs were classified depending on how satisfaction is
  defined (`$=$' can be interpreted as $\doar$, $\leftrightarrow^\ast$, etc.)
  As they remark this can be generalized by allowing for arbitrary predicates
  on the variables as conditions (cf.\ also \cite{[DJS88],[Toy88]}).

  Clearly, all these CTRSs are context-free CERSs since they only allow conditions 
  on the arguments not on the context of rewrite rules.
  For this reason sometimes results for them are a special case
  of general results which hold for all CERSs.
  In particular, {\em stable\/} 
  CTRSs for which the unconditional version
  is orthogonal as defined in~\cite{[B.K.]} 
  are orthogonal in our sense, so confluent.
  Several confluence results were obtained in the above papers for
  non-orthogonal CTRSs as well, which perhaps can also be generalized to the 
  higher-order case.


\suppress{
  In Bergstra-Klop~\cite{[B.K.]} a notion of conditional TRSs, 
  let us call it CTRS*s, is introduced. Rules in CTRS*s have the form: 
  $t\ar s\,\,\Leftarrow\,\,P_1(\overline{t_1}),\ldots,P_n(\overline{t_n})$,
  where $P_i$ are arbitrary predicates and $\overline{t_i}$ are 
  lists of terms of corresponding lengths. An instance $t\theta$ of $t$ 
  is a redex iff $\theta(\overline{t_i})$ satisfy $P_i$; 
  and $t\theta$ can be rewritten into $s\theta$ in any context, 
  i.e., CTRS*s are context-free.

  In Dershowitz\&Okada\&Sivakumar~\cite{[DJS88]} a classification of 
  CTRS*s is introduced, which is a generalization of the one introduced 
  in~\cite{[B.K.]}. In particular, {\em semi-equational, join, normal,} 
  and {\em generalized} CTRS*s are defined. Our CERSs cover all these systems.
  Further, {\em closed orthogonal\/} CTRS*s as defined 
  in~\cite{[B.K.],[Kl.CRS]} are orthogonal; therefore our confluence result 
  covers some confluence results from~\cite{[B.K.]} for orthogonal CTRS*s. 
  Several confluence results are obtained in the above papers for 
  non-orthogonal CTRS*s as well, which perhaps can also be generalized 
  to the higher-order case.
}

\delete{
  The only confluence result in context-sensitive CERS we are aware of is 
  in Akama~\cite{[Aka]}. It establishes confluence for reductions, 
  that involves expansion steps as well. These reductions cannot be considered 
  as reductions in CERSs (because of the expansion steps).
}

\subsection{Encoding of strategies}

   In the literature (\cite{[Bar]}) a strategy for a
  rewriting system $(R,\Sigma)$ is a map 
  $F \colon Ter(\Sigma) \to Ter(\Sigma)$, such that 
  $t \ar F(t)$ if $t$ is not a normal form, and
  $t = F(t)$ otherwise.
  Such strategies are deterministic and only specify
  what to do, not how to do it.
  We prefer to view a strategy as a set $F$ of triples
  $(r,\theta,C[\;])$ specifying that rule $r:t \ar s \in R$ can be
  used with assignment $\theta$ in context $C[\;]$
  to rewrite $C[t\theta]$ to $C[s\theta]$.\footnote{
    Note that an ordinary strategy $F$ can be directly encoded by associating the set 
    $\{ (r:t \ar s,\theta,C[\;]) \mathrel{|} 
        r \in R, C[s\theta] = F(C[t\theta])\}$ to it.
  }
  To a strategy $F$ one can associate a CERS $R_F$ encoding exactly
  the same information, by taking $\theta, C[\;]$ admissible
  for $r$ iff $(r,\theta,C[\;]) \in F$.
  Obviously, this also holds the other way around, that is, 
  every CERS can be viewed as a strategy for its unconditional version.


\suppress{
  In the literature a strategy is a map $F\colon Ter(\Sigma) \to Ter(\Sigma)$ such
  that $t \ar F(t)$ if $t$ is not a normal form, and $t = F(t)$ otherwise. 
  For our purposes this definition is not satisfactory. 
  A strategy in our sense is a set $F$ of quadruples  
  of the form $(t,r,\theta,C[\;])$, where $r$ is a rule,
  $\theta$ is an admissible substitution for $r$,  
  $C[\;]$ is an admissible context for $(r,\theta)$, such that $t = C[LHS(r)\theta]$.  

  Given an ERS $R$ and a strategy $F$ for it, we can construct
  a CERS $R_F$ where exactly the $R$-reductions performed according
  to the strategy $F$ are possible.  We take the signature of $R$ 
  for the signature of $R_F$; we take the rules of $R$ for $R_F$-rules 
  without changing the sets of admissible assignments for them; 
  finally, for each rule $r$ and admissible assignment $\theta$, 
  if and only if $(t,r,\theta,C[\;]) \in F$, we declare $C[\;]$ 
  to be admissible for $(r,\theta)$ in $R_F$. 
  Of course, this encoding is neither the only nor always the best 
  way of encoding a strategy. 
}



\subsection{Encoding of rewrite systems with priorities}

 


  A priority rewrite system, or PRS for short is a pair consisting
  of a TRS $R$ and a partial order $<$ on the set of rules of $R$~\cite{[BBKW89]}.
  The partial order is meant as a judge in case of conflict between rules.
  An $r$-redex $u$ can be contracted iff it is a closed term, 
  and there is no $r'>r$ such that $u$ can be rewritten to an $r'$-redex  
  by means of an internal (i.e.\ taking place below the headsymbol) reduction;
  such redexes ar allowed to be contracted in any context.
  Because of the negative condition in the definition of the rewrite relation,
  PRSs are not always well-defined, but it is clear that those which
  are well-defined can be expressed as a conditional ERS.
  In~\cite{[BBKW89]} some criteria sufficient for well-definedness
  as well as for ground confluence are found.
  In particular, it is shown that 
  {\em essentially regular\/}\footnote{The left-linearity
  condition in~\cite{[BBKW89]} is redundant, since it is implied
  by essential nonambiguity.} RPSs are ground confluent.
  Such PRSs are orthogonal in our sense, so this confluence
  result is covered by ours.
\suppress{
  A TRSs with priorities~\cite{[BBKW89]}, PRSs for short, 
  is a TRS with a well-founded ordering $>$ on rules. 
  An $r$-redex $u\subt t$ is admissible iff there is no 
  $r'$-redex in $t$ with $r'>r$, and $u$ cannot be rewritten 
  to an $r'$-redex without contracting a redex involving the 
  top symbol of $u$. So clearly PRSs are context-sensitive CERSs. 
  Not every ordering can define a sound rewrite relation on ground terms; 
  therefore some sufficient criteria for the relation to be well defined 
  are studied in~\cite{[BBKW89]}. A criterion for ground confluence for 
  PRSs with well defined operational semantics is also found. 
  In particular, it is shown that left-linear and 
  {\em essentially non-ambiguous} RPSs are ground confluent 
  (in fact, essential non-ambiguity is enough). 
  Such PRSs are orthogonal in our sense, and the confluence 
  criterion is covered by our CR theorem for OCERSs. 
}

\subsection{Encoding of Hilbert style proof systems}

  To illustrate the expressive power of CERSs we give
  an encoding of Hilbert style proof systems into CERSs,
  translating deduction into reduction.
  A Hilbert style system $H$ has a number of axioms 
  $F_1,F_2,\ldots$ and two rules: 
  {\em Modus Ponens}, 
  allowing to infer $B$ when $A$ and $A \impl B$ are theorems, and the 
  {\em $\exists$-rule}, 
  allowing to infer $\exists x.A[x]$ if $A[t]$ is a theorem. 
  A proof in the axiomatic theory $H$ is a finite sequence of formulae 
  $G_1,G_2,G_3,\ldots,G_m$  such that $G_i$ is either an axiom 
  (i.e., coincides with one of the $F_j$) or is obtained from 
  $G_1,\ldots,G_{i-1}$ by one of the above two rules.
  To each $H$ we can associate a CERS $R_H$ as follows.
\suppress{
  In order to model proofs in the system $H$, 
  to each proof in $H$ we associate a reduction sequence, 
  in an appropriate CERS $R_H$,
  starting from the term $P^0$ and leading to the term $P^m(G_1,\ldots,G_m)$,
  where $P^n$ is an $n$-ary operator symbol of type 
  $Bool \times \ldots \times Bool \to Nat$.
  $P^n$ encodes a list of $m$ formulae.}
The alphabet of $R_H$ consists of the alphabet of $R$ augmented by
the function symbols $P^n$ of arity $n$, used to model
the current stock of theoremata.
The rules, more precisely the rule-schemata, of $R_H$ are:
\begin{itemize}
\item
  $P^n(A_1,\ldots,A_n) \ar P^{n+1}(A_1,\ldots,A_n,F)$, 
  for each $n$ and axiom $F$. 
  In particular $P^0 \ar P^1(F)$. 
  Admissible assignments assign arbitrary formulae to the 
  metavariables $A_1,\ldots,A_n$, and an axiom to the metavariable $F$.
\item 
  $P^n(A_1,\ldots,A_k,\ldots,A_k \impl A,\ldots,A_n) \ar 
   P^{n+1}(A_1,\ldots,A_n,A)$ 
  for each $n \geq 2$.
  The $A_k$ may also appear after $A_k \impl A$ in the sequence. 
  Admissible substitutions are the same as in the previous case.
\item   
  $P^n(A_1,\ldots,(A/x)A_k,\ldots,A_n) \ar  
   P^{n+1}(A_1,\ldots,(A/x)A_k,\ldots,A_n,\exists a A_k)$ 
  for each $n \geq 1$.
  An admissible assignment $\theta$ assigns arbitrary formulae  
  to $A_1,\ldots,A_n$ and a term to $A$.
\end{itemize} 
  Obviously there is a 1--1 correspondence between 
  theoremata of $H$ and terms which occur as argument
  of some $P^n$ in a $R_H$-reduction starting from $P^0$.

  Encoding a Gentzen style proof system is similar to 
  a Hilbert style system, the main idea being to translate
  inference rules into rewrite rules, proofs into terms and
  deduction into reduction. We refer to ~\cite{[KO95]} for full treatement.
\suppress{
  \subsection{Encoding of Gentzen style proof systems}

  A sequent calculus $G$ has rules of one of the two following forms, 
  where $\Gamma$ and $\Delta$ are lists of formulas 
  (we ignore structural rules, which do not cause problems for our encoding):

  $$r:\frac{\Gamma'\vdash\Delta'}{\Gamma\vdash\Delta},\,\,\,\,\,\,\,\,\,\,\,\,
  r:\frac{\Gamma'\vdash\Delta',\,\,\Gamma''\vdash\Delta''}{\Gamma\vdash\Delta}$$


  We present a sequent $F_1,\ldots,F_n\vdash G_1,\ldots,G_m$ from $G$ 
  as a term $P_{n,m}(F_1,\ldots,F_n,G_1,\ldots,G_m)$, 
  where $P_{n,m}$ is an $n+m$-ary function symbol. 
  A proof is presented as $r(sequ, pr_1)$ or $r(sequ, pr_1,pr_2)$, 
  depending on the number of premises in the $G$-rule, 
  where $r$ is the name of the last applied rule, 
  considered as a binary or ternary function symbol, 
  $sequ$ is the root of the proof tree in $G$, and  $pr_i$ 
  are representations of the proofs whose roots have been used as 
  the premises in the last step of the $G$-inference. 
  In a stage of a $G$-inference several subproofs $SPR_1,\ldots,SPR_k$ 
  are constructed. We represent that stage as $PS^k(pr_1,\ldots,pr_k)$, 
  where $pr_i$ is the representation of $SPR_i$.

  The CERS $R_G$ that encodes $G$ has three kinds of rewrite rule-schemata, 
  which correspond to introduction of axioms, and to applications 
  of one and two premise rules, respectively:
  1. $PS^k(pr_1,\ldots,pr_k)\ar 
     PS^{k+1}(pr_1,\ldots,pr_k,ax(axiom,\emptyset))$;
  2. $PS^k(pr_1,\ldots,r'(sequ',pr'),\ldots,pr_k)\ar 
     PS^k(pr_1,\ldots,r(sequ,r'(sequ',pr')),\ldots,pr_k)$;
  3. $\begin{array}{l}
       PS^k(pr_1,\ldots,r'(sequ',pr'),r''(sequ'',pr''),\ldots,pr_k)\ar \\
       \quad\quad\quad\quad\quad\quad\quad\quad
       PS^k(pr_1,\ldots,r(sequ,r'(sequ',pr'),r''(sequ'',pr'')),\ldots,pr_k);
     \end{array}$
  
  \noindentHere $axiom$ is the representation of an axiom of $G$ -- 
  a sequent of the form $\Gamma\vdash\Gamma$, $sequ$ represents the sequent 
  $\Gamma\vdash\Delta$, and similarly for $sequ'$ and $sequ''$. 
  Now a $G$-inference is encoded as an $R_G$-reduction starting from the constant $PS^0$.  

  \delete{
  For example, the rewrite schema for the $G$-rule 
  $$\forall^+:\frac{\Gamma\vdash F_1,\ldots,F[y/x],\ldots,F_n}{
    \Gamma\vdash F_1,\ldots,\forall xF,\ldots,F_n}$$
  where $y$ doesn't occur free in the lower sequent, has the form
  $$\begin{array}{l}
  PS^k(pr_1,\ldots,r'(P_{n,m}(\Gamma,F_1,\ldots,F[y/x],\ldots,F_n),\,pr'),\ldots,pr_k)\ar \\
  \quad\quad\quad\quad\quad\quad\quad\quad
  PS^k(pr_1,\ldots,\forall^+(P_{n,m}(\Gamma,F_1,\ldots,\forall xF,\ldots,F_n),r'(sequ,pr')),\ldots,pr_k)
  \end{array}$$
  where $m$ is the number of formulas in the list $\Gamma$ and the same condition on $y$ is required. 
  }
}

\subsection{Encoding of the $\pi$-calculus}

In this paragraph we will encode the version of 
$\pi$-calculus as described in~\cite{[Mil]} as a CERS.
Recall that $\pi$-calculus agents $P$, $Q$, \ldots 
are defined as follows:
\def\pipar{\mathord{\vert}}
\[P \mathrel{::=} 
  \overline{x}y.P \backor
  x(y).P          \backor
  0               \backor
  P \pipar P      \backor
  !P              \backor
  (x)P
\]
Basic interaction is generated from the rule
\[ x(y).P \pipar \overline{x}z.Q \ar 
   [z/y]P \pipar Q \]
by closing under unguarded contexts and working
modulo structural congruence (see \cite{[Mil]}).

To $\pi$-calculus a CERS $(\Sigma_\pi,R_\pi)$ can be associated as follows.
The alphabet $\Sigma_\pi$ consists of the function symbols
$0,!,\pipar,O$ with respective arities $0,1,2,3$, and
the quantifier symbols $I$ and $R$ with arities $(1,2)$ and $(1,1)$.
$I$ binds only in its last argument.
The map $[\,\,]$ transforms $\pi$-terms into terms in $Ter(\Sigma_\pi)$.
The only non-obvious cases are input, output and restriction:
\[ [x(y).P]          = Iy(x,[P])  \,;\,
   [\overline{x}z.Q] = O(x,z,[Q]) \,;\,
   [(x)P]            = Rx([P])
\]
Combining the transformation $[\,\,]$ with the closing under
unguarded contexts and the structural congruence leads to
rules $R_\pi$ of the form 
%\[ C[Iy(X,P),O(X,Z,Q)] \ar
%   C[(Z/y)P,Q] \zurab{where} \]
\[ C_1[Iy(X,P)]\,\vert\,C_2[O(X,Z,Q)] \ar 
   C_1[(Z/y)P]\,\vert\,C_2[Q]\mbox{\rm,\ where} \]
\begin{enumerate}
\item
  $P,Q,X,Z$ are metavariables, 
  and admissible assignments for $X,Z$ are variables.           
\item
%  Consider $C[Iy(X,P),O(X,Z,Q)]$.
%  The indicated subterms must be unguarded
%  (among the symbols above them only the operators 
%   $\pipar$, $!$ and $R$ can occur), and each 
%  restriction \zurab{$RX$} contains both or neither subterms.
  The indicated subterms must be unguarded in $C_1[\,]$ and $C_2[\,]$ 
  and not in the scope of $RX$ 
  (among the symbols above them only the operators 
   $\pipar$, $!$ and $Rx$ with $x\not= X$ can occur).
\item
   Only (all) unguarded contexts are admissible, for any redex.
\suppress{ 
  $C[\,\,]$ is a context such that among symbols above
  $Iy(X,P)$ and $O(X,Z,Q)$ in the LHS only the operators $\pipar$, $!$, and
  $Rx'$ with $x'\not=x$ can occur. 
  Thus $Iy(X,P)$ and $O(X,Z,Q)$ are unguarded, 
  and $X$ means the same for both processes.
  A context $C[\,\,]$ is admissible for an $R_{\pi}$-redex iff
  above the hole in $C[\,\,]$ only the operators $\pipar$, $!$, and $R$ can
  occur, i.e., admissible redexes are unguarded. (Note that it is not
  possible to bind, in an admissible redex, the occurrences of variables
  corresponding to $X$ with different occurrences of $R$.)}
\end{enumerate}
Obviously, the `critical pairs' for the interaction rule
are preserved by the translation, so $R_\pi$ is not orthogonal.
Nevertheless, we expect results like: for the standard translation
of $\lambda$- into $\pi$-calculus, $R_\pi$ is orthogonal hence
confluent modulo the structural congruence.

\begin{thebibliography}{99}

\bibitem[{Aka93}]{[Aka]}
Akama Y. On Mints' reduction for ccc-calculus. 
In: Proc.\ of the $1^{st}$ International conference on 
Typed Lambda Calculus and Applications, TLCA'93, LNCS, 
vol.~664, Bezem M., Groote J.F., eds., 1993, p.~1--12.

\bibitem[{AFMOW94}]{[A.F.]}
 Ariola Z.M., Felleisen M., Maraist J., Odersky M., Wadler P. 
 A Call-By-Need Lambda Calculus.
 In: Proc.\ ACM Conference on Principles of Programming Languages, 1995.

\bibitem[{BBKW89}]{[BBKW89]} 
 Baeten J.C.M., Bergstra J.A., Klop J.W., Weijland W.P. Term Rewriting Systems with rule priorities. Journal of TCS 67, 1989, p.~283--301.

\bibitem[{Bar84}]{[Bar]} 
Barendregt H.P.  The Lambda Calculus, its Syntax and Semantics.  North-Holland, 1984.

%\bibitem[{BW87}]{[BW87]}
 
\bibitem[{BK86}]{[B.K.]}
Bergstra J. A., Klop J. W. Conditional Rewrite Rules: confluence and termination. JCSS vol.~32, n.~3, 1986, p.~323--362.

%\bibitem[{DOS87}]{[DJS887]}
%Dershowitz N., Okada M., Sivakumar G. 
%Confluence of Conditional Rewrite Systems. 
%In: Proc.\ of the $1^{st}$ International Workshop on 
%Conditional Term Rewrite Systems, CTRS'87, LNCS, vol.~308, p.~31--44.

\bibitem[{DOS88}]{[DJS88]}
Dershowitz N., Okada M., Sivakumar G. Canonical conditional rewrite systems. 
In: Proc.\ of the $9^{th}$ International Conference on Automated Deduction, 
LNCS, vol.~310, p.~538--549.

\bibitem[{Kha92}]{[OCRS]} 
Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.

\bibitem[{Kha94}]{[lfcs]} 
Khasidashvili Z.  The longest perpetual reductions in orthogonal 
expression reduction systems. In: Proc.\ of the $3^{rd}$ 
International Conference on Logical Foundations of Computer Science, 
LFCS'94, LNCS, vol.~813, Nerode~A., Matiyasevich Yu.~V. eds. 
St.~Petersburg, 1994. p.~191--203.

\bibitem[{KO95}]{[KO95]}
Khasidashvili Z., van Oostrom V. Context-sensitive Conditional Rewrite Systems.
Report SYS-C95-06. University of East Anglia, 1995.

\bibitem[{Klo80}]{[Kl.CRS]}
Klop  J.W. Combinatory Reduction  Systems. Mathematical Centre  Tracts  127.  Centre  for  Mathematics  and  Computer Science, Amsterdam, 1980.

\bibitem[{Klo90}]{[Klo90]}
Klop J.W. Term Rewriting Systems. Report CS-R9073, 
Centre for Mathematics and Computer Science, 1990.

%\bibitem[{Klo92}]{[Klo92]} 
%Klop J.W. Term  Rewriting Systems. 
%In:  S.Abramsky, D.Gabby,  and T.Maibaum eds.  
%Handbook  of Logic in  Computer Science, vol.~II, 
%Oxford University Press, 1992.

\bibitem[{KOR93}]{[kor]}
Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction systems:
introduction and survey. In: To Corrado B\"ohm, J. of Theoretical
Computer Science 121, 1993, p. 279--308.

\bibitem[{Mel93}]{[Mel]}
Melli{\`e}s P.-A. An abstract theorem of finite developments.
Talk presented at CONFER-meeting, september 1993, Amsterdam.

\bibitem[{Mes92}]{[Mes]} 
Meseguer J. Conditional Rewriting Logic as a unified model of concurrency. Journal of TCS 96, 1992, p.~73--155.

\bibitem[{Mil92}]{[Mil]}
Milner R. Functions as processes. In: Journal of Mathematical structures in Computer Science. 2(2): 1992, p.~119--141.

\bibitem[{Ned73}]{[7]} 
Nederpelt R.P. Strong normalization for a typed lambda-calculus with lambda structured types. Ph.D. Thesis, Eindhoven, 1973.

\bibitem[{Nip93}]{[Nip.b]}
Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc.\ of the $1^{st}$ International conference on Typed Lambda Calculus and Applications, TLCA'93, LNCS, vol.~664, Bezem M., Groote J.F., eds., 1993, p.~306-317.

\bibitem[{Oos94}]{[Oos.th]} 
Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.~D. Thesis, Free University of Amsterdam, 1994.

\bibitem[{OR94}]{[OR94]}
Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc.\ of the $3^{rd}$ International  Symposium on Logical Foundations of Computer Science, LFCS'94, LNCS, vol.~813, Nerode~A., Matiyasevich~Yu.~V., eds. St.~Petersburg, 1994, p.~379-392.

\bibitem[{vR93}]{[vR.rta]}
Van Raamsdonk F. Confluence and superdevelopments. In: Proc.\ of the $5^{th}$ International Conference on Rewriting Techniques and Applications, RTA'93,
LNCS, vol.~690, C.~Kirchner, ed. Montreal, 1993, p.~168-182.

\bibitem[{Tak93}]{[Tak93]}
Takahashi M. $\lambda$-Calculi with Conditional Rules.
In: Proc.\ of the $1^{st}$ International conference on Typed Lambda Calculus and Applications, 
TLCA'93, LNCS, vol.~664, Bezem M., Groote J.F., eds., 1993, p.~406--417.

\bibitem[{Toy88}]{[Toy88]}
Toyama Y. Confluent term rewriting systems with membership conditions. In: Proc.\ of the $1^{st}$ 
International Workshop on Conditional Term Rewriting Systems,
LNCS, vol.~308, 1988, p.~128--141.

\bibitem[{Wol93}]{[Wol]}
Wolfram D. The clausal theory of types. Cambridge Tracts in Theoretical Computer Science, vol.~21, Cambridge University Press, 1993.

\end{thebibliography}
\end{document}
