Parallel Closedness Revisited
Kiraku Shintani1 and Nao Hirokawa1JAIST, Japan{s1820017,hirokawa}@jaist.ac.jp∗
Abstract
In this note we present a simple proof of Huet’s parallel closedness theorem (1980).
We also show that Toyama’s almost parallel closedness (1988), a generalization of Huet’stheorem, is subsumed by his earlier result (1981), which is known to be a generalization ofGramlich’s confluence criterion based on parallel critical pairs (1996).

1

Introduction

The parallel closedness theorem by Huet [3] is a pioneering work in analyzing confluence of leftlinear term rewrite systems (TRSs). It claims that a left-linear TRS is confluent if every criticalq His theorem, including its ingenious proof technique, had
pair is closed by parallel step −→.
a significant influence on later confluence research. In 1996, Gramlich [2] introduced parallel
critical pairs to make a powerful variant of Huet’s theorem. While the resulting criterion enables
us to use relaxed forms for the closing condition, he also showed that it is not comparable with
Huet’s theorem. This might give us the impression that criteria based on parallel critical pairs
cannot supersede ones based on ordinary critical pairs (see e.g. [1, Section 6.5]). However, thisis wrong. We will show that Toyama’s earlier result [9] subsumes Huet’s theorem as well as
Gramlich’s criterion. Actually it subsumes the almost parallel closedness theorem [10], whichis Toyama’s later work and known as a generalization of Huet’s theorem.
In the remaining part of the note we revisit Huet’s and Toyama’s parallel closedness theorems. Introducing a new induction measure, we give a simple proof of the parallel closedness
theorem in Section 2. In Section 3 we show that Toyama’s earlier result subsumes his later
result. We assume familiarity with term rewriting [1, 8].

2

Huet’s Parallel Closedness

In this section we present a simple proof of Huet’s parallel closedness theorem [3] with a newmeasure. By denoting the critical pair t ← · →− u by t ←o→− u, the theorem is stated as follows:qDefinition 1 ([3]). A TRS is parallel closed if ←o→− ⊆ −→.
Theorem 1 ([3]). A left-linear TRS is confluent if it is parallel closed.
We prepare notations for our new measure. Let t be a term. The size of t is denoted by|t|. Given a set P of positions in t, we write |t|P for the sum of |(t|p )| for all p ∈ P . Notethat |t| > |t|P holds if P is a set of parallel positions of t. We define the strict order  as thelexicographic product of the standard order > on N and the proper superterm relation B. WeP
also prepare terminologies for analyzing peaks. Let Γ : t ←q− `σ →− rσ be a peak, where ` → r
is a rewrite rule. We say that Γ is overlapping if some position p ∈ P is a function position inP` and in the case of P = {} the rule employed in t ←q− `σ is not a variant of ` → r. Otherwise,Γ is non-overlapping. We are ready for proving the theorem.
∗ Supported by JSPS KAKENHI Grant Number 17K00011 and Core-to-Core Program.

Parallel Closedness RevisitedI.H.

||||·tuQ||ss

PMLt(ii) non-rootu·||q||>
||s0

P0t(iii) non-overlappingQ0||uI.H.

||s||>

K. Shintani and N. Hirokawa·||(iv) overlapping

Figure 1: Proof of Theorem 1.
Proof of Theorem 1. Let R be a left-linear and parallel closed TRS. It is sufficient to show thatQP
q u be a peak. By well-founded induction onq has the diamond property. Let Γ : t ←q− s −→−→q(|t|P + |u|Q , s) with respect to  we show t −→ · ←q− u. Depending on the shape of Γ, wedistinguish four cases. Figure 1 illustrates cases (ii)–(iv).
q u or t ←q− u. In either case the claim holds.
(i) If P or Q is empty then t −→q f (u1 , . . . , un )(ii) If P * {} and Q * {} then Γ is of form f (t1 , . . . , tn ) ←q− f (s1 , . . . , sn ) −→PiQi

q ui for all 1 6 i 6 n. Here Pi = {p | ip ∈ P } and Qi = {q | iq ∈ Q}. Forwith ti ←q− si −→each i ∈ {1, . . . , n}, we have |t|P > |ti |Pi and |u|Q > |ui |Qi , and therefore |t|P + |u|Q >|ti |Pi + |ui |Qi . Since (|t|P + |u|Q , s)  (|ti |Pi + |ui |Qi , si ) holds, the induction hypothesis
q vi ←q− ui for some vi . Thus, t −→q f (v1 , . . . , vn ) ←q− u follows.
yields ti −→(iii) If Γ is non-overlapping and P or Q is {} then the Parallel Moves Lemma applies [1,Lemma 6.4.4]. Figure 1(iii) illustrates the case of P = {}.
(iv) If Γ is overlapping and P or Q is {}, say P = {}, then there exists an overlapping peakQ0qP0q u for Q0 = Q \ {q}. By parallel closedness we have s0 −→q t fort←−s−→ s0 with s0 −→0some P . As |t|{} > |t|P 0 and |u|Q > |u|Q0 hold, |t|{} + |u|Q > |t|P 0 + |u|Q0 holds. Sinceq · ←q− u.
(|t|{} + |u|Q , s)  (|t|P 0 + |u|Q0 , s0 ) holds, the induction hypothesis yields t −→With a small example taken from [2], we illustrate the usage of the theorem.
Example 1. Consider the left-linear and non-terminating TRS [2]:a→bf(a, a) → g(f(a, a))f(b, x) → g(f(x, x))f(x, b) → g(f(x, x))

While the TRS admits three critical peaks, all of them are closed by single parallel steps:f(a, a)f(b, a)g(f(a, a))f(a, a)f(a, b)||f(b, b)g(f(a, a))||g(f(b, b))g(f(b, b))||Thus, the TRS is parallel closed. Hence, the TRS is confluent.
Using the TRS in Example 1, we compare our induction measure with Huet’s originalmeasure [3]. Our proof measures a peak by the amount of contractums. Consider e.g. the peak:{1,2}{}q g(f(a, a))f(b, b) ←q− f(a, a) −→2

Parallel Closedness RevisitedK. Shintani and N. Hirokawa

The overlined part indicates the contractums in the target terms of the parallel steps.1 So theP2
P1
q u by theamount is |b| + |b| + |g(f(a, a))| = 6. Huet’s proof [3, 1] measures a peak t ←q− s −→amount of overlaps of redexes:X(s|p )|s, P1 , P2 | :=p∈Q1 ∪Q2

where Q1 = {p ∈ P1 | p > q for some q ∈ P2 } and Q2 = {p ∈ P2 | p > q for some q ∈ P1 }.
In the above peak the doubly underlined part indicates the overlaps of the redexes. So theamount is 2. Even with this measure the same proof goes through, provided that well-foundedinduction on (|s, P, Q|, s) with respect to  is performed. However, proving the inequality|s, {}, Q| > |s0 , P 0 , Q0 | in case (iv) is notoriously difficult [5, 4]. This part is trivial in our proof.

3Toyama’s Extensions

Toyama made two variations of Huet’s parallel closedness theorem in 1981 [9] and in 1988 [10],but their relation has not been known. In this section we briefly recall his and related results,
and then show that Toyama’s earlier result subsumes the later one.
In 1988, Toyama showed that the closing form for overlay critical pairs, originating fromproot overlaps, can be relaxed. Let t ←−·→− u be a critical pair. We write t ←−o→ u if p = ,>and t ←−−o→ u if p > .
q · ∗← andDefinition 2 ([10]). A TRS is almost parallel closed if the inclusions ←−o→ ⊆ −→>q hold.
←−−o→ ⊆ −→Theorem 2 ([10]). A left-linear TRS is confluent if it is almost parallel closed.
Inspired by almost parallel closedness, Gramlich [2] developed a confluence criterion basedon parallel critical pairs in 1996.
Definition 3. We say that (`σ)[rp ]p∈P ←q− `σ →− rσ is a parallel critical peak of a TRS R if• P ⊆ PosF (`) is a non-empty set of parallel positions in `,• ` → r and `p → rp (for p ∈ P ) are variants of R-rules having no common variables,• σ is a most general unifier of {`p ≈ (`|p )}p∈P , and• if P = {} then ` → r is not a variant of ` → r.
>

P



We write t ←q−o→ u if t ←q− s →− u is a parallel critical peak and P 6= {}.
q · ∗← andTheorem 3 ([2]). A left-linear TRS is confluent if the inclusions ←o→− ⊆ −→>
←q−o→ ⊆ →∗ hold.
Unfortunately, this criterion by Gramlich does not subsume (almost) parallel closedness.
Example 2 (Continued from Example 1). The TRS admits the following non-overlay parallel
critical peak f(b, b) ←q− f(a, a) →− g(f(a, a)). However, f(b, b) →∗ g(f(a, a)) does not hold.
1 Up to our best knowledge, this idea first appeared in the paper by Oyamaguchi and Ohta [7].

3Parallel Closedness RevisitedK. Shintani and N. Hirokawa

As noted in the paper [2], Toyama [9] had already obtained in 1981 a closedness result thatsubsumes Theorem 3.
Theorem 4 ([9]). A left-linear TRS is confluent if the following conditions hold.
q · ∗← holds.
(a) The inclusion ←o→− ⊆ −→PQ(b) Every parallel critical peak t ←q− s →− u admits Sa valley of the form t →∗ v ←q− u withVar(s, P ) ⊇ Var(v, Q). Here Var(s, P ) stands for p∈P Var(s|p ).
Example 3. Consider again the TRS of Example 1. As witnessed in Example 1, the inclusion
q holds. Thus, condition (a) of Theorem 4 holds. There are four parallel critical←o→− ⊆ −→peaks and they can be closed as follows:g(f(a, a))||f(a, b)g(f(a, a))∗g(f(b, b))∗g(f(b, b))f(b, b)g(f(a, a))∗∗||f(b, a)f(a, a)||f(b, b)||f(a, a)||f(a, a)g(f(b, b))
It is easy to see that the diagrams fulfil condition (b). Hence, confluence follows by Theorem 4.
We show that Theorem 4 even subsumes Theorem 2. The next lemma relates the Parallel
Moves Lemma [1, Lemma 6.4.4] to the variable condition of Theorem 4.
P

QLemma 1. Let R be a left-linear TRS. If t ←q− s →− u is non-overlapping then t →− v ←q− u andVar(s, P ) ⊇ Var(v, Q) for some term v and set Q of parallel positions.
The above statement is extended to parallel peaks for almost parallel closed TRSs.
P1

P2

q u thenLemma 2. Let R be a left-linear almost parallel closed TRS. If t ←q− s −→Q1

• t →∗ v1 ←q− u and Var(s, P1 ) ⊇ Var(v1 , Q1 ) for some v1 and Q1 , andQ2

q v2 ∗← u and Var(s, P2 ) ⊇ Var(v2 , Q2 ) for some v2 and Q2 .
• t −→
P1P2

q u. We perform well-founded induction on (|t|P1 + |u|P2 , s) with respect
Proof. Let Γ : t ←q− s −→to . We distinguish cases, depending on the shape of Γ.
Pq v.
(i) If P1 or P2 is ∅ then the claim follows from the fact: Var(w, P ) ⊇ Var(v, P ) if w −→(ii) If P1 * {} and P2 * {} then we may assume s = f (s1 , . . . , sn ), t = f (t1 , . . . , tn ), u =PiPi

1q2 ui for all 1 6 i 6 n. Here Pki denotes the set {p | i·p ∈ Pk }.
f (u1 , . . . , un ), and ti ←q−si −→As in case (ii) of the proof of Theorem 1 we can deduce (|t|P1 +|u|P2 , s)  (|ti |P1i +|ui |P2i , si ).

PiPi

1q2 ui . By the induction hypothesis it admits valleys ofConsider an i-th peak ti ←q−
si −→

QiQi

2q1 v1i ∗← ui and ti →∗ v2i ←q−ui such that Var(vki , Qik ) ⊆ Var(si , Pki ) for boththe forms ti −→k ∈ {1, 2}. For each k, take Qk = {i · q | 1 6 i 6 n and q ∈ Qik } and vk = f (vk1 , . . . , vkn ).

QQ

1q2 v2 ∗← u hold, and moreover the inclusion
Then, t →∗ v1 ←q− u and t −→Var(vk , Qk ) =n[Var(vki , Qik ) ⊆i=1

holds for each k. Hence, the claim follows.
4n[i=1Var(si , Pki ) = Var(s, Pk )

Parallel Closedness RevisitedK. Shintani and N. Hirokawa(iii) If Γ is non-overlapping and P1 or P2 is {} then the claim is straightforward from Lemma 1.
Q1(iv) If Γ is overlapping with P1 = P2 = {} then by almost parallel closedness t →∗ v1 ←q− u
Q2q v2 ∗← u for some v1 , v2 , Q1 , and Q2 . For each k ∈ {1, 2} we have s →∗ vk , soand t −→Var(vk ) ⊆ Var(s) follows. Therefore, Var(vk , Qk ) ⊆ Var(vk ) ⊆ Var(s) = Var(s, {}). Theclaim holds.
(v) If Γ is overlapping with P1 = {} and P2 6= {} then there exists p ∈ P2 such thatps −→ s0P2 \{p}q−→pu and t ←− s −→ s0 is an instance of a critical peak. By almost parallel

P10closedness t ←q− s0 for some P10 . As in case (iv) of the proof of Theorem 1 we can deduce(|t|P1 +|u|P2 , s)  (|t|P10 +|u|P2 \{} , s0 ). Thus, the claim follows by the induction hypothesis
P0P \{p}21q u and Var(s0 , P2 \ {p}) ⊆ Var(s, P2 ).
for t ←q−s0 −→Theorem 5. Every left-linear and almost parallel closed TRS satisfies conditions (a) and (b)of Theorem 4. In other words, Theorem 4 subsumes Theorem 2.
q Lemma 2 entails the claim.
Proof. Since (parallel) critical peaks are instances of ←q− · −→,4Concluding Remark

We presented a simple proof of Huet’s parallel closedness theorem, using a new measure, andalso proved that Toyama’s almost parallel closedness theorem is subsumed by his earlier result
based on parallel critical pairs. We anticipate that our measure can be adapted to otherconfluence criteria for term rewriting and conditional rewriting, while it is unclear whether it
can be adapted to the proof of van Oostrom’s development closedness [6]. At least the current
definition does not go through. Despite its powerfulness, Theorem 4 has not been well studied.
In particular, whether the variable condition of Theorem 4 is essential is our primary question.

References[1] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
[2] B. Gramlich. Confluence without termination via parallel critical pairs. In Proc. 21st CAAP,
volume 1059 of LNCS, pages 211–225, 1996.
[3] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems.
Journal of the ACM, 27:797–821, 1980.
[4] J. Nagele. Mechanizing Confluence. PhD thesis, University of Innsbruck, 2017.
[5] J. Nagele and A. Middeldorp. Certification of classical confluence results for left-linear term rewritesystems. In Proc. 7th ITP, volume 9807 of LNCS, pages 290–306, 2016.
[6] V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.
[7] M. Oyamaguchi and Y. Ohta. A new parallel closed condition for Church-Rosser of left-linear
term rewriting systems. In Proc. 10th RTA, volume 1232 of LNCS, pages 187–201, 1997.
[8] TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
[9] Y. Toyama. On the Church-Rosser property of term rewriting systems. Technical Report 17672,
NTT Electro-Technical Laboratory, 1981. In Japanese.
[10] Y. Toyama. Commutativity of term rewriting systems. In Programming of Future Generation
Computers II, pages 393–407. North-Holland, 1988.

5