% Author-created version.
% The final version, available at
% http://www.springerlink.com/content/u222753gl333221p/
% and is copyrighted by Springer-Verlag.
\documentclass[runningheads,oribibl]{llncs}
%
\usepackage{makeidx} % allows for indexgeneration
%
\usepackage{amsfonts,amssymb,amsmath}
\usepackage{proof}
\usepackage{chngpage}
\usepackage[latin1]{inputenc}
\input{macros_modified}
\input{entete}
%\usepackage{hyperref}
\begin{document}
\title{Completion is an Instance of Abstract Canonical System Inference}
%
%\titlerunning{Completion and Abstract Canonical Systems} % abbreviated title (for running head)
% also used for the TOC unless
% \toctitle is used
%
\author{Guillaume Burel\inst{1} \and Claude Kirchner\inst{2}}
%
\authorrunning{Guillaume Burel \and Claude Kirchner} % abbreviated author list (for running head)
%
%%%% modified list of authors for the TOC (add the affiliations)
%\tocauthor{Guillaume Burel \and Claude Kirchner (LORIA Nancy)}
%
\institute{
Ecole Normale Supérieure de Lyon \& LORIA\thanks{UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP} % Université Henri Poincaré
\and
INRIA \& LORIA\footnotemark[1]
}
\maketitle % typeset the title of the contribution
\begin{abstract}
Abstract canonical systems and inference (ACSI) were introduced
%in \cite{DershowitzKirchner-lics2003,aci}
to formalize the intuitive notions of good proof
and good inference appearing typically in first-order logic or in Knuth-Bendix like
completion procedures.
Since this abstract framework is intended to be generic, it is of fundamental interest to
show its adequacy to represent the main systems of interest. This has been done for ground
completion (where all equational axioms are ground)
%in~\cite{DershowitzFTP2003}
but was still an
open question for the general completion process.
By showing that the standard completion
%\cite{KnuthBendix70}
is an instance of the ACSI
framework we close the question. For this purpose, two proof representations, proof terms
and proofs by replacement, are compared to built a proof ordering that provides an
instantiation adapted to the abstract canonical system framework. \medskip
\textbf{Classification:} Logic in computer science, rewriting and deduction, completion,
good proof, proof representation, canonicity.
\end{abstract}
%-------------\\
%-[ck: Dec 14 05] il faut ajouter encore un paragraphe sur les differents travaux voyant KB
%comme une instance d'un autre mécanisme:
%Struth, Aiguier\&Bahrami, lics[24] et contraster par rapport à ces travaux:
%
%``Je vois aussi a un certain lien entre ma these et l'article de LICS, mais (comme vous
%avez ecrit dans cet article) il y a pourtant une grande difference. Moi, je considerais
%les procedures KB, de Buchberger et de saturation clausale comme construction d'une base
%irredondante et irreducible qui permet des preuves normales. Mais je n'envisageais pas
%une theorie de preuve explcite comme vous l'avez fait. J'etait plutot motive par l'algebre
%et le travail de Le Chennadec, Marche et Buendgen sur la symmetrisation et les anneaux
%polynomiels (tu trouveras les references dans ma these) et sur l'algorithme de Burchberger
%comme procedure de completion. ''
%
%A vérifier: Karel Stokkermans a traite les memes procedures du point de vue categoriel
%dans sa these
%
%----------------- [ck: Jan 7 06]
\section{Introduction}
The notion of good proof is central in mathematics and crucial when mechanizing deduction,
in particular for defining useful and efficient tactics in proof assistant and theorem provers.
Motivated on one hand by this quest for \emph{good proof} theory and on the other by the
profound similarities between many proof search approaches, N. Dershowitz and C. Kirchner
proposed in \cite{DershowitzKirchner-lics2003,acp} a general framework based on
ordering the set of proofs. In this context the best proofs are simply the minimal one.
Once one has defined what the best proofs are by the mean of a proof ordering, the next
step is to obtain the best presentation of a theory, i.e.\ the set of axioms necessary for
obtaining the best proofs for all the theory, but not containing anything useless.
To formalize this, the notion of \emph{good inference} was introduced by M.P. Bonacina and
N. Dershowitz~\cite{aci}. Given a theory, its canonical presentation is defined as the set of
the axioms needed to obtain the minimal proofs. It is general enough to produce all best
proofs, leading to a notion of \emph{saturation}, but it does not contain any redundant
informations, hence the notion of \emph{contraction}. Presentations, i.e.\ sets of
axioms, are then transformed using appropriate deduction mechanisms to produce this
canonical presentation.
This leaded to the Abstract Canonical Systems and Inference (ACSI) generic framework
presented in~\cite{acp,aci}.
%\medskip
The ACSI framework got its sources of inspiration from three related points.
%
First, the early works on \emph{Proof orderings} as introduced
in \cite{Bachmair-87} and~\cite{BD-94} to prove the completeness of completion procedures
\textit{a la} Knuth-Bendix.
%
Second, the developments about
redundancy~\cite{HsiangRusi-jacm-91,BachmairGanzinger:HandbookAR:resolution:2001} to focus
on the important axioms to perform further inferences.
%
Last but not least, by the completion procedure \cite{KnuthBendix70}, central in most
theorem proving tools where an equality predicate is used. This procedure has been
refined, mainly for two purposes: to have a more specific and thus more efficient
algorithm when dealing with particular cases, or to increase the efficiency although
remaining general. For the first case, a revue of specific completion procedures for
specific algebraic structures can be found in \cite{LeChenadec-86}. For the second case,
completion has been extended to equational
completion~\cite{Huet80,PS81,JouannaudKirchnerSIAM86}; inductionless induction, initiated
by J.A. Goguen~\cite{Goguen80} and D. Musser~\cite{musser80ind}; and ordered completion
\cite{Lankfords75,HsiangRusi-jacm-91,BD-94}, to mention only a few. One important
application of the completion procedure is rewrite based programming, either based on
matching or on unification. The seminal work of J.A.~Goguen on OBJ and its various
incarnations~\cite{OBJ-book-1997} plays a preeminent role in this class of algebraic
languages and has directly inspired CafeOBJ~\cite{FutatsugiN-IEEE97},
ELAN~\cite{borovansky02a} or Maude~\cite{Maude-RwLg1996}. When the operational semantics of
the language is based on unification, we find logic programming languages of the Prolog
family, where EQLOG~\cite{Goguen1986b} is also a preeminent figure.
Good syntheses about
completion based rewrite programs can be found
in~\cite{DershowitzIC85,BonacinaMP:JLPrewprog}.
Several works intend to uniform this different completion procedures, and to make it a
special case of a more general process. The notion of critical-pair completion procedure
was introduced by \cite{Buchberger83} and covers not only standard completion, but also
Buchberger algorithm for Gr\"obner basis \cite{BuchbergerTHESE,WinklerISSAC89} and
resolution~\cite{Robinson65}. Indeed, R. B\"undgen shown that Buchberger's algorithm can
be simulated by standard completion~\cite{Buendgen91}. This concept of critical-pair
completion was categorically formalized by
K. Stokkermans~\cite{DBLP:conf/ctrs/Stokkermans92}. Other generalizations can be found in
works of M. Schorlemmer~\cite{DBLP:journals/entcs/Schorlemmer98}, M. Aiguier and
D. Bahrami~\cite{AiguierBahrani-jar} or in the PhD of G. Struth~\cite{Struth-PhD}, where standard completion,
Buchberger's algorithm and resolution are shown to be special instantiation of a
non-symmetric completion procedure.
But, even if initially motivated by these three points, the ACSI framework has been
developed as a full stand alone theory. This theory provide important abstract results
based on basic hypothesis on proofs and a few postulates.
Therefore, a main question remains: is this framework indeed useful? Does this theory allows
to \emph{uniformly} understand and prove the main properties of a proof system, centered around
the appropriate ordering on proofs?
At the price of a slight generalization of two postulates, it is shown
in~\cite{Burel-master}, that good proofs in natural deduction are indeed the cut free
proofs as soon as proofs are compared using the ordering induced by beta reduction over
the simply typed lambda-terms.
%
For ground completion, the adequacy of the framework has been shown
in~\cite{DershowitzFTP2003}, leaving the more general question of standard completion
open.
This paper proves the adequacy to the framework for the standard completion procedure,
generalizing in a non trivial way the result of~\cite{DershowitzFTP2003} and showing the
usefulness of abstract canonical systems.
This brings serious hopes that the ACSI framework is indeed well
adapted and useful to uniformly understand and work with other
algorithms, in particular all the ones based on critical-pair
completion.
\medskip
The next section will summarize the framework of abstract canonical systems, as
defined in \cite{acp,aci}, and briefly recall the standard completion. Section
\ref{sec:pr} deals with two representations of proofs in equational logic, namely as proof
terms in the rewriting logic~\cite{MeseguerTCS92}, and as proof by
replacement~\cite{Bachmair-87}. We will show how to combine them to keep the tree
structure of the first one, and the ordering associated with the second one, which is well
adapted to prove the completeness of the standard completion. Finally, in
Section~\ref{sec:csc}, we will apply the abstract canonical systems framework to this
proof representation to show the completeness of the standard completion. The proofs
details are given in the Appendix.
\section{Presentation}
\subsection{Abstract Canonical Systems}
The results in this section are extracted from \cite{acp,aci}, which
should be consulted for motivations, details and proofs. %% The proofs mentioned here, unless
%% otherwise specified by a reference, are corrections from the original
%% ones.
Let $\A$ be the set of all formul\ae\ over
some fixed vocabulary. Let $\P$ be the set
of all proofs. These sets are linked by two functions: $\Ax\cdot:\P\rightarrow 2^\A$ gives
the \Def{premises} in a proof, and
$\Cl\cdot:\P\rightarrow \A$ gives its
\Def{conclusion}. Both are extended to sets of proofs in the usual
fashion. The set of proofs built using assumptions in $A\subseteq\A$
is noted by\footnote{$\inlinedf$ is used for definitions.}
$$\Pf A\df \left\{p\in\P : \Ax p\subseteq A\right\}\enspace.$$
The framework proposed here is predicated on two {\em well-founded}
partial orderings over $\P$: a \Def{proof ordering} $>$ and a
\Def{subproof relation} $\rhd$. They are related by a monotonicity
requirement (postulate \ref{post:replacement}). We assume for
convenience that the proof ordering only compares proofs with the same
conclusion ($p> q\Rightarrow \Cl p=\Cl q$), rather than mention this
condition each time we have cause to compare proofs.
We will use the term \Def{presentation} to mean a set of
formul\ae, and \Def{justification} to mean a set of proofs. We
reserve the term \Def{theory} for deductively closed
presentations:
$$
\Th A ~~\df~~ \Cl{\Pf A} ~~=~~ \{\Cl p \st p\in\P,~ \Ax p
\subseteq A\}\enspace.
$$
Theories are monotonic:
\begin{proposition}[Monotonicity]\label{prop:mono}
For all presentations $A$ and $B$:
$$ A\subseteq B \imp \Th A\subseteq \Th B$$
\end{proposition}
Presentations $A$ and $B$ are \Def{equivalent}
($A ~\equiv ~ B $) if their theories are
identical: $\Th A = \Th B$.
In addition to this, we assume the two following postulates:
\begin{post}[Reflexivity]\label{post:refl}
For all presentations $A$:
$$ A\subseteq \Th A$$
\end{post}
\begin{post}[Closure]\label{post:closure}
For all presentations $A$:
$$ \Th{\Th A}\subseteq \Th A$$
\end{post}
We call a proof
\Def{trivial} when it proves only its unique assumption and has no
subproofs other than itself, that is, if $\Ax p = \{\Cl p\}$ and
$p\unrhd q\Rightarrow p=q$, where $\unrhd$ is the reflexive closure of
the subproof ordering $\rhd$. We denote by $\triva
a$ such a trivial proof of $a\in\A$
and by $\triva A$ the set of trivial proofs of each $a\in A$.
We assume that proofs use their assumptions (postulate
\ref{post:premSubproofs}), that subproofs don't use non-existent
assumptions (postulate \ref{post:premMono}), and that proof orderings
are monotonic with respect to subproofs (postulate \ref{post:replacement}):
\begin{post}[Trivia]\label{post:premSubproofs}
For all proofs $p$ and formul\ae\ $a$:
$$a\in\Ax p \imp p\unrhd\triva a$$
\end{post}
\begin{post}[Subproofs Premises Monotonicity]
\label{post:premMono}
For all proofs $p$ and $q$:
$$p\unrhd q\imp \Ax p\supseteq \Ax q$$
\end{post}
\begin{post}[Replacement]\label{post:replacement}
For all proofs $p$, $q$ and $r$:
$$p\rhd q > r \imp \exists v\in \Pfa{\Ax p\cup\Ax r}.~ p > v\rhd r$$
\end{post}
We make no other assumptions regarding proofs or their structure. As
remarked in \cite{aci}, the subproof relation essentially defines a
tree structure over proof: a ``leaf'' is a proof with no subproofs but
itself, and direct subproofs, i.e. subproofs that are not subproofs of
another subproof, can be considered as ``subtrees''. These trees can
be infinitely branching, but their height is finite because of the
wellfoundedness of $\rhd$.
The proof ordering $>$ is lifted to an ordering $\simpler$ over presentations:
$$A\simpler B\mbox{ if }A~\equiv~ B\mbox{ and }\forall p\in\Pf A~\exists q\in\Pf B.~p\geq q\enspace.$$
We define what a \emph{normal-form proof} is, i.e. one of the
minimal proofs of $\Pf{\Th A}$:
$$\Nf A\df\mu\Pf{\Th A} \df \{p\in\Pf{\Th A}~:~\neg\exists q\in\Pf{\Th
A}.~p>q\}\enspace.$$
The \Def{canonical presentation} contains those formul\ae\ that
appear as assumptions of normal-form
proofs:
\[ A^\sharp \df \Ax{\Nf A}\enspace. \]
So, we will say that $A$ is \Def{canonical} if $A=A^\sharp$.
A presentation $A$ is \Def{saturated} if it supports all possible
normal form proofs: $$\Pf A \supseteq \Nf A\enspace.$$
The set of all \Def{redundant formul\ae} of a given presentation $A$
will be denoted as follows:
\[
\Red A ~~\df~~ \left\{r \in A \st A \simpler A\setminus
\{r\}\right\} \enspace .\]
and a presentation $A$ is \Def{contracted} if
$$ \Red A = \emptyset \enspace.$$
The following main result can then be derived~\cite{DershowitzKirchner-lics2003}:
\begin{theorem}
A presentation is canonical iff it is saturated and contracted.
\end{theorem}
We now consider inference and deduction mechanisms.
A \Def{deduction mechanism} $\infers$ is a function from
presentations to presentations and we call the relation
$A \infers B$ a \Def{deduction step}.
%
A sequence of presentations $A_0 \leadsto A_1 \leadsto \cdots$ is
called a \Def{derivation}.
%
The \emph{result} of the derivation is, as usual, its
\Def{persisting} formul\ae:
\[A_\infty \df \liminf_{j\rightarrow\infty} A_j ~=~ \bigcup\limits_{j>0}
\bigcap\limits_{i>j} A_i \enspace.\]
%% We also define the set of all generated
%% formul\ae:
%% $$A_*=\bigcup\limits_{i>0}A_i$$
A deduction mechanism $\infers$ is \Def{sound} if $A \infers B$
implies $\Th B \subseteq \Th A$. It is \Def{adequate} if $A \infers
B$ implies $\Th A \subseteq \Th B$. It is \Def{good} if proofs only
get better:
$$
\infers ~\subseteq~ \simpler
\enspace.$$
A derivation $A_0 \leadsto A_1 \leadsto \cdots$ is \Def{good} if
$A_i \simpler A_{i+1} $ for all $i$.
We now extend the notion of saturation and contraction to
derivation:
\begin{itemize}
\item A derivation $\{A_i\}_i$ is \Def{saturating} if $A_\infty$ is
saturated.
\item It is \Def{contracting} if $A_\infty$ is contracted.
\item It is \Def{canonical} if both saturating
and contracting.
\end{itemize}
A canonical derivation can be used to build the canonical presentation
of the initial presentation:
\begin{theorem}\label{lemma:limit_canon}
A good derivation is canonical if and only if $$A_\infty=A_0^\sharp\enspace.$$
\end{theorem}
%% \begin{defi}[Fairness]\
%% A good derivation is \Def{uniformly fair} if
%% $$\triva{A_\infty}\setminus\triva{A_0^\sharp}\better\Pf {A_*}$$
%% \end{defi}
%% \begin{theo}
%% If a good derivation is uniformly fair, then its limit is saturated.
%% \end{theo}
\subsection{The Standard Completion}
The standard completion algorithm was first introduced by Knuth and
Bendix in \cite{KnuthBendix70}, hence the name it is often called.
Its correctness was first shown by Huet in
\cite{Huet-81}, using a fairness hypothesis. We use here
a presentation of this algorithm as inference rules (see Fig.
\ref{fig:KB}), as can be found in \cite{Bachmair-87}. For basics on rewritings and
completions, we refer to~\cite{BaaderNipkowREW-98,KirchnerKirchner-RSP-99}.
The Knuth-Bendix algorithm consists of 6 rules which apply to a couple
$E,R$ of a set of equational axioms and a set of rewriting rules. It
takes a reduction ordering $\tg$ over terms as argument. The rules
are presented in Fig. \ref{fig:KB}.
\begin{rules}[!ht]{fig:KB}{Standard Completion Inference Rules.}
\Rule{Deduce:}
If $(s,t)$ is a critical pair of $R$
$$E,R~~\infers~~ E\cup\{s=t\},R$$
\Rule{Orient:}
If $s\tg t$
$$ E\cup\{s=t\},R~~\infers~~ E, R\cup\{s\rightarrow t\}$$
\Rule{Delete:}
$$E\cup\{s=s\},R~~\infers~~ E,R$$
\Rule{Simplify:}
If $s\rewrite[R] u$
$$ E\cup\{s=t\},R~~\infers~~ E\cup\{u=t\}, R$$
\Rule{Compose:}
If $t\rewrite[R] u$
$$E,R\cup\{s\rightarrow t\}~~\infers~~ E,R\cup\{s\rightarrow u\}$$
\Rule{Collapse\footnote{$\encord$ designate the encompassment ordering, $s\encord
t$ if a subterm of $s$ in an
instance of $t$ but not vice versa.}:}
If $\rpfstep s{v\rightarrow w\in R}{}u$, and $s\encord
v$,
$$ E,R\cup\{s\rightarrow t\}~~\infers~~ E\cup\{u=t\}, R$$
\end{rules}
Since \cite{Huet-81}, standard completion is associated
with a fairness assumption (see \cite[Lemma 2.8]{Bachmair-87}): at the
limit, all equations are oriented ($E_\infty=\emptyset$) and all
persistent critical pairs coming from $R_\infty$ are treated by
\Rule{Deduce} at least once.
Because we work with terms with variables, the reduction ordering
$\tg$ cannot be total, so that \Rule{Orient} may fail. Therefore, the
standard completion algorithm may either:
\begin{itemize}
\item terminate with success and yield a terminating, confluent set of
rules;
\item terminate with failure; or
\item not terminate.
\end{itemize}
Here, the completeness of the standard completion will only be shown using the ACSI
framework for the first case.
\section{Proof Representations}\label{sec:pr}
Our goal is now to use the ACSI framework to directly show that standard completion
inference rules are correct and complete. We have therefore first to find the right order
on proofs. We have two main choices that we are now defining and relating.
\subsection{Proof Terms}
Let us first consider the proof representation coming from the one
used in rewriting logic (introduced by Meseguer \cite{MeseguerTCS92},
see also \cite{KirchnerKV-MIT95}). Consider a signature $\Sigma$, and
a set of variable $V$. The set of terms built upon these signature and
variables is noted $\terms\Sigma V$. Consider also a set of equational
axioms $E$ and a set of rewrite rules $R$ based on this signature. To
simplify the notations of proof terms, equational axioms and rewrite
rules are represented by labels not appearing in the signature
$\Sigma$. An equational axiom or a rewrite rule $(l,r)\in E\cup R$
will be also noted $(l(\vect x),r(\vect x))$ where $\vect x$ are the
free variables of both sides. We consider the rules of the equational
logic given in the Fig.~\ref{fig:EL}. These inference rules define the
\Def{proof term} associated with a proof. The notation
$\pi:t\longrightarrow t'$ means that $\pi$ is a proof term---that
could also be seen as a trace--- showing that the term $t$ can be
rewritten to the term $t'$.
\begin{rules}{fig:EL}{Inference Rules for Equational Logic}
\Rule{Reflexivity:}
$$\infer{t:t\rewrite t}{}$$
\Rule{Congruence:}
$$\infer{f(\vect\pi):f(\vect t)\rewrite f(\vect{t'})}
{\pi_1:t_1\rewrite t_1' &\ldots & \pi_n:t_n\rewrite t_n'}$$
\Rule{Replacement:}
For all rules or equational axioms\\ $\ell=(g(\vect x), d(\vect x)) \in
E\cup R$,
$$\infer{\ell(\vect\pi):g(\vect t)\rewrite d(\vect{t'})}
{\pi_1:t_1\rewrite t_1' &\ldots & \pi_n:t_n\rewrite t_n'}$$
\Rule{Transitivity:}
$$\infer{\pi_1;\pi_2:t_1\rewrite t_3}
{\pi_1:t_1\rewrite t_2 & \pi_2:t_2\rewrite t_3}$$
\Rule{Symmetry:}
$$\infer{\pi^{-1}:t_2\rewrite t_1}
{\pi:t_1\rewrite t_2}$$
\end{rules}
By definition, $\terms\Sigma V$ is plunged into the proof terms when
they are formed with the rules \Rule{Reflexivity} and
\Rule{Congruence}. Also, \Rule{Reflexivity} for $t\longrightarrow t$
is not essential because it can be replaced by a tree of
\Rule{Congruence} isomorph to $t$. The proof terms associated are
furthermore the same in both case: $t$. Notice that these proof
terms are a restricted form of rho-terms~\cite{rhoCalIGLP-I+II-2001}.
\begin{example}
Consider the rewrite rules and equational axiom
$$\ell_1 : g(x)\rewrite
d(x),~~ \ell_2 : s=t,~~\ell_3:l\rewrite r,$$
\begin{itemize}
\item $r$ is a proof term of $r=r$,
\item $f(\ell_1(\ell_2),(\ell_3;r)^{-1})$ is a proof term of
$f(g(s),r)=f(d(t),l)$.
\end{itemize}
\end{example}
\medskip
Some proof terms defined here are ``essentially the same''. For
instance, the transitivity operator should be considered as
associative, so that the proofs $(\pi_1;\pi_2);\pi_3$ and
$\pi_1;(\pi_2;\pi_3)$ are equal. This can be done by quotienting the
proof terms algebra by the congruence rules of Fig. \ref{fig:cong}.
In particular, in proof terms, parallel rewriting can be combined in
one term without transitivity. The \Rule{Parallel Moves Lemma}
equivalence corresponds to the fact that this parallel rewriting can
be decomposed by applying first the outermost rule, then the
innermost, or conversely. (About the Parallel Moves Lemma, see for
instance \cite{HuetLevyCL1}.)
\begin{rules}{fig:cong}{Equivalence of Proof Terms}
\Rule{Associativity:}
For all proof terms $\pi_1,\pi_2,\pi_3$,
$$\pi_1;(\pi_2;\pi_3)\congr(\pi_1;\pi_2);\pi_3$$
\Rule{Identities:}
For all proof terms $\pi:t\rewrite t'$,
$$\pi;t'\congr t;\pi\congr\pi$$
\Rule{Preservation of Composition:}
For all proof terms $\vect{\pi},\vect{\pi'}$, for all function symbols $f$,
$$f(\pi_1;\pi'_1,\ldots,\pi_n;\pi'_n)\congr f(\vect\pi);f(\vect{\pi'})$$
\Rule{Parallel Moves Lemma:}
For all rewrite rules or equational axiom $\ell=(g(\vect x), d(\vect
x)) \in E\cup R$, for all proof terms $\pi_1:t_1\rewrite
t_1',\ldots,\pi_n:t_n\rewrite t_n'$,
$$\begin{array}{r@{\congr}l}
\ell(\vect\pi) & \ell(\vect t);d(\vect\pi)\\
& g(\vect\pi);\ell(\vect{t'})
\end{array}
$$
\Rule{Inverse:}
For all proof terms $\pi:t\rewrite t'$,
$$\begin{array}{r@{\congr}l}\pi;\pi^{-1}&t\\\pi^{-1};\pi&t'\end{array}$$
\end{rules}
\begin{example}
From the rules \Rule{Associativity}, \Rule{Identities} and
\Rule{Inverse} we can deduce that the proofs
$(\pi_1;\pi_2)^{-1}$ and $\pi_2^{-1};\pi_1^{-1}$ are equivalent:
$
\begin{array}{rl}
(\pi_1;\pi_2)^{-1} &\congr (\pi_1;\pi_2)^{-1};t\\&
\congr (\pi_1;\pi_2)^{-1};\pi_1;\pi_1^{-1}\\&
\congr (\pi_1;\pi_2)^{-1};\pi_1;t';\pi_1^{-1}\\&
\congr (\pi_1;\pi_2)^{-1};\pi_1;\pi_2;\pi_2^{-1};\pi_1^{-1}\\&
\congr t'';\pi_2^{-1};\pi_1^{-1}\\&
\congr \pi_2^{-1};\pi_1^{-1}\enspace.
\end{array}
$
We
similarly have $f(\vect\pi)^{-1}$ equivalent to $f(\vect{\pi^{-1}})$,
because $
\begin{array}{rl}
f(\vect{\pi^{-1}})&\congr f(\vect{\pi^{-1}});f(\vect t)\\&
\congr f(\vect{\pi^{-1}});(f(\vect\pi);f(\vect\pi)^{-1})\\&
\congr (f(\vect{\pi^{-1}});f(\vect\pi));f(\vect\pi)^{-1}\\&
\congr f(\pi_1^{-1};\pi_1,\ldots,\pi_n^{-1};\pi_n);f(\vect\pi)^{-1}\\&
\congr f(\vect{t'});f(\vect\pi)^{-1}\\&
\congr f(\vect\pi)^{-1} \enspace.
\end{array}
$
\end{example}
\subsection{Proofs by Replacement of Equal by Equal}
This proof representation was introduced by \cite{Bachmair-87}
to prove the completeness of the Knuth-Bendix completion algorithm,
using an ordering over such proofs that decreases for every completion
step.
An \Def{equational proof step} is an expression $\epfstep s e p t$
where $s$ and $t$ are terms, $e$ is an equational axiom $u=v$, and
$p$ is a position of $s$ such that $\subterm s p = \sigma(u)$ and
$t=\replacement s{\sigma(v)}p$ for some substitution $\sigma$.
An \Def{equational proof} of $s_0=t_n$ is any finite sequence of
equational proof steps $\left(\epfstep {s_i} {e_i} {p_i}
{t_i}\right)_{i\in\{0,\ldots,n\}}$ such that $t_i = s_{i+1}$ for all
$i\in\{0,\ldots,n-1\}$. It is noted:
$$\epfstep {s_0} {e_0} {p_0}
{\epfstep {s_1} {e_1} {p_1} {s_2\cdots\epfstep {s_n} {e_n} {p_n}
{t_n}}} \enspace.$$
A \Def{rewrite proof step} is an expression $\rpfstep s \ell p
t$ or $\lpfstep t \ell p s$
where $s$ and $t$ are terms, $\ell$ is a rewrite rule $u\rightarrow
v$, and $p$ is a position of $s$ such that $\subterm s p =
\sigma(u)$ and $t = \replacement s{\sigma(v)}p$ for some
substitution $\sigma$.
An \Def{proof by replacement (of equal by equal)} of $s_0=t_n$ is
any finite sequence of equational proof steps and rewrite proof step
$\left(\upfstep[i] {s_i}
{\ell_i} {p_i}
{t_i}\right)_{i\in\{0,\ldots,n\}}$ where
$\upfstep[i]{}{}{}{}\in\{\epfstep{}{}{}{},\rpfstep{}{}{}{},\lpfstep{}{}{}{}\}$
for $i\in\{0,\ldots,n\}$ and such that $t_i = s_{i+1}$ for all
$i\in\{0,\ldots,{n-1}\}$. It is noted:
$$\upfstep [0]{s_0} {\ell_0} {p_0} {\upfstep [1]{s_1} {\ell_1} {p_1}
{s_2\cdots\upfstep [n]{s_n} {\ell_n} {p_n} {t_n}}}\enspace.$$
\begin{example}
Consider the rewrite rules and equational axiom:
$$\ell_1 : g(x)\rewrite
d(x),~~ \ell_2 : s=t,~~ \ell_3:l\rewrite r,$$
\begin{itemize}
\item $r$ is a proof by
replacement of $r=r$ (empty sequence),
\item $\rpfstep{f(g(s),r)}{\ell_1}1{\epfstep{f(d(s),r)}{\ell_2}{11}{\lpfstep{f(d(t),r)}{\ell_3}2{f(d(t),l)}}}$
is a proof by replacement of $f(g(s),r)=f(d(t),l)$.
\end{itemize}
\end{example}
\subsection{From Proof Terms to Proofs by Replacement}
In order to have a one to one correspondence between proof
representations, we use the equivalence of proof terms
defined in Fig. \ref{fig:cong}. We can refine them to the proof
term rewrite system $\ptrs$ given in
Fig. \ref{fig:PTRS}, in which $\pi,\pi',\pi_1,\ldots$ range over
proof terms, $t,t',t_1,\ldots$ over $\Sigma$-terms, $f,g,d$ over
function symbols, $\ell$ over rules and equational axioms labels and
$i$ and $k$ over $\vectset$.
\begin{rules}[!ht]{fig:PTRS}{Rewrite System for Proof Terms}
\Rule{Delete Useless Identities:}
$$\left.\begin{array}{c}
\pi;t'\\t;\pi\end{array}\right\}\ptrs\pi$$
\Rule{Sequentialization:}
If $\pi_k:t_k\rewrite t'_k$ and there exists
$i\neq j\in\{1,\ldots,n\}$ such that $\pi_i\neq t_i$ and $\pi_j\neq t_j$,
$$f(\vect\pi)~\ptrs~f(\pi_1,t_2,\ldots,t_n);f(t'_1,\pi_2,\ldots,t_n);\ldots;f(t'_1,t'_2,\ldots,\pi_n)$$
\Rule{Composition Shallowing:}
If $\pi_i:t_i\rewrite t_i'$ and $\pi'_i:t'_i\rewrite {t'_i}'$,
$$f(t_1,\ldots,\pi_i;\pi'_i,\ldots,t_n)~\ptrs~f(t_1,\ldots,\pi_i,\ldots,t_n);f(t_1,\ldots,\pi'_i,\ldots,t_n)$$
\Rule{Parallel Moves:}
If $\ell=(g(\vect x), d(\vect x))$, $\pi_1:t_1\rewrite
t_1',\ldots,\pi_n:t_n\rewrite t_n'$, and if there exists
$i\in\{1,\ldots,n\}$ such that $\pi_i\neq t_i$,
$$\ell(\vect\pi)~\ptrs\ell(\vect t);d(\vect\pi)$$
\Rule{Delete Useless Inverses:}
$$t^{-1}\ptrs t$$
\Rule{Inverse Congruence:}
If $\pi_i:t_i\rewrite t'_i$,
$$f(t_1,\ldots,\pi_i^{-1},\ldots,t_n)~\ptrs~f(t_1,\ldots,\pi_i,\ldots,t_n)^{-1}$$
\Rule{Inverse Composition:}
$$(\pi_1;\pi_2)^{-1}~\ptrs~\pi_2^{-1};\pi_1^{-1}$$
\end{rules}%
The associativity is still considered in the congruence, so that all
proof terms rewrite rules must be considered modulo the
associativity of $;$ which will be noted
$\assoc$. The class rewrite system that
we consider will be therefore noted
$\ptrs/\assoc$. As it is linear,
we can use the framework and results from \cite{Huet80}.
We first prove that this rewrite system is included in the equivalence
relation of Fig. \ref{fig:cong}.
\begin{proposition}[Correctness]
For all proof terms $\pi_1,\pi_2$, if $\pi_1\ptrs\pi_2$ then
$\pi_1\congr\pi_2$.
\end{proposition}
The converse is false: for instance $f(\ell_1,\ell_2)\congr
f(t_1,\ell_2);f(\ell_1,t'_2)$ but we do not have
$f(\ell_1,\ell_2)\mathop{\leftrightarrow}\limits_{\ptrs}^*
f(t_1,\ell_2);f(\ell_1,t'_2)$.
\begin{proposition}[Termination and Confluence]
The proof term rewrite system $\ptrs$ modulo $\assoc$ is terminating
and confluent modulo $\assoc$.
\end{proposition}
The proof terms rewrite system $\ptrs$ allow us to give a
correspondence between proof terms and proofs by replacement of equal
by equal: normal forms of proof terms correspond exactly to proofs by
replacement. This fact is expressed in the following theorem, which is
indeed a generalization of Lemma 3.6 in \cite{MeseguerTCS92} for
equational logic. We also have operationalized the way to construct
the chain of ``one-step sequential rewrites''.
\begin{theorem}[Correspondence between Proof Representations]\label{theo:corr}
The normal form of a proof term $\pi$ for the rewrite system
$\ptrs$, noted $\ptrsnf(\pi)$, has the following form:
For some $n\in\mathbb N$, some contexts
$w_1[],\ldots,w_n[]$, some indices $\vect i\in\{-1,1\}$,
some rule labels $\vect\ell$ and some terms
$\vect[m_1]{t^1},\ldots,\vect[m_n]{t^n}$:
$$\ptrsnf(\pi)
=
(w_1[\ell_1(\vect[m_1]{t^1})])^{i_1};\ldots;(w_n[\ell_n(\vect[m_n]{t^n})])^{i_n}$$
where for all proof terms $\nu$, $\nu^1$ is a notation for $\nu$.
\medskip
Such a proof term correspond with the following proof by replacement
of equal by equal:
$$\upfstep[1]{w_1[g_1(\vect[m_1]{t^1})]}{\ell_1}{p_1}{\upfstep[2]{w_1[d_1(\vect[m_1]{t^1})]}{\ell_2}{p_2}\cdots}
\upfstep[n]{}{\ell_n}{p_n}{w_n[d_n(\vect[m_n]{t^n})]}$$
where for all $j\in\{1,\ldots,n\}$ we have:
\begin{itemize}
\item $\ell_j=(g_j,d_j)$,
\item $p_j$ is the position of $[]$ in $w_j[]$,
\item $\upfstep[j]{}{}{}{}=$\begin{tabular}[t]{cl}$\rpfstep{}{}{}{}$& if $i_j=1$ and
$\ell_j\in R$,\\$\lpfstep{}{}{}{}$& if $i_j=-1$ and
$\ell_j\in R$,\\$\epfstep{}{}{}{}$& if $\ell_j\in E$.\end{tabular}
\item if $j\neq n$,
$w_j[d_j(\vect[m_j]{t^j})]=w_{j+1}[g_{j+1}(\vect[m_{j+1}]{t^{j+1}})]$.
\end{itemize}
\end{theorem}
\begin{example}
Consider $\pi=f(\ell_1(\ell_2),(\ell_3;r)^{-1})$ where $\ell_1 : g(x)\rewrite
d(x)$, $\ell_2 : s=t$, $\ell_3:l\rewrite r$, we have:\\
$\begin{array}{r@{~\rewrite[\ptrs]~}l@{\hspace{2em}}l} \pi &
f(\ell_1(s);d(\ell_2),(\ell_3;r)^{-1}) & \text{(\Rule{Parallel Moves})}\\
& f(\ell_1(s);d(\ell_2), r); f(d(t),(\ell_3;r)^{-1}) &
\text{(\Rule{Sequentialization})}\\
& f(\ell_1(s);d(\ell_2), r); f(d(t), r^{-1};\ell_3^{-1})&
\text{(\Rule{Inverse Composition})}\\
& f(\ell_1(s);d(\ell_2), r); f(d(t), r;\ell_3^{-1})&
\text{(\Rule{Delete Useless Inverses})}\\
& f(\ell_1(s);d(\ell_2), r); f(d(t), \ell_3^{-1})&
\text{(\Rule{Delete Useless Identities})}\\
& f(\ell_1(s),r);f(d(\ell_2), r); f(d(t), \ell_3^{-1})&
\text{(\Rule{Composition Shallowing})}\\
& f(\ell_1(s),r);f(d(\ell_2), r); f(d(t), \ell_3)^{-1}&
\text{(\Rule{Inverse Congruence})}\\
\end{array}
$
This last term is the normal form proof term, and it is equivalent to
the proof by replacement
$\rpfstep{f(g(s),r)}{\ell_1}1{\epfstep{f(d(s),r)}{\ell_2}{11}{\lpfstep{f(d(t),r)}{\ell_3}2{f(d(t),l)}}}$.
\end{example}
Due to this theorem, normal forms of proof terms can be considered in
the following indifferently as proof terms or as proofs by replacement.
\subsection{Proofs Ordering}
The representation of Bachmair by the mean of proof by replacement
was defined to introduce an order on proofs \cite{Bachmair-87}:
given a reduction ordering $\tg$, to each single proof steps
$\upfstep s \ell p t$ is associated a \Def{cost}. The cost of an
equational proof step $\epfstep s {u=v} p t$ is the triple $(\lmbra
s,t\rmbra,u,t)$. The cost of a rewrite proof step $\rpfstep s
{u\rightarrow v} p t$ is $(\lmbra s\rmbra,u,t)$. Proof steps are
compared with each other according to their cost, using the
lexicographic combination of the multiset $\mult{\tg}$ extension of
the reduction ordering over terms in the first component, the
encompassment ordering $\encord$ on the second component, and the
reduction ordering $\tg$ on the last component. Proofs are compared
as multisets of their proof steps. For two proofs by replacement
$p,q$, we will write $p>_{rep}q$ if $p$
is greater than $q$ for such an ordering.
Using theorem \ref{theo:corr}, we can translate Bachmair's proof
ordering to proof terms:
\begin{definition}[Bachmair's Ordering on Proof Terms]
For all proof terms $\pi_1,\pi_2$, we say that
$\pi_1>_{B}\pi_2$ iff
$$ \ptrsnf(\pi_1)>_{rep} \ptrsnf(\pi_2) \enspace.$$
\end{definition}
\begin{example}\label{exa:bordering}
Suppose we have $\Sigma=\{f^1,a^0,b^0,c^0\}$ where the exponents of
function symbols denote their arity, and a precedence $f>a>b>c$.
Consider $\pi_1 = f(\ell_1^{-1};\ell_2)$ and $\pi_2=f(\ell_3)$ where
$\ell_1=a\rewrite b$, $\ell_2=a\rewrite c$ and $\ell_3={b = c}$,
and suppose $a>b>c$.
We have
$\ptrsnf(\pi_1)=\lpfstep{f(b)}{\ell_1}{1}{\rpfstep{f(a)}{\ell_2}{1}{f(c)}}$
and $\ptrsnf(\pi_2)=\rpfstep{f(b)}{\ell_3}{1}{f(c)}$. The cost of
$\ptrsnf(\pi_1)$ is $\lmbra (\lmbra f(a) \rmbra,a,f(b)), (\lmbra f(a)
\rmbra, a, f(c)) \rmbra$, the cost of $\ptrsnf(\pi_2)$ is $\lmbra (\lmbra
f(b),f(c) \rmbra,b,f(c)) \rmbra$, so $\ptrsnf(\pi_1)>_{rep}\ptrsnf(\pi_2)$ and
$\pi_1>_B\pi_2$.
\end{example}
As we can see, the way we define the ordering over proofs is not
trivial. The question remains if we could have defined it more
directly, without using the representation as proof by
replacement. The following statement give a beginning of answer: we cannot
hope to extend an RPO on $\Sigma$-terms to a RPO\footnote{Or better an
ordering compatible with associativity, such as the $AC$-RPO
\cite{rubio95total}.} $\rpo>$ on proof terms so that $>_B$ and $\rpo>$
coincide for the normal forms of proof terms:
\begin{cexample}
With the same hypothesis as in Example \ref{exa:bordering}, let
$\ell_f=f(a)\rewrite c$ and $\ell_b = b\rewrite c$.
We now want to extend the precedence to $\ell_f$ and $\ell_b$ in order
to extend the RPO to proof terms. If we have $\ell_f<\ell_b$,
$\rpfstep{f(a)}{\ell_f}\epsilon c>_{rep}\rpfstep b{\ell_b}\epsilon c$ but
$\ell_f\rpo<\ell_b$.
If we suppose $f>\ell_f>\ell_b$ we have $\rpfstep{f(a)}{\ell_f}\epsilon
c >_{rep} \rpfstep{f(b)}{\ell_b}{1}{f(c)}$ but $\ell_f \rpo<
f(\ell_b)$.
If we suppose $\ell_f>\ell_b$ and $\ell_f>f$, then
$\rpfstep{f(f(b))}{\ell_b}{11}{f(f(c))}>_{rep}\rpfstep{f(a)}{\ell_f}{\epsilon}c$
but $f(f(\ell_b))\rpo<\ell_f$.
Such an extension is therefore impossible, there is no extension of
$\rpo>$ on proof terms such that for all proof terms $\pi_1,\pi_2$, we
have $\ptrsnf(\pi_1)\rpo>\ptrsnf(\pi_2)$ if and only if
$\ptrsnf(\pi_1)>_{B}\ptrsnf(\pi_2)$.
\end{cexample}
In other words, the ordering we defined above can \emph{not} be
defined as a RPO over proof terms.
\bigskip
In the following, proofs will be represented by proof terms, the proof
ordering $>$ between them will be
the ordering $>_B$ restricted to proofs with the same conclusion, and
the subproof relation $\rhd$ will be the subterm relation.
\section{Standard Completion is an Instance of Abstract Canonical System}\label{sec:csc}
\subsection{Adequacy to the Postulates}
Adequacy to postulates \ref{post:refl}, \ref{post:closure},
\ref{post:premSubproofs} and \ref{post:premMono} comes from the tree
structure of the proof terms representation.
Postulate \ref{post:replacement} is not trivially verified, because of
the definition of the ordering as translation of an ordering over
proof by replacement. Nevertheless:
\begin{theorem}[Postulate \ref{post:replacement} for Equational Proofs]
For all contexts $w[]$, for all proof terms $q,r$:
$$q>r\text{ implies } w[q]>w[r] \enspace.$$
\end{theorem}
\bigskip
The deduction mechanism $\infers$ used here will be of course the standard
completion. We now show that it has the required properties.
\subsection{Standard Completion is Sound and Adequate}
This is shown in \cite[Lemma 2.1]{Bachmair-87}: if $E,R\infers E',R'$,
then $\epfstep{}{E\cup R}*{}$ and $\epfstep{}{E'\cup R'}*{}$ are the
same. To prove this, one has simply to verify it for each inference rule of
standard completion.
\subsection{Standard Completion is Good}
This is shown in \cite[Lemma 2.5, 2.6]{Bachmair-87}: if $E,R\infers
E',R'$, then proofs in $E,R$ can be transformed to proofs in $E',R'$
using following rules:
%\newcommand{\goodrew}{\twoheadrightarrow}
$$\begin{array}{r@{~~\goodrew~~}l@{~~~~~~~~~~~~~}r}
\epfstep s{E}{}t & \rpfstep s{R'}{}t&(\Rule{Orient})\\
\epfstep s{E}{}t & \rpfstep s{R'}{}{\epfstep u{E'}{}t}&(\Rule{Simplify})\\
\epfstep s{E}{}s & s&(\Rule{Delete})\\
\lpfstep s{R}{}{\rpfstep u R{} t}& \epfstep s{E'}{}t&(\Rule{Deduce})\\
\lpfstep s{R}{}{\rpfstep u R{} t}& \rpfstep s{R'}{*}{\lpfstep v
{R'}{*} t}\\
\rpfstep s{R}{}t & \rpfstep s{R'}{}{\lpfstep v
{R'}{} t}&(\Rule{Compose})\\
\rpfstep s{R}{}t & \rpfstep s{R'}{}{\epfstep v
{E'}{} t}&(\Rule{Collapse})
\end{array}$$
We have $\rewrite[\goodrew]\subseteq >$, so these proofs become
indeed better.
\subsection{Standard Completion is Canonical}
We can now show the following theorem:
\begin{theorem}[Completeness of Standard Completion]
Standard completion results---at the limit, when it terminates
without failure---in the canonical, Church-Rosser basis.
\end{theorem}
\begin{proof}
We can show $R_\infty=E_0^\sharp$, and because standard completion is
good we can use Theorem \ref{lemma:limit_canon}.
%% Notice that because, when standard completion terminates without
%% failure, $R_\infty\setminus E_0^\sharp=\emptyset$, it is in fact
%% uniformly fair, as expected.
\end{proof}
\begin{remark}
When standard completion does not terminate, we can show that
$E_0^\sharp=R_\infty^\sharp\subseteq R_\infty$. Consequently, the
resulting set $R_\infty$ is then \emph{saturated}, but it is not
necessarily \emph{contracted}.
\end{remark}
This shows that the standard completion is an instance of the
framework of the abstract canonical systems, when we choose the
convenient proof representation.
\section{Conclusion}
We presented a proof that standard completion can be seen as an
instance of the abstract canonical systems and inference
framework. This led us to make precise the relation between different
equational proof representations. The first one, proof terms as
presented in \cite{MeseguerTCS92}, is convenient to consider proofs as
terms, with a subterm relation and substitutions. The other one,
initiated in \cite{Bachmair-87}, is well adapted to the study of the
completeness of the standard completion procedure. We presented a way
to pass from one representation to another by the mean of the proof
term rewrite rules presented in Fig.~\ref{fig:PTRS}. Thanks to this,
we extended the ordering introduced with the proof by replacement to
the proof terms and thus combine the advantages of both
representations. This therefore positively answer to the question whether the
abstract canonical systems, centered in a quite general way around the
notion of proof ordering, are indeed the right framework to uniformly
prove the completeness of completion.
We plan now to understand how the results we have presented here can be extended to other
completion procedures. Bachmair introduced another proof ordering to prove the
completeness of the completion modulo \cite{Bachmair-87}, so that the generalization seems
rather natural. We plan also to look at other kinds of deduction mechanisms, such as
Buchberger's algorithm or resolution. For this, we may show that Struth's
non-symmetric completion~\cite{Struth-PhD}, which subsumes
both procedures, is also an instance of the ACSI framework.
Furthermore, proof terms as presented by \cite{MeseguerTCS92,KirchnerKV-MIT95} are
specific terms of the rewriting calculus~\cite{rhoCalIGLP-I+II-2001}
[\url{http://rho.loria.fr}]. The link between the completion procedure and the sequent
systems mentioned above can probably be found here and be related to Dowek's work proving
that confluent rewrite rules can be linked with \Rule{Cut}-free proofs of some sequent
systems~\cite{DBLP:conf/rta/Dowek03}.
\paragraph{Acknowledgments} This paper benefited greatly from suggestions, discussions
and the enthusiasm of Nachum Dershowitz. We thank also Georg Struth for his useful comments
and the anonymous referees for their careful reading and constructive suggestions.
%
% ---- Bibliography ----
%
\bibliographystyle{myplain}
%\bibliography{/users/protheo/bibtex/abbrev,/users/protheo/bibtex/protheo,/users/protheo/bibtex/ckirchne,/users/protheo/bibtex/divers/handbookAR,../lics03/canon.bib}
\bibliography{sciacs2}
\appendix
\section{Proofs for Section \ref{sec:pr} and \ref{sec:csc}}
\subsection{From Proof Terms to Proof by Replacement}
To prove the termination of $\ptrs/\assoc$, we need a reduction
ordering compatible with associativity. We consider only
associativity here, although most of the existing works use
associativity and commutativity. Therefore, we need the following
lemma.
\begin{lemma}
If $A\subseteq B$ then $>$ is $B$-compatible implies $>$ is
$A$-compatible.
\end{lemma}
\begin{proof}
Just notice that $s'\mathop{\longleftrightarrow}\limits_A^* s > t
\mathop{\longleftrightarrow}\limits_A^* t'$ implies
$s'\mathop{\longleftrightarrow}\limits_B^* s > t
\mathop{\longleftrightarrow}\limits_B^* t'$.
\end{proof}
We can therefore use the $AC$-RPO ordering:
a total $AC$-compatible simplification ordering on ground terms is
defined in \cite{rubio95total}, as an extension of the RPO. To compare
terms, they are interpreted using flattening and interpretation rules.
As we consider here that the associative commutative symbols
have the lowest precedence, we do not need the interpretation rules,
and we will only present the flattening rules: terms are reduced using
a set of rules
\begin{equation}\label{eq:flat}f(\vect x,f(\vect[r]y),\vect[m]z)
\rightarrow f(\vect x,\vect[r]y,\vect[m]z)\end{equation} for all
$AC$-symbols $f$ with $n+m\geq 1$ and $r\geq 2$. Such a rewrite system
is terminating as shown in \cite{rubio95total}.
For all terms $t$, let $snf(t)$ denote the \Def{set of normal
forms} of $t$ using rules (\ref{eq:flat}).
Given a precedence $>$ on function symbols, let $>_{rpo}$ denote the
recursive path ordering with precedence $>$ where $AC$ function
symbols have multiset status and other symbols have lexicographic
status.
If $f(\vect s)$ is the normal form of a term $s$ rewriting by
(\ref{eq:flat}) only at topmost position, then $tf(s)\df(\vect s)$.
\begin{definition}[{\Def{$AC$-RPO}}]\label{defi:acrpo}
For all terms $s, t$, $s>_{AC-rpo} t$ if:
\begin{itemize}
\item $\forall t'\in snf(t)~\exists s'\in snf(s),~s'>_{AC-rpo}t'$
\textbf{or}
\item $\forall t'\in snf(t)~\exists s'\in snf(s),~s'\geq_{rpo}t'$
\textbf{and} $tf(s)=f(\vect[m]s)$ and $tf(t)=(\vect t)$ \textbf{and}
\begin{itemize}
\item if the head of $s$ is $AC$ then
$\lmbra\vect[m]s\rmbra\mult{>_{AC-rpo}}\lmbra\vect t\rmbra$
\textbf{or}
\item if the head of $s$ is not $AC$ then
$(\vect[m]s)\lex{>_{AC-rpo}}(\vect t)$.
\end{itemize}
\end{itemize}
\end{definition}
\begin{proposition}[\cite{rubio95total}]
The $AC$-RPO is an $AC$-compatible simplification ordering which is
total for non $AC$-equivalent ground terms.
\end{proposition}
We define a precedence $>$ such that for all function symbols $f$ and
for all rule labels $\ell$ we have $\ell>f>\cdot^{-1}>~;~$. The $AC$-RPO
built with this precedence will be noted $\succ$.
\medskip
To show termination, we also need the following lemma:
\begin{lemma}
For all proof terms $\pi:t\rewrite t'$, we have $\pi\succeq t$ and
$\pi\succeq t'$.
\end{lemma}
\begin{proof}
By induction on the structure of the proof term $\pi$.
For \Rule{Reflexivity}, $\pi=t=t'$.
For \Rule{Congruence}, $\pi=f(\vect\pi)$, $t=f(\vect t)$ and
$t'=f(\vect{t'})$. By induction hypothesis, for all
$i\in\vectset$, we have $\pi_i\succeq t_i,t'_i$. Furthermore,
$\pi$ is not reducible on the top position using rules (\ref{eq:flat}), so
that $snf(\pi)=\{f(\vect{\pi'})~:\;\forall i,\; \pi'_i\in
snf(\pi_i)\}$, whereas $t$ and $t'$ are not reducible. Consequently,
by definition of an $AC$-RPO, $\pi\succeq t,t'$.
For \Rule{Replacement}, $\pi=\ell(\vect\pi)$, $t=g(\vect t)$ and
$t'=d(\vect{t'})$ where $\ell=(g,d)\in E\cup R$. With the same
arguments than for \Rule{Congruence}, we can conclude that $\pi\succeq
t,t'$ (recall that $\ell>g,d$).
For \Rule{Transitivity}, $\pi=\pi_1;\pi_2$ where $\pi_1:t\rewrite t''$
and $\pi_2:t''\rewrite t'$. By induction hypothesis, $\pi_1\succeq t$
and $\pi_2\succeq t'$. As $\succ$ is a simplification ordering,
$\pi\succ\pi_1,\pi_2\succeq t,t'$.
For \Rule{Symmetry}, $\pi={\pi'}^{-1}$ where $\pi':t'\rewrite t$. By
induction hypothesis and because $\succ$ is a simplification ordering,
$\pi\succ\pi'\succeq t', t$.
\end{proof}
\begin{proposition}[Termination]
The rewrite system $\ptrs$ of Fig. \ref{fig:PTRS} modulo $\assoc$
is terminating for ground proof terms.
\end{proposition}
\begin{proof}
We can show that
$\ptrs\subseteq\succ$, thus proving the termination of
$\ptrs/\assoc$:
For \Rule{Delete Useless Identities}, it comes from the fact that
$\succ$ is a simplification ordering.
For \Rule{Sequentialization}, rules (\ref{eq:flat}) are not applicable
on the left side whereas they lead on the right side to
$;(f(\pi_1,t_2,\ldots,t_n),f(t'_1,\pi_2,\ldots,t_n),\ldots,
f(t'_1,t'_2,\ldots,\pi_n))$. We have $f>;$, thus by definition of a
RPO, we must then prove that for all $i\in\vectset$ we have
$f(\vect\pi)\succ_{RPO}
f(t'_1,\ldots,t'_{i-1},\pi_i,t_{i+1},\ldots,t_n)$, i.e.
$(\vect\pi)\succ_{RPO}^{lex} (
t'_1,\ldots,t'_{i-1},\pi_i,t_{i+1},\ldots,t_n)$. By hypothesis there
exists at least a $j\in\{1,\ldots,n\}\setminus\{i\}$ such that
$\pi_j\neq t_j$, so we can conclude with the preceding lemma.
For \Rule{Composition Shallowing}, both sides are not reducible using
rules (\ref{eq:flat}). We have $f>;$, thus we
have to show: $f(t_1,\ldots,\pi_i;\pi'_i,\ldots,t_n)\succ_{RPO}
f(t_1,\ldots,\pi_i,\ldots,t_n)$ and
$f(t_1,\ldots,\pi_i;\pi'_i,\ldots,t_n)\succ_{RPO}
f(t_1,\ldots,\pi'_i,\ldots,t_n)$. Both comparisons hold by definition
of a RPO.
For \Rule{Parallel Moves}, both sides are not reducible using rules
(\ref{eq:flat}). We have $\ell>;$, thus we have to prove that
$\ell(\vect\pi)\succ_{RPO}\ell(\vect t)$ and
$\ell(\vect\pi)\succ_{RPO} d(\vect\pi)$. The first comparison holds
because of the lemma and because there exists a $i\in\vectset$
such that $\pi_i\neq t_i$; the second one holds because $\ell> d$.
For \Rule{Delete Useless Inverses}, this comes from the fact that
$\succ$ is a simplification ordering.
For \Rule{Inverse Congruence}, both sides are not reducible using
rules (\ref{eq:flat}), therefore this is a consequence of
$f>\cdot^{-1}$.
For \Rule{Inverse Composition}, both sides are not reducible using
rules (\ref{eq:flat}), therefore this is a consequence of
$\cdot^{-1}>;$. \medskip
\end{proof}
We can also prove confluence:
\begin{proposition}[Confluence]
The rewrite system $\ptrs$ is confluent modulo $\assoc$
on ground proof terms.
\end{proposition}
\begin{proof}
The class rewrite system is linear and terminating, so we just have
to check that the critical pairs are confluent \cite{Huet80}.
For $\mathop{\longleftarrow}\limits_R \circ \rewrite[R]$, it is easy
to check for most of the critical pairs that they are confluent. We
only detail the most problematic one. For two possible applications
of \Rule{Sequentialization}, we have for instance
$f(g(\vect[m]\nu),\vect\pi)$ that can be rewritten to
$f(g(\vect[m]\nu),\vect t);
f(g(\vect[m]s),\pi_1,\ldots,t_n);\ldots;$\\$f(g(\vect[m]s),t'_1,\ldots,\pi_n)$
and to
$f(g(\nu_1,\ldots,s_m);\ldots;g(s'_1,\ldots,\nu_m),\vect\pi)$. Both
of them reduce to
$f(g(\nu_1,\ldots,s_m);\ldots;g(s'_1,\ldots,\nu_m),\vect t);$\\$
f(g(\vect[m]s),\pi_1,\ldots,t_n);\ldots;f(g(\vect[m]s),t'_1,\ldots,\pi_n)$.
For $\mathop{\longleftarrow}\limits_R \circ \epfstep{}A{}{}$, the
only rules that can interfere with $\assoc$ are \Rule{Delete Useless
Identities}, \Rule{Composition Shallowing} and \Rule{Inverse
Composition}. We can check that all critical pairs are confluent.
\end{proof}
\begin{theorem}[Correspondence between Proof Representations]
The normal form of a proof term $\pi$ for the rewrite system
$\ptrs$, noted $\ptrsnf(\pi)$, has the following form:
For some $n\in\mathbb N$, some contexts
$w_1[],\ldots,w_n[]$, some indices $\vect i\in\{-1,1\}$,
some rule labels $\vect\ell$ and some terms
$\vect[m_1]{t^1},\ldots,\vect[m_n]{t^n}$:
$$\ptrsnf(\pi)
=
(w_1[\ell_1(\vect[m_1]{t^1})])^{i_1};\ldots;(w_n[\ell_n(\vect[m_n]{t^n})])^{i_n}$$
where $\nu^1$ is a notation for $\nu$.
We will denote by $\ptrsnf(\pi)$ the normal form of a proof term $\pi$.
\medskip
Such a proof term correspond with the following proof by replacement
of equal by equal:
$$\upfstep[1]{w_1[g_1(\vect[m_1]{t^1})]}{\ell_1}{p_1}{\upfstep[2]{w_1[d_1(\vect[m_1]{t^1})]}{\ell_2}{p_2}\cdots}
\upfstep[n]{}{\ell_n}{p_n}{w_n[d_n(\vect[m_n]{t^n})]}$$
where for all $j\in\{1,\ldots,n\}$ we have:
\begin{itemize}
\item $\ell_j=(g_j,d_j)$,
\item $p_j$ is the position of $[]$ in $w_j[]$,
\item $\upfstep[j]{}{}{}{}=$\begin{tabular}{cl}$\rpfstep{}{}{}{}$& if $i_j=1$ and
$\ell_j\in R$,\\$\lpfstep{}{}{}{}$& if $i_j=-1$ and
$\ell_j\in R$,\\$\epfstep{}{}{}{}$& if $\ell_j\in E$.\end{tabular}
\item if $j\neq n$,
$w_j[d_j(\vect[m_j]{t^j})]=w_{j+1}[g_{j+1}(\vect[m_{j+1}]{t^{j+1}})]$.
\end{itemize}
\end{theorem}
\begin{proof}
We first have to check that proof terms in that form are indeed
irreducible by $\ptrs$, what is left to the reader.
Then, suppose that we have an irreducible proof term. Because
\Rule{Sequentialization} cannot be applied, there is at most one
$;$ under all function symbols. Because \Rule{Composition
Shallowing} cannot be applied, there are no $;$ under all function
symbols. Because \Rule{Inverse Congruence} and \Rule{Inverse
Composition} cannot be applied, $\cdot^{-1}$ is applied between $;$
and function symbols. Irreducible proof term are therefore
application of $;$ over eventually $\cdot^{-1}$ over base terms
composed of function symbols and rule labels.
Because \Rule{Delete Useless Identities} and
\Rule{Delete Useless Inverse} cannot be applied, there is a least
one non-trivial proof (i.e a proof with a label in it) in each of
these base terms. Because \Rule{Sequentialization} cannot be
applied, there is at most one non-trivial proof in each of them.
Because \Rule{Parallel Moves} cannot be applied, the subterms of
the labels are $\Sigma$-terms. Consequently, each base term contains
one and only one rule label, applied to $\Sigma$-terms.
\end{proof}
\subsection{Adequacy to the Postulates}
\paragraph{Postulate \ref{post:refl}:}
The proof of $(u,v)\in E\cup R$ labeled by $\ell$ is $\ell(\vect x)$
where $\vect x$ are the free variables of $(u,v)$.
\paragraph{Postulate \ref{post:closure}:}
We can replace the assumption $\ell(\vect\pi)$ of something proved by
its proof where the free variables are replaced by the proofs
$\vect\pi$.
\paragraph{Postulate \ref{post:premSubproofs} and \ref{post:premMono}:}
These postulates hold because of the tree structure of proofs.
\paragraph{Postulate \ref{post:replacement}:}
This one does not trivially hold.
We first show the following lemma:
\begin{lemma}\label{lemma:rep_f}
For all function symbols $f$ of arity $n+1$, for all proof terms
$\vect\pi$, $q$ and $r$:
$$q>r\text{ implies
}f(\pi_1,\ldots,q,\ldots,\pi_n)>f(\pi_1,\ldots,r,\ldots,\pi_n)\enspace. $$
\end{lemma}
\begin{proof}
Suppose $q>r$, thus by definition $\ptrsnf(q)>_{rep}\ptrsnf(r)$. To compare
$f(\pi_1,\ldots,q,\ldots,\pi_n)$ and
$f(\pi_1,\ldots,r,\ldots,\pi_n)$, we have to transform them to proof
by replacement. As $\rewrite[\ptrs/\assoc]$ is Church-Rosser, the
way it is applied does not matter.
We have
$$\begin{array}{rl}
\multicolumn{2}{l}{f(\pi_1,\ldots,q,\ldots,\pi_n)}\\
\rewrite[\ptrs]^*&
f(\pi_1,t_2,\ldots,t_n);\ldots;f(t_1',\ldots,q,\ldots,t_n);\ldots;f(t_1',\ldots,\pi_n)\\
\rewrite[\ptrs]^*&
f(\pi_1,t_2,\ldots,t_n);\ldots;{\underline{f(t_1',\ldots,\ptrsnf(q),\ldots,t_n)}};\ldots;f(t_1',\ldots,\pi_n)\\
\end{array}$$
Then, if $\ptrsnf(q)$ contains $;$ the underlined term will be split by
\Rule{Composition Shallowing}. If it contains ${}^{-1}$ the rule
\Rule{Inverse Congruence} will be applied. Some terms outside the
underline corresponding to identity will be removed by \Rule{Delete
Useless Identities}, and the normal form will look like:
$$\begin{array}{r}f(\pi_1,t_2,\ldots,t_n);\ldots;
{\underline{f(t_1',\ldots,q_1,\ldots,t_n)^{i_1};\ldots;f(t_1',\ldots,q_m,\ldots,t_n)^{i_m}}};
\ldots;\\f(t_1',\ldots,\pi_n)
\end{array}
$$ with $\ptrsnf(q)=q_1^{i_1};\ldots;q_m^{i_m}$.
The same will apply with $r$, and therefore, to compare the initial
proofs, we just have to compare the costs of the underlined terms.
The cost of $\ptrsnf(q)$ will look like $\lmbra (\lmbra s_1\rmbra, u_1,
h_1), \ldots, (\lmbra s_m\rmbra, u_m, h_m) \rmbra$. Then the cost of
$f(t_1',\ldots,q_1,\ldots,t_n)^{i_1};\ldots;f(t_1',\ldots,q_m,\ldots,t_n)^{i_m}$
will be:
$$\left\{ \begin{array}{l}(\lmbra f(t'_1,\ldots,s_1,\ldots,t_n)\rmbra, u_1,
f(t'_1,\ldots,h_1,\ldots,t_n)), \ldots,\\(\lmbra
f(t'_1,\ldots,s_m,\ldots,t_n)\rmbra, u_m,
f(t'_1,\ldots,h,m,\ldots,t_n))
\end{array}
\right\}\enspace.$$ For $\ptrsnf(r)$ they will be
respectively $\lmbra(\lmbra g_1\rmbra, v_1,
d_1), \ldots, (\lmbra g_p\rmbra, v_p, d_p) \rmbra$ and:
$$\left\{\begin{array}{l} (\lmbra f(t'_1,\ldots,g_1,\ldots,t_n)\rmbra, v_1,
f(t'_1,\ldots,d_1,\ldots,t_n)), \ldots,\\(\lmbra
f(t'_1,\ldots,g_p,\ldots,t_n)\rmbra, v_p,
f(t'_1,\ldots,d_p,\ldots,t_n))
\end{array}
\right\}\enspace.$$
$\tg$, which is used to compare the first and the third components of
each part of the cost, is a reduction ordering, so that
$\ptrsnf(q)>_{rep}\ptrsnf(r)$ implies for instance
$f(t_1',\ldots,q_1,\ldots,t_n)^{i_1};\ldots;
f(t_1',\ldots,q_m,\ldots,t_n)^{i_m}>_{rep}
f(t_1',\ldots,r_1,\ldots,t_n)^{i_1};\ldots;
f(t_1',\ldots,r_p,\ldots,t_n)^{i_p}$.
\end{proof}
The same is true for labels:
\begin{lemma}\label{lemma:rep_ell}
For all rule labels $\ell$, for all proof terms
$\vect\pi$, $q$ and $r$:
$$q>r\text{ implies
}\ell(\pi_1,\ldots,q,\ldots,\pi_n)>\ell(\pi_1,\ldots,r,\ldots,\pi_n)$$
\end{lemma}
\begin{proof}
$\ell(\pi_1,\ldots,q,\ldots,\pi_n)$ and
$\ell(\pi_1,\ldots,r,\ldots,\pi_n)$ can be reduced by \Rule{Parallel
Moves} to $\ell(\vect t); d(\pi_1,\ldots,q,\ldots,\pi_n)$ and
$\ell(\vect t); d(\pi_1,\ldots,r,\ldots,\pi_n)$. We can therefore
conclude using the preceding lemma.
\end{proof}
This allows us to show
\begin{theorem}[Postulate \ref{post:replacement} for Equational Proofs]
For all proof terms $p,r$, for all position $i$ of $p$:
$$\subterm p i>r\text{ implies } p>\replacement p r i \enspace.$$
\end{theorem}
\begin{proof}
This is proved by induction on $i$. For $i=\epsilon$ this is
trivial. For $i\neq\epsilon$, by induction hypothesis, the result
holds for the subproofs of $p$. For the head of $p$:
\begin{itemize}
\item for \Rule{Symmetry}, it is trivial;
\item for \Rule{Transitivity}, it comes from the fact that
equational proofs are compared as the multiset of their equational
proof steps;
\item for \Rule{Congruence}, it comes from lemma \ref{lemma:rep_f};
\item for \Rule{Replacement}, it comes from lemma \ref{lemma:rep_ell}.
\end{itemize}
\end{proof}
\subsection{Standard Completion is Canonical}
Remember that by fairness assumption, $E_\infty=\emptyset$.
\begin{lemma}
For all standard completion derivations $\left(E_i,R_i\right)_i$:
$$E_0^\sharp~\subseteq~ R_\infty \enspace.$$
\end{lemma}
\begin{proof}
By contradiction, suppose there is $(a,b)\in E_0^\sharp\setminus
R_\infty$, labeled $\ell$. Because completion is adequate, there
exists $p\in\mu\Pf{R_\infty}$ proving $a=b$. Because $a=b\in
E_0^\sharp$, $\ell(\vect x)\in\Nf{E_0}=\Nf{R_\infty}$ where
${(x_i)}_i$ are the free variables of $\ell$, so that
$$p > \ell(\vect x)$$
\begin{itemize}
\item
If there are no peak in $\ptrsnf(p)$, then $\ptrsnf(p)$ is a valley proof,
and it is easy to show that it is smaller than $\ell(\vect x)$, which is a
contradiction with the preceding comparison.
\item If there is a parallel peak, for instance $\lpfstep
{s[c,e]}{\ell_1}i{\rpfstep{s[d,e]}{\ell_2}j{s[d,f]}}$, then the
proof by replacement where this peak is replaced by $\rpfstep
{s[c,e]}{\ell_2}j{\lpfstep{s[c,f]}{\ell_1}i{s[d,f]}}$ is smaller,
thus leading to a contradiction with the minimality of $p$ in
$\Pf{R_\infty}$.
\item If there is a critical peak, then by fairness assumption there is
some step $k$ where this critical peak is treated by
\Rule{Deduce}. The proof of the conclusion of the critical peak
at the step $k+1$ is therefore smaller. Because standard
completion is good, it can only go smaller, so that at the limit
we can find by replacement of the critical peak by this proof a
smaller proof of $a=b$, thus leading to a contradiction with the
minimality of $p$ in $\Pf{R_\infty}$.
\end{itemize}
\end{proof}
\begin{lemma}
For all standard completion derivations $\left(E_i,R_i\right)_i$
which \emph{terminate without failure}:
$$R_\infty~\subseteq~E_0^\sharp \enspace.$$
\end{lemma}
\begin{proof}
By contradiction, suppose there is $(a,b)\in R_\infty\setminus
E_0^\sharp$, labeled by $\ell$. Then there exists a proof
$p\in\mu\Pf{E_0^\sharp}$ such that $\ell(\vect x)>p$ where $\vect x$
are the free variables of $\ell$.
Rules comes from orientation of equational axioms through \Rule{Orient},
so that $a\tg b$. The cost of $\ell(\vect x)$ is
then $\lmbra (\lmbra a\rmbra, a, b)\rmbra$. Consider the leftmost
step of $\ptrsnf(p)$. It is of the form $\upfstep a{(c,d)}i\replacement a
d i$ where $c=\subterm a i$. If it is $\lpfstep a{d\rightarrow
c}i\replacement a d i$ then the cost of this proof step would be
$\lmbra (\lmbra \replacement a d i\rmbra, d, a)\rmbra$, which is
then greater than $\lmbra (\lmbra a\rmbra, a, b)\rmbra$, thus
leading to a contradiction with the fact that $\ell(\vect x)>p$. If
$\epfstep a{c=d}i\replacement a d i$ then the cost of this proof
step would be $\lmbra (\lmbra a, \replacement a d i\rmbra, c,
\replacement a d i)\rmbra$, which is then greater than $\lmbra
(\lmbra a\rmbra, a, b)\rmbra$, thus leading to a contradiction with
the fact that $\ell(\vect x)>p$. If it is $\rpfstep a{c\rightarrow
d}i\replacement a d i$ then there is a critical pair
$(b,\replacement a d i)$ in $R_\infty$ (we just proved that
$E_0^\sharp\subseteq R_\infty$). The fairness assumption will
therefore apply, and therefore \Rule{Deduce} will produce the
equational axiom $b=\replacement a d i$, which will be oriented, and
$a\rewrite b\in R_\infty$ will be simplified through \Rule{Compose}
or \Rule{Collapse}. Because $a \rewrite b$ is persisting, it must be
generated once again, thus contradicting the termination of the completion.
\end{proof}
\begin{theorem}[Completeness of Standard Completion]
Standard completion results --- at the limit, when it terminates
without failure --- in the canonical, Church-Rosser basis.
\end{theorem}
\begin{proof}
There is nothing more to prove, because we have
$R_\infty=E_0^\sharp$, and standard completion is good so we can use
Theorem \ref{lemma:limit_canon}.
\end{proof}
\end{document}