JAIST Repository
https://dspace.jaist.ac.jp/

Title

A New and Formalized Proof of Abstract Completion

Author(s)Hirokawa, Nao; Middeldorp, Aart; Sternagel,
Christian

Citation

Lecture Notes in Computer Science, 8558: 292‑307

Issue Date

2014‑07

Type

Journal Article

Text version

author

URL

http://hdl.handle.net/10119/12800

RightsThis is the author‑created version of Springer,
Nao Hirokawa, Aart Middeldorp, and Christian
Sternagel, Lecture Notes in Computer Science,
8558, 2014, 292‑307. The original publication isavailable at www.springerlink.com,
http://dx.doi.org/10.1007/978‑3‑319‑08970‑6̲19

Description

5th International Conference, ITP 2014, Held as
Part of the Vienna Summer of Logic, VSL 2014,
Vienna, Austria, July 14‑17, 2014.

Japan Advanced Institute of Science and Technology

A New and Formalized Proof of Abstract
Completion?
Nao Hirokawa1 , Aart Middeldorp2 , and Christian Sternagel2
1

JAIST, Japan hirokawa@jaist.ac.jp
2
University of Innsbruck, Austria{aart.middeldorp|christian.sternagel}@uibk.ac.at

Abstract. Completion is one of the most studied techniques in term
rewriting. We present a new proof of the correctness of abstract completion that is based on peak decreasingness, a special case of decreasing
diagrams. Peak decreasingness replaces Newman’s Lemma and allows us
to avoid proof orders in the correctness proof of completion. As a result,our proof is simpler than the one presented in textbooks, which is confirmed by our Isabelle/HOL formalization. Furthermore, we show thatcritical pair criteria are easily incorporated in our setting.

1

Introduction

Knuth and Bendix’ completion procedure [11] is a landmark result in term rewriting. Given an equational system E and a reduction order, the completion procedure aims to construct a complete (terminating and confluent) term rewrite
system that is equivalent to E, thereby providing a general solution to the validity problem. Completion has had significant impact on various areas of computerscience, in particular automated theorem proving.
The completion process is non-trivial and showing its correctness is a challenge [8]. Bachmair, Dershowitz, and Hsiang [4] introduced abstract inference
rules that capture the essence of completion and introduced a new proof technique based on proof orders and persistent sets. This became the de facto standard and has been adopted in textbooks on term rewriting [1,17]. Very recently,
this proof was further simplified for finite runs and formalized in Isabelle/HOL
by Sternagel and Thiemann [16]. Still, we do not hesitate to point to the intricacy of these proofs, especially when practical critical pair criteria [2,3] areincorporated in completion.
Contribution. In this paper we present a new and formalized correctness proofof abstract completion for finite runs. We introduce a new confluence criterion
for abstract rewriting, which we name peak decreasingness, allowing us to abstract from proof orders in order to obtain a simple and elementary proof of the?

Supported by JSPS KAKENHI Grant Number 25730004 and the Austrian Science
Fund (FWF) projects I963 and J3202.

correctness of completion. Moreover the proof incorporates a critical pair criterion: it suffices to consider prime critical pairs. Our formalization was conductedusing Isabelle/HOL [12].
Formalization. Our formalization is available as part of IsaFoR (an Isabelle/HOL
formalization of rewriting) version 2.14.3 To have a look at the actual formalization visit IsaFoR’s website and follow the link Mercurial repository under Downloads. Alternatively you can download the provided *.tgz file. Eitherway, all the relevant theory files are to be found in the subdirectory IsaFoR/.
The content of this paper comprises the following theory files: Renaming formalizes permutations and permutation types, and proves useful facts about
them; Renaming_Interpretations gives permutation type instances for terms,
rules, substitutions, TRSs, etc., i.e., allows us to apply permutations to them;
Peak_Decreasingness defines labeled conversions and peak decreasingness, andcontains the proof that the latter implies confluence; CP defines overlaps, criticalpeaks, and critical pairs, and proves the critical pair lemma as well as the factthat for finite TRSs only finitely many representatives of critical pairs have to
be considered; Prime_Critical_Pairs defines prime critical pairs and proves animportant result about peaks that allows us to restrict to prime critical pairs forfairness; Abstract_Completion defines the inference rules of abstract completion, and proves their soundness; finally Completion_Fairness proves soundnessof abstract completion when restricting fairness to prime critical pairs. For the
benefit of a general audience we present all the proofs in the following on a highlevel and using standard mathematical notation. Nevertheless the proofs are exactly along the lines of our formalization and from time to time we sprinkle thetext with comments directed at Isabelle initiates. But those are not essential forunderstanding.
Organization. The remainder of the paper is organized as follows. In the next
section we recall some rewriting preliminaries. In Section 3 we discuss our formalization of variable renamings. Peak decreasingness is introduced in Section 4.
The critical pair lemma, or rather: a formalized critical peak lemma, is the subject of Section 5. Our new correctness proof for abstract completion is presented
in full detail in Section 6. Related work is discussed in Section 7 before weconclude in Section 8.

2

Preliminaries

We assume familiarity with term rewriting and all that (e.g., [1]) and only shortly
recall notions that are used in the following. An abstract rewrite system (ARS
for short) A is a set A, also called the carrier, equipped with a binary relation→. Sometimes we partition the binary relation into parts according to a set I of
indices (or labels). Then we write A = hA, {→α }S
α∈I i where we denote the partof the relation with label α by →α , i.e., → = α∈I →α . In our formalization3

http://cl-informatik.uibk.ac.at/software/ceta

2

ARSs are just relations which are represented by sets of pairs in Isabelle/HOL,
i.e., of type (α × α) set, and their carrier is given implicitly by the type α.
Terms are defined inductively as follows: a term is either a variable x from theset V or is constructed by applying a function symbol f ∈ F to a list of argument
terms f (t1 , . . . , tn ). Here F is called the signature. The set of all terms built over
F and V is denoted by T (F, V). In our formalization terms are represented by
the datatype
datatype (α, β) term = Var β | Fun α ((α, β) term list)that is, the signature as well as the set of variables is given implicitly by the typeparameters α and β, respectively. The set of variables of a term t is denoted byVar(t) (this is easily extended to rules, term rewrite systems, etc.). Positions
are finite lists of positive natural numbers where the empty position (or root
position) is denoted by . The set of positions of a term t is denoted by Pos(t) andpartitioned into function positions PosF and variable positions PosV . Positions
are partially ordered by the prefix order, i.e., p 6 q if p is a prefix of q (wealso say that p is above q). Two positions p and q for which neither p 6 q nor
q 6 p are called parallel, denoted by p k q. Whenever p 6 q, by q \ p we denoteposition q without its prefix p. The subterm of t at position p is denoted by t|p
and replacing this term by s is denoted by t[s]p .
A substitution is a mapping σ from variables to terms such that its domain{x ∈ V | σ(x) 6= x} is finite. Applying a substitution to a term is written tσ.
A pair of terms (s, t) is sometimes considered an equation, then we writes ≈ t, and sometimes a (rewrite) rule, then we write s → t. In the latter case
we assume that the left-hand side is not a variable and that the variables of theright-hand side t are all contained in the left-hand side s. This assumption wecall the variable condition.
A set E of equations is called an equational system (ES for short) and a set
R of rules a term rewrite system (TRS for short). In the following we assume
the variable condition for all rules of a TRS. Sets of pairs of terms induce arewrite relation by closing their components under contexts and substitutions.
More precisely the rewrite relation of R, denoted by →R , is defined inductively
by s →R t whenever there are a rule ` → r ∈ R, a position p, and a substitution
σ such that s|p = `σ and t = s[rσ]p . In the following we sometimes drop R
in →R if it is clear from the context. Moreover, individual steps are sometimes
annotated with additional information (the employed rule, the corresponding
position, etc.).
A binary relation → is well-founded (or terminating) if it does not admit
any infinite descending sequence a1 → a2 → a3 → · · · . A well-founded orderthat is closed under contexts and substitutions is called a reduction order. Thus
a reduction order that strictly orients all rules of a TRS establishes terminationof the induced rewrite relation.
3

3

Renaming Variables

This section is not essential for understanding the remainder of the paper. However, it addresses a typical problem that arises when formalizing proofs involving
variable renaming. Thus it is mostly interesting for users of proof assistants.
One thing that is often neglected or treated implicitly in paper proofs isrenaming of variables, which is often necessary to make sure that two given
objects do not contain any common variables. While on the one hand, this isclearly not good enough for a formalization using a proof assistant; on the other
hand, a thorough treatment quickly leads to tedious reasoning (which is typicallyleft as an exercise in textbooks; see for example the proof of the statement that
two most general unifiers only differ by a renaming in [17, Chapter 2] and [1,Chapter 4]).
We aim for a setup that allows us to argue along the lines of a paper proof
also in its formalization. The advantage of doing so is that not only the result iscertified to be correct, but also the proof itself. Moreover, simulating the implicit
reasoning used in a paper proof should be as painless as possible.
To this end it turns out that a slight modification of a previous Isabelle/HOL
formalization of permutations and permutation types by Urban et al. [9,18] isvery useful. Here a permutation (also called renaming) is just a bijective function
f such that {x | f (x) 6= x} is finite, and a permutation type is a type whose
elements support applying a permutation to them. The mentioned modificationconsists in parameterizing permutation types over the type of atoms (which wecall variables in the following) in addition to the type of elements (which may beterms, substitutions, rules, TRSs, etc.) To make this possible we have to switchfrom Isabelle’s type classes to locales and therefore to reformalize a theory of
permutations (thankfully, most proofs are not much different from the type classversion). Moreover many useful results only hold under the assumption that wehave an infinite set of variables, e.g., that we can always rename the variables of
two finite objects apart. This we express in Isabelle by demanding that the typeof variables is in the type class infinite (whose only assumption says that theuniverse of all values of the corresponding type be infinite). Permutation types
are expressed as follows in Isabelle (see theory Renaming):
locale pt =fixes · :: (α :: infinite) perm ⇒ β ⇒ βassumes id · x = x and (π1 ◦ π2 ) · x = π1 · (π2 · x)
where id is the empty permutation, ◦ denotes function composition, and π · xdenotes applying the renaming π to the element x. Also note that α :: infinite
requires the type α to contain infinitely many elements. Associated with each
permutation type is the notion of support. Since we will not give any moredetails about permutation types, suffice it to say that for permutation types
whose elements have finite support, this notion corresponds to the set of freevariables.
The most important result about finitely supported permutation types forour purposes is that we can always find a permutation π which makes the support4

of x disjoint from a given finite set of variables. Intuitively, this means that we
can always rename variables apart.
After a general theory of renamings we have to create concrete instances forterms, rules, substitutions, TRSs, etc. (see theory Renaming_Interpretations).
Using this machinery we have formalized the following results (the interested
reader is referred to the formalization for proofs).
Lemma 1. Let σ and τ be substitutions.4
1. If σ 0 and τ 0 are substitutions with σσ 0 = τ and τ τ 0 = σ then there is arenaming π such that π · σ = τ .
2. If σ and τ are two most general unifiers of a set of equations, then they arevariants of each other.
In the remainder, whenever we say that a term t is a variant of a term u,
what we formally mean is that there is a permutation π such that π · t = u. Of
course, this also works for rules, substitutions, TRSs, etc.

4Peak Decreasingness

In this section we present the abstract result that replaces Newman’s Lemma inthe proof of the correctness of abstract completion.
Definition 2. An ARS A = hA, {→α }α∈I i is peak decreasing if there exists awell-founded order > on I such that for all α, β ∈ I the inclusion∗α ← · →β⊆ ←−−→∨αβ

holds. Here ∨αβ denotes the set {γ ∈ I | α > γ or β > γ} and if J ⊆ I then −→J∗denotes the union of all −→ with γ ∈ J and ←→ denotes a conversion consistingγJof −→ steps.
J

Peak decreasingness is a special case of decreasing diagrams [13], which is
known as a powerful confluence criterion. Correctness of decreasing diagramshas been formally verified in Isabelle/HOL by Zankl [20] and it should in principle be possible to obtain our results on peak decreasingness as a special case.
However, for the sake of simplicity we present its easy direct proof (which we
also formalized in order to verify its correctness). We denote by M(J) the setof all multisets over a set J.
Lemma 3. Every peak decreasing ARS is confluent.
Proof. Let > be a well-founded order on I which shows that the ARS A =hA, {→α }α∈I i is peak decreasing. With every conversion C in A we associate themultiset MC consisting of the labels of its steps. These multisets are comparedby the multiset extension >mul of >, which is a well-founded order on M(I).
4

Finiteness of substitution domains is used (only) for this lemma (in this paper).

5

We prove ↔∗ ⊆ ↓ by well-founded induction on >mul . Consider a conversion C
between a and b. We either have a ↓ b or a ↔∗ · ← · → · ↔∗ b. In the former case
we are done. In the latter case there exist labels α, β ∈ I and multisets Γ1 , Γ2 ∈M(I) such that MC = Γ1 ] {α, β} ] Γ2 . By the peak decreasingness assumption
there exists a conversion C 0 between a and b such that MC 0 = Γ1 ] Γ ] Γ2 with
Γ ∈ M(∨αβ). We obviously have {α, β} >mul Γ and hence MC >mul MC 0 . We
obtain a ↓ b from the induction hypothesis.
tuWhat we informally state as with every conversion we associate the multisetof the labels of its steps in the proof above is formalized as an inductive predicate defined by the rules
α∈I
a
{} a

α

a←
→b
b
M c
a
M ]{α} c

together with the fact that for all a and b, we have a ↔∗ b if and only if there
is a multiset M such that a M b. (This predicate is called conv in theory
Peak_Decreasingness.)

5

Critical Pair Lemma

Completion is based on critical pair analysis. In this section we present a versionof the critical pair lemma that incorporates primality. The correctness proof isbased on peak decreasingness.
Definition 4. An overlap of a TRS R is a triple h`1 → r1 , p, `2 → r2 i satisfying
the following properties:– there are renamings π1 and π2 such that π1 · (`1 → r1 ), π2 · (`2 → r2 ) ∈ R,
– Var(`1 → r1 ) ∩ Var(`2 → r2 ) = ∅,– p ∈ PosF (`2 ),– `1 and `2 |p are unifiable,– if p =  then `1 → r1 and `2 → r2 are not variants.
In general this definition may lead to an infinite set of overlaps, since there
are infinitely many possibilities of taking variable disjoint variants of rules. Fortunately it can be shown (and has been formalized) that overlaps that originate
from the same two rules are variants of each other (see theory CP). Overlaps giverise to critical peaks and pairs.
Definition 5. Suppose h`1 → r1 , p, `2 → r2 i is an overlap of a TRS R. Let σ bea most general unifier of `1 and `2 |p . The term `2 σ[`1 σ]p = l2 σ can be reduced
in two different ways:`2 σ[`1 σ]p = `2 σ
` 1 → r1

` 2 → r2
p



r2 σ

`2 σ[r1 σ]p

6

We call the quadruple (`2 σ[r1 σ]p , p, `2 σ, r2 σ) a critical peak and the equation`2 σ[r1 σ]p ≈ r2 σ a critical pair of R, obtained from the overlap. The set of all
critical pairs of R is denoted by CP(R).
In our formalization we do not use an arbitrary most general unifier in theabove definition. Instead we use the most general unifier that is computed by
the formalized unification algorithm that is part of IsaFoR (thereby removing one
degree of freedom and making it easier to show that only finitely many criticalpairs have to be considered for finite TRSs).
p
A critical peak (t, p, s, u) is usually denoted by t ←−s→− u. It can be shown(and has been formalized) that different critical peaks and pairs obtained fromtwo variants of the same overlap are variants of each other. Since rewriting isequivariant under permutations, it is enough to consult finitely many criticalpairs or peaks for finite TRSs (one for each pair of rules and each appropriate
position) in order to conclude rewriting related properties (like joinability or
fairness, see below) for all of them.
We present a variation of the well-known critical pair lemma for critical peaks
and its formalized proof. The slightly cumbersome statement is essential to avoid
gaps in the proof of Lemma 9 below.
p1

p2

Lemma 6. Let R be a TRS. If t R ←− s −→R u then one of the following holds:(a) t ↓R u,
p1 \p2p2 \p1(b) p2 6 p1 and t|p2 ←−−− s|p2 →− u|p2 is an instance of a critical peak,(c) p1 6 p2 and u|p1 ←−−− s|p1 →− t|p1 is an instance of a critical peak.
Proof. Consider an arbitrary peak t p1 ,`01 →r10 ,σ10 ← s →p2 ,`2 →r2 ,σ2 u. If p1 k p2
then t →p2 ,`2 →r2 ,σ2 t[r2 σ2 ]p2 = u[r10 σ10 ]p1 p1 ,`01 →r10 ,σ10 ← u. If the positions of thecontracted redexes are not parallel then one of them is above the other. Without
loss of generality we assume that p1 > p2 . Let p = p1 \ p2 . Moreover, let π be a
permutation such that `1 → r1 = π · (`01 → r10 ) and `2 → r2 have no variables
in common. Such a permutation exists since we only have to avoid the finitely
many variables of `2 → r2 and assume an infinite set of variables. Furthermore,let σ1 = π −1 · σ10 . We have t = s[r1 σ1 ]p1 = s[`2 σ2 [r1 σ1 ]p ]p2 and u = s[r2 σ2 ]p2 .
We consider two cases depending on whether p ∈ PosF (`2 ) in conjunction withthe fact that whenever p =  then `1 → r1 and `2 → r2 are not variants, is trueor not.
– Suppose p ∈ PosF (`2 ) and p =  implies that `1 → r1 and `2 → r2 are
not variants. Let σ 0 (x) = σ1 (x) for x ∈ Var(`1 → r1 ) and σ 0 (x) = σ2 (x),otherwise. The substitution σ 0 is a unifier of `2 |p and `1 : (`2 |p )σ 0 = (`2 σ2 )|p =`1 σ1 = `1 σ 0 . Then h`1 → r1 , p, `2 → r2 i is an overlap. Let σ be a most generalpunifier of `2 |p and `1 . Hence `2 σ[r1 σ]p ←− `2 σ →− r2 σ is a critical peak andthere exists a substitution τ such that σ 0 = στ . Thereforep

`2 σ2 [r1 σ1 ]p = (`2 σ[r1 σ]p )τ ←− (`2 σ)τ →− (r2 σ)τ = r2 σ2
and thus (b) is obtained.
7

– Otherwise, either p =  and `1 → r1 , `2 → r2 are variants, or p ∈/ PosF (`2 ).
In the former case it is easy to show that r1 σ1 = r2 σ2 and hence t = u. In thelatter case, there exist positions q1 , q2 such that p = q1 q2 and q1 ∈ PosV (`2 ).
Let `2 |q1 be the variable x. We have σ2 (x)|q2 = `1 σ1 . Define the substitution
σ20 as follows:(
σ2 (y)[r1 σ1 ]q2 if y = x0σ2 (y) =σ2 (y)
if y 6= x
Clearly σ2 (x) →R σ20 (x), and thus r2 σ2 →∗ r2 σ20 . We also have`2 σ2 [r1 σ1 ]p = `2 σ2 [σ20 (x)]q1 →∗ `2 σ20 → r2 σ20
Consequently, t →∗ s[r2 σ20 ]p2 ∗ ← u. Hence, (c) is concluded.

tu

An easy consequence of the above lemma is that for every peak t R ← s →R u
we have t ↓R u or t ↔CP(R) u. It might be interesting to note that in ourformalization of the above proof we do actually not need the fact that left-handsides of rules are not variables.
pDefinition 7. A critical peak t ←−s→− u is prime if all proper subterms of s|p
are in normal form. A critical pair is called prime if it is derived from a prime
critical peak. We write PCP(R) to denote the set of all prime critical pairs of a
TRS R.
Below we prove that non-prime critical pairs need not be computed. In the
proof we use a new ternary relation on terms. It expresses the condition underwhich a conversion between two terms is considered harmless (when it comes toproving confluence of terminating TRSs). This relation is also used in the newcorrectness proof of abstract completion that we present in the next section.
Definition 8. Given a TRS R and terms s, t, and u, we write t Os u if s →+
R t,
s →+
u,
and
t
↓
u
or
t
↔
u.
PCP(R)
RRp

Lemma 9. Let R be a TRS. If t ←−s→− u is a critical peak then t Os2 u.
Proof. First suppose that all proper subterms of s|p are in normal form. Thent ≈ u ∈ PCP(R) and thus t Os u. Since also u Os u, we obtain the desired t Os2 u.
This leaves us with the case that there is a proper subterm of s|p that is not
in normal form. By considering an innermost redex in s|p we obtain a positionqq > p and a term v such that s −→ v and all proper subterms of s|q are in normalq
form. Now, if v ←−s→− u is an instance of a critical peak then v →PCP(R) u.
Otherwise, v ↓R u by Lemma 6, since q 66 . In both cases we obtain v Os u.
pqFinally, we analyze the peak t ←−s−→ v by another application of Lemma 6.
1. If t ↓R v, we obtain t Os v and thus t Os2 u, since also v Os u.
q\p
2. Since p < q, only the case that v|p ←−− s|p →− t|p is an instance of a criticalpeak remains. Moreover, all proper subterms of s|q are in normal form andthus we have an instance of a prime critical peak. Hence t ↔PCP(R) v andtogether with v Os u we conclude t Os2 u.
tu
8Corollary 10. Let R be a TRS. If t R ← s →R u then t Os2 u.
Proof. From Lemma 6, either t ↓R u and we are done, or t R ← s →R u containsa (possibly reversed) instance of a critical peak. By Lemma 9 we conclude theproof, since rewriting is closed under substitutions and contexts.
tu
The following result is due to Kapur et al. [10, Corollary 4].
Corollary 11. A terminating TRS is confluent if and only if all its prime critical pairs are joinable.
Proof. Let R be a terminating TRS such that PCP(R) ⊆ ↓R . We label rewrite
steps by their starting term and we claim that R is peak decreasing. As wellfounded order we take > = →+R . Consider an arbitrary peak t R ← s →R u.
Lemma 10 yields a term v such that t Os v Os u. From the assumption PCP(R) ⊆↓R we obtain t ↓R v ↓R u. Since s →+R v, all steps in the conversion t ↓R v ↓R u
are labeled with a term that is smaller than s. Since the two steps in the peakreceive the same label s, peak decreasingness is established and hence we obtainthe confluence of R from Lemma 3. The reverse direction is trivial.
tuNote that unlike for ordinary critical pairs, joinability of prime critical pairs
does not imply local confluence.
Example 12. Consider the following TRS R:
f(a) → b

f(a) → ca→a

The set PCP(R) consists of the pairs f(a) ≈ b and f(a) ≈ c, which are triviallyjoinable. But R is not locally confluent because the peak b R ← f(a) →R c is notjoinable.

6

Abstract Completion

The abstract completion procedure for which we give a new and formalized
correctness proof is presented in the following definition.
Definition 13. The inference system KB operates on pairs consisting of an ES
E and a TRS R over a common signature F. It consists of the following six
inference rules:
deduceorientdeleteE, R
if s R ← · →R t
E ∪ {s ≈ t}, R

composeE ] {s ≈ t}, R
if s > t
E, R ∪ {s → t}

simplify

E ] {s ≈ t}, R
if t > s
E, R ∪ {t → s}
E ] {s ≈ s}, R
E, R

collapse

9

E, R ] {s → t}
if t →R u
E, R ∪ {s → u}
E ] {s ≈ t}, R
if s →R u
E ∪ {u ≈ t}, R
E ] {s ≈ t}, R
if t →R u
E ∪ {s ≈ u}, R
E, R ] {t → s}
if t →R u
E ∪ {u ≈ s}, R

Here > is a fixed reduction order on T (F, V).
Inference rules for completion were introduced by Bachmair, Dershowitz, andHsiang in [4]. The version above differs from most of the inference systems in theliterature (e.g. [2,3]) in that we do not impose any encompassment restriction incollapse. The reason is that only finite runs will be considered here (cf. [16]).
We write (E, R) for the pair E, R when it increases readability. We write(E, R) `KB (E 0 , R0 ) if (E 0 , R0 ) can be obtained from (E, R) by applying one of
the inference rules of Definition 13.
According to the following lemma the equational theory induced by E ∪ R is
not affected by application of the inference rules of KB. This is well-known, but
our formulation is new and paves the way for a simple correctness proof.
Lemma 14. Suppose (E, R) `KB (E 0 , R0 ).
=

=

=

R

E ∪R

R

1. If s −−−→ t then s −−→· −−0−−→
· ←−−
t.
0
0
0
E∪R

∗

t then s ←−−→ t.
2. If s −−0−−→
0
E∪R

E ∪R

Proof. By inspecting the inference rules of KB we easily obtain the following
inclusions:deduceE ∪ R ⊆ E 0 ∪ R0
orientE ∪ R ⊆ E 0 ∪ R0 ∪ (R0 )−1deleteE ∪ R ⊆ E 0 ∪ R0 ∪ =compose· ←−−E ∪ R ⊆ E 0 ∪ R0 ∪ −−→R0R0
simplify
E ∪ R ⊆ E 0 ∪ R0 ∪ −−→
· −→
∪ −→
· ←−−
R0
E0
E0
R0
collapseE ∪ R ⊆ E 0 ∪ R0 ∪ −−→
· −→
0
0
R

E

E 0 ∪ R0 ⊆ E ∪ R ∪ ←− · −→RR

E 0 ∪ R0 ⊆ E ∪ R ∪ E −1
E 0 ∪ R0 ⊆ E ∪ R
E 0 ∪ R0 ⊆ E ∪ R ∪ −→ · −→
R

0

0

0

0

R

E ∪ R ⊆ E ∪ R ∪ ←− · −→∪−→ · −→
RE

E

R

E ∪ R ⊆ E ∪ R ∪ ←− · −→R

R

Consider for instance the collapse rule and suppose that s ≈ t ∈ E ∪ R. If
s ≈ t ∈ E then s ≈ t ∈ E 0 because E ⊆ E 0 . If s ≈ t ∈ R then either s ≈ t ∈ R0
or s →R u with u ≈ t ∈ E 0 and thus s →R0 · →E 0 t. This proves the inclusionon the left. For the inclusion on the right the reasoning is similar. Suppose thats ≈ t ∈ E 0 ∪ R0 . If s ≈ t ∈ R0 then s ≈ t ∈ R because R0 ⊆ R. If s ≈ t ∈ E 0
then either s ≈ t ∈ E or there exists a rule u → t ∈ R with u →R s and thuss R ← · →R t.
Since rewrite relations are closed under contexts and substitutions, the inclusions in the right column prove statement (2). Because each inclusion in theleft column is a special case of
=

=

=

R

E ∪R

R

E ∪ R ⊆ −−→· −−0−−→
· ←−−
0
0
0
also statement (1) follows from the closure under contexts and substitutions ofrewrite relations.
t
u
10

∗

∗

E∪R

E ∪R

Corollary 15. If (E, R) `∗KB (E 0 , R0 ) then ←−−→ = ←−0−−→
.
0

t
u

The next lemma states that termination of R is preserved by applications of
the inference rules of KB. It is the final result in this section whose proof refers
to the inference rules.
Lemma 16. If (E, R) `∗KB (E 0 , R0 ) and R ⊆ > then R0 ⊆ >.
Proof. We consider a single step (E, R) `KB (E 0 , R0 ). The statement of the lemma
follows by a straightforward induction proof. Observe that deduce, delete, andsimplify do not change the set of rewrite rules and hence R0 = R ⊆ >. For collapse
we have R0 ( R ⊆ >. In the case of orient we have R0 = R ∪ {s → t} withs > t and hence R0 ⊆ > follows from the assumption R ⊆ >. Finally, consider
an application of compose. So R = R00 ] {s → t} and R0 = R00 ∪ {s → u} witht →R u. We obtain s > t from the assumption R ⊆ >. Since > is a reduction
order, t > u follows from t →R u. Transitivity of > yields s > u and hence
R0 ⊆ > as desired.
tu
To guarantee that the result of a finite KB derivation is a complete TRS
equivalent to the initial E, KB derivations must satisfy the fairness condition
defined below. Fairness requires that prime critical pairs of the final TRS Rn
which were not considered during the run are joinable in Rn .
Definition 17. A run for a given ES E is a finite sequence
E0 , R0 `KB E1 , R1 `KB · · · `KB En , Rnsuch that E0 = E and R0 = ∅. The run fails if En 6= ∅. The run is fair ifn[

PCP(Rn ) ⊆ ↓Rn ∪

↔Ei

i=0

The reason for writing ↔Ei instead of Ei in the definition of fairness is thatcritical pairs are ordered, so in a fair run a (prime) critical pair s ≈ t of Rn may
be ignored by deduce if t ≈ s was generated, or more generally, if s ↔Ei t holds
at some point in the run. Non-prime critical pairs can always be ignored.
According to the main result of this section (Theorem 20), a completion
procedure that produces fair runs is correct. The challenge is the confluence
proof of Rn . We show that Rn is peak decreasing by labeling rewrite steps (notonly in Rn ) with multisets of terms. As well-founded order on these multisets
we take the multiset extension of >.
Definition 18. Let → be a rewrite relation and M a finite multiset of terms.
M
We write s −→ t if s → t and there exist terms s0 , t0 ∈ M such that s0 > s and0t > t. Here > denotes the reflexive closure of the given reduction order >.
M

M

E∪R

E ∪R

∗
Lemma 19. Let (E, R) `KB (E 0 , R0 ). If s ←−−→∗ t and R0 ⊆ > then s ←−0−−→
t.
0

11

Proof. We consider a single (E ∪ R)-step from s to t. The statement of thelemma follows then by induction on the length of the conversion between s andt. According to Lemma 14(1) there exist terms u and v such that
=

=

=

R

E ∪R

R

s −−→
u −−0−−→
v ←−−
t
0
0
0
We claim that the (non-empty) steps can be labeled by M . There exist terms
s0 , t0 ∈ M with s0 > s and t0 > t. Since R0 ⊆ >, s > u and t > v and thus alsos0 > u and t0 > v. Hence
M

M

M

R

E ∪R

R

=
=
s −−→
u −−0−−→
v = ←−−
t
0
0
0
M

∗
and thus also s ←−0−−→
t.
0

t
u

E ∪R

After these preliminaries we are ready for the main result of this section. A
TRS R is called a representation of an ES E if ↔∗R and ↔∗E coincide.
Theorem 20. For every fair non-failing run γ
E0 , R0 `KB E1 , R1 `KB · · · `KB En , Rn
the TRS Rn is a complete representation of E.
Proof. We have En = ∅. From Corollary 15 we know that ↔∗E = ↔∗Rn . Lemma 16
yields Rn ⊆ > and hence Rn is terminating. It remains to prove that Rn is
confluent. Let
M1
M2
t ←−−
s −−→
u
Rn

Rn

From Lemma 10 we obtain t Os2 u. Let v Os w appear in this sequence (so t = v
or w = u). We obtain(v, w) ∈ ↓Rn ∪

n
[

↔Ei

i=0

from the definition of Os and fairness of γ. We label all steps between v and w
with the multiset {v, w}. Because s > v and s > w we have M1 >mul {v, w}
and M2 >mul {v, w}. Hence by repeated applications of Lemma 19 we obtain aconversion in Rn between v and w in which each step is labeled with a multisetthat is smaller than both M1 and M2 . It follows that Rn is peak decreasing. tuA completion procedure is a program that generates KB runs. In order toensure that the final outcome Rn is a complete representation of the initial ES,
fair runs should be produced. Fairness requires that prime critical pairs of Rn
are considered during the run. Of course, Rn is not known during the run, so
to be on the safe side, prime critical pairs of any R that appears during the run
should be generated by deduce. (If a critical pair is generated from a rewrite
rule that disappears at a later stage, it can be safely deleted from the run.) In
particular, there is no need to deduce equations that are not prime critical pairs.
So we may strengthen the condition s R ← · →R t of deduce to s ≈ t ∈ PCP(R)without affecting Theorem 20.
12

7

Related Work

Formalizations of the Critical Pair Lemma. There is previous work on formalizing the Critical Pair Lemma. The first such formalization that we are aware of isby Ruiz-Reina et al. in ACL2 [15]. Details of the formalization are not presented
in the paper, however, the authors state the following:
The main proof effort was done to handle noncritical (or variable) overlaps. It is interesting to point out that in most textbooks and surveys
this case is proved pictorially. Nevertheless, in our mechanical proof [it]turns out to be the most difficult part and it even requires the design ofan induction scheme not discovered by the heuristics of the prover.
In contrast our proof of Lemma 6 handles the variable overlap case rigorously
but still without excessive complexity (also in the formalization).
Another formalization of the Critical Pair Lemma was conducted by Galdino
and Ayala-Rincón in PVS [7]. Here renamings are handled as substitutions satisfying further restrictions. While this was also our first approach in our own
formalization, it leads to rather cumbersome proof obligations where basicallythe same kind of proofs have to be done for every object that we want to permute, i.e., terms, rules, substitutions, TRSs, etc. Most of those obligations canbe handled in the abstract setting of permutation types once and for all and thus
freely carry over to any concrete instance. Moreover the obtained set of criticalpairs is infinite but there is no formalized proof that it suffices to look at only
finitely many representatives for finite TRSs.
The latest formalization of the Critical Pair Lemma we are aware of is by
Sternagel and Thiemann in Isabelle/HOL [16]. It consists of a rather involved
proof. Moreover, it is restricted to strings and relies on concrete renaming functions. Thus it is not so convenient to use in an abstract setting. A big advantage,
however, is that this formalization is executable and the obtained set of criticalpairs is finite (for finite TRSs) by construction. The good news is that it should
be possible to prove the soundness of the same executable function also via ourabstract formalization, which would combine the advantages of executability andan abstract theory.
Soundness of Completion. Bachmair et al. [4] consider an infinite fair run tocharacterize the output system as the pair (E∞ , R∞ ) of the persistent sets:
[ \
[ \
E∞ =
Ei
R∞ =
Ri
i>0 j>ii>0 j>iWhen proving confluence of R∞ , conversions s1 ↔ · · · ↔ sn in E∞ ∪ R∞ arecompared by comparing the corresponding multisets{cost(si , si+1 ) | i < n}using the proof order given by (>mul , B,
>)
.
Here
the function cost is·lex muldefined as({s, t}, –, –) if s ↔E∞ t
cost(s, t) = ({s}, `, t)
if s →R∞ t({t}, `, s)
if t →R∞ s
13Table 1. Comparison between existing Isabelle/HOL formalizations

renaming (+ interpretations)peak decreasingness
critical peak/pair lemmasoundness of completion
longest proof
soundness with PCPs

∼ LoI new

∼ LoI [16]

2000
400
300
600
80
120

–
–
300
1600
900
–

where – is an arbitrary fixed element. Whenever a conversion contains a local
peak, one can find a conversion that is smaller in the proof order. In this way
confluence is obtained.
Sternagel and Thiemann [16] observed that the encompassment restriction in
the collapse inference rule is unnecessary for finite runs. Based on this observation
they simplified the cost function (for runs of length n) to({s, t}, –)cost(s, t) = ({s}, n − o(` → r))({t}, n − o(` → r))

if s ↔E∞ t
if s →`→r t and ` → r ∈ R∞
if t →`→r s and ` → r ∈ R∞

where o(` → r) denotes the highest i 6 n such that ` → r ∈ Ri . The proof
order is (>mul , >N )lex mul . In our new proof the second ingredient of the cost is
replaced by mathematical induction in Lemma 19, and the proof order is hidden
behind the abstract notion of peak decreasingness.
For a more detailed comparison between our current formalization and theone of Sternagel and Thiemann consult Table 1, where we compare Lines ofIsabelle code (LoI for short). A general theory of renamings (plus special instances for terms, rules, TRSs, etc.) is a big part of our formalization and notpresent in the previous formalization at all. However this theory should be usefulin future proofs. Moreover, its absence restricts the previous work to strings asvariables. Peak decreasingness is also exclusive to our formalization. Concerning
the critical pair lemma, both formalizations are approximately the same size,
but note that our formalization is concerned with critical peaks instead of critical pairs (which is more general and actually needed in later proofs). As forsoundness of abstract completion, our new formalization is drastically shorter(both columns include all definitions and intermediate lemmas that are needed
for the final soundness result). Another interesting observation might be thatin our new formalization of soundness the longest proof (confluence of the final
TRS via peak decreasingness) is a mere 80 LoI, whereas the longest proof in theprevious formalization is more than 900 LoI long (and concerned with the factthat applying an inference rule strictly decreases the cost). Finally, on top of theprevious result the soundness of completion via prime critical pairs is an easy
extension.
14

In the literature (e.g. [2,3]) critical pair criteria (like primality) are formulated
as fairness conditions for completion, and correctness proofs are a combination of
proof orders and a confluence criterion known as connected-below due to Winkler
and Buchberger [19]. Our new approach avoids this detour.

8

Conclusion

In this paper we presented a new and formalized correctness proof of abstract
completion which is significantly simpler than the existing proofs in the literature. Unlike earlier formalizations of the critical pair lemma and abstract
completion, our formalization follows the paper proof included in this paper.
This was made possible by extending IsaFoR with an abstract framework forhandling variable renamings inspired by and based on a previous formalization
for Nominal Isabelle.
Furthermore, our formalization of completion is the first that incorporates
critical pair criteria. The key to the simple proof is the notion of peak decreasingness, a very mild version of the decreasing diagrams technique for proving
confluence in the absence of termination.
There are several important variations of completion. We anticipate thatthe presented approach can be adapted for them, in particular ordered completion [5].
Acknowledgments. We want to give special thanks to the team around Sledgehammer and Nitpick [6] two indispensable Isabelle tools, the former increasing
productivity while proving by a factor of magnitude, and the latter often pointing
out slightly wrong statements that could cost hours, if not days, of a formalization attempt.

References
1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University
Press, 1998.
2. L. Bachmair. Canonical Equational Proofs. Birkhäuser, 1991.
3. L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof
orderings. Journal of the ACM, 41(2):236–276, 1994. doi:10.1145/174652.174655.
4. L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In
Proc. 1st IEEE Symposium on Logic in Computer Science, pages 346–357, 1986.
5. L. Bachmair, N. Dershowitz, and D. A. Plaisted. Resolution of Equations in Algebraic Structures: Completion without Failure, volume 2, pages 1–30. Academic
Press, 1989.
6. J.C. Blanchette, L. Bulwahn, and T. Nipkow. Automatic proof and disproof in
Isabelle/HOL. In Proc. 8th International Symposium on Frontiers of Combining
Systems, volume 6989 of Lecture Notes in Computer Science, pages 12–27, 2011.
doi:10.1007/978-3-642-24364-6_2.
7. A.L. Galdino and M. Ayala-Rincón. A formalization of the Knuth-Bendix(-Huet)
critical pair theorem. Journal of Automated Reasoning, 45(3):301–325, 2010.
doi:10.1007/s10817-010-9165-2.

15

8. G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23(1):11–21, 1981. doi:10.1016/
0022-0000(81)90002-7.
9. B. Huffman and C. Urban. A new foundation for Nominal Isabelle. In M. Kaufmann and L.C. Paulson, editors, Proc. 1st International Conference on Interactive
Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 35–50.
Springer, 2010. doi:10.1007/978-3-642-14052-5_5.
10. D. Kapur, D.R. Musser, and P. Narendran. Only prime superpositions need beconsidered in the Knuth-Bendix completion procedure. Journal of Symbolic Computation, 6(1):19–36, 1988. doi:10.1016/S0747-7171(88)80019-1.
11. D.E. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech,
editor, Computational Problems in Abstract Algebra, pages 263–297. 1970.
12. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL – A Proof Assistant forHigher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer,
2002. doi:10.1007/3-540-45949-9.
13. V. van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259–280, 1994. doi:10.1016/0304-3975(92)00023-K.
14. F. van Raamsdonk, editor. Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013.
15. J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, and F.-J. Martı́n-Mateos. Formal
proofs about rewriting using ACL2. Annals of Mathematics and Artificial Intelligence, 36(3):239–262, 2002. doi:10.1023/A:1016003314081.
16. C. Sternagel and R. Thiemann. Formalizing Knuth-Bendix orders and KnuthBendix completion. In van Raamsdonk [14], pages 287–302. doi:10.4230/LIPIcs.
RTA.2013.287.
17. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in TheoreticalComputer Science. Cambridge University Press, 2003.
18. C. Urban and C. Kaliszyk. General bindings and alpha-equivalence in Nominal
Isabelle. Logical Methods in Computer Science, 8(2):465–476, 2012. doi:10.2168/
LMCS-8(2:14)2012.
19. F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductionsin the Knuth-Bendix algorithm. In Proc. Colloquium on Algebra, Combinatorics
and Logic in Computer Science, Vol. II, volume 42 of Colloquia Mathematica Societatis J. Bolyai, pages 849–869, 1986.
20. H. Zankl. Decreasing diagrams – formalized. In van Raamsdonk [14], pages 352–
367. doi:10.4230/LIPIcs.RTA.2013352.

16