%%\documentstyle[fullpage,11pt,amssymbols]{article} %%\documentstyle[fullpage,11pt]{article} %% %% ENTCS style: %% \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{\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. \suppress{Vincent: definitions should go in preamble, i.e. here} \suppress{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 }}{} } \suppress{Vincent: Elsevier uses defn \newtheorem{deff}{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} \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} \suppress{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 the notion of conditional TRS and generalizing it 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}