Some symmetries of commutation diamonds
Vincent van Oostrom
University of Innsbruck
Vincent.van-Oostrom@uibk.ac.at
Abstract
We study commutation of rewrite systems under swapping, reversing.

1

Introduction

Commutation may be used as a building block in various settings ranging from the abstract tothe concrete. For instance, causality may be analysed as the independence of events which may
be modeled as their commutation, and correctness of compiler optimisations may be modeled
as commutation between evaluation and optimisation. Commutation generalises confluence,
which itself may be used for establishing consistency of and deciding equational theories.
In this short paper we investigate commutation under swapping and reversing of the rewrite
systems. We show that at the level of abstract rewriting this perspective, although bringing
nothing new per se, may serve to bring unity into disparate results in the literature. At thelevel of term rewriting some fun is to be had, albeit simple, because in the commutation-bycritical-pair-analysis (due to Knuth and Bendix and Huet for first-order term rewriting, andextended to higher-order term rewriting by Nipkow), rules are commonly assumed to conformto certain restrictions, restrictions that may not be preserved when reversing them.
Example 1. Reversing the term rewrite rules:
f (x) → x

f (x) → af (x) → g(x, x)(λx.F (x))G → F (G)violates the respective requirements that: the lhs should not be a variable (x is),1 variables in
the rhs should occur in the lhs (x does not occur in a), the lhs should be linear (x occurs twicein g(x, x)),2 the lhs should be a pattern (in the sense of Miller; F (G) is not a pattern).
Instead of a conclusion we have positions after each subtopic.3

2

Diamond symmetries in abstract rewriting

We assume knowlege of abstract and term rewriting [7]. We employ arrow-like notations I,., . . . for abstract rewrite systems or relations on a (the same) set of objects, reversing thesenotations J, /, . . . to denote the reverse systems,and their repetitions II, .., . . . to denote thereflexive–transitive closures. We define J. := J ∪ . and → := I ∪ .. As in [5], we extend
terminology and notation for a single rewrite system I to the diagonal I, I, i.e. such that
P (I) iff P (I, I) for P a property of (pairs of) rewrite systems.
Definition 1. The pair I,. has the diamond property if J · . ⊆ . · J, it commutes if II,..
has the diamond property, and has the Church–Rosser property if (J ∪ .)∗ ⊆ .. · JJ.
1 Variable-lhss are allowed by Huet in his Critical Pair Lemma, but not in Nipkow’s higher-order version.
2 Although non-left-linear rules are usually allowed in term rewriting, they do not go well with commutation:
Hirokawa and Shintani show in IWC 2015, for them commutation is not even preserved by signature extension.
3 For lack of space we often only provide hyperlinks for informal references to the literature.

Commutation symmetries

V. van Oostrom

We may refer to the diagonal of P as self -P . For instance, self-commutation is conventionallyknown as confluence. The name of the diamond property derives from that it can be visualised
like that. The 8 symmetries of such a diamond (the dihedral group D4 ) give rise to 8 instancesof the diamond property, obtained by swapping and reversing the rewrite systems I, ., andhence also of commutation. We have visualised4 three of these, together with their respective(conventional) names:5

⇓

⇐

⇑

commutation

factorisation

upward commutation

Formally, letting P range over the properties in Definition 1, left–right reflecting the diamondcorresponds to swapping the pair I, . into ., I and is a symmetry: P (I, .) iff P (., I).6 Clockwise rotating the diamond corresponds to first swapping the pair I, . and then reversing thefirst element yielding /, I. The first displayed rotation turns commutation into factorisation,.. · II ⊆ II · .., which is equivalent to the Church–Rosser property of /, I, i.e. that a reductiona  b factors as a II · .. b. Symmetries preserve results. E.g. that the diamond property
implies the Church–Rosser property is the same result as that . · I ⊆ I · . implies factorisation.
Position 1. Results for diamond and commutation are to be taken up to symmetries.
How to show the Church–Rosser property of I, .? Based on a note from 1978 by De Bruijn,
we introduced the decreasing diagrams (DD) technique in my PhD thesis, requiring for each
local 7 peak a J · . b existence of a suitably constrained valley a .. · JJ b, a result we extended
in 2008 to allow conversions instead of valleys:
S
S
Definition 2. I, . is decreasing, if I := i∈I Ii , . := j∈J .j for families (Ii )i∈I , (.j )j∈J
and some well-founded strict order < on I ∪ J, such that for all i ∈ I,j ∈ J i J · .j ⊆ J.∗gi · .=j ·J.∗g{i,j} · i J= · J.∗gj , where gK := {k ∈ I ∪ J | ∃` ∈ K ` > k} and gk := g{k}.
Theorem 1 (Decreasing Diagrams, DD [4]). I, . commute if decreasing.
Since then, DD has found wide application in the literature in the study of confluence andcommutation (see below), but somewhat surprisingly (given their symmetry), as far as we know,
not yet within the study of factorisation. Here and in Section 3 we give examples8 illustrating
the power of DD also for establishing factorisation results, and at the same time how DD allows
one to focus on extracting appropriate families and orders on them, easing applicability.
S
S
Example 2. I := i Ii∈I and . := j∈I .j commute if for all i, j, .j is terminating and∗i J · .j ⊆ .j · (i J ∪ .i )(1)

To see this, first note it suffices to show Ii , . commutefor all i. Fixing i allows to turn (1)Sinto a DD by decomposing . into .i and .¬i := k6=i .k , ordering .¬i -steps above others, andordering Ii - and .i -steps via their targets by (IIi · i /·IIi )+ , well-founded by (1) [7, Exc. 1.3.19].
4 As usual, ordinary/dashed arrows represent universally/existentially quantified steps and reductions.
5 Other names of factorisation are postponement (from a .-perspective) or preponement (I-perspective).
6 This is apparent via left–right reflection of our formal notations, as these mirror those of the diamond.
7 Following Newman’s 1942 in localising properties P , we use local P to refer to P with its assumption
restricted to single steps (I,.) instead of general reductions (II,..). E.g., local commutation is J · . ⊆ .. · JJ.
8 Found by us over the past 20 years, but only privately communicated and circulated.

2

Commutation symmetries

V. van OostromThat families →• := ( • , • ) and →◦ := ( ◦ , ◦ ) satisfy the conditions of a squarefactorisation system [1], directly entails ◦ , ◦ are terminating and (1) holds for9 • ←, →◦ ,yielding the main abstract factorisation result of that paper [1, Thm. 5.2].
Note that using DD not only allowed our statement and proof to be (much) more compact,10
but also our result to be (much) more general, not just because of allowing arbitrary size families;
already for families of size 2 it is more general: e.g. where square factorisation systems require+++•·◦ to be contained in◦·( • ∪◦)◦ ·• , (1) only requires it to be contained inand similarly for . In [4] we showed that in fact all ‘local commutation ⇒ commutation’results we knew of then, could be obtained as instances of DD. We did so by introducing various
basic techniques for finding families and orders such as self - and rule-labelling. For instance,
the Lemma of Hindley–Rosen was obtained by taking for > the empty order on families [4,Example 13], and the commutation version (due to Backhouse and Doornbos) of Newman’s
Lemma was obtained by self -labelling a step a → b by its source and ordering labels by ←+ [4,Example 12].11 DD has been formalised in Isabelle and is part of the AFP, due to Zankl for
Theorem 1 and to Felgenhauer for a proof order version. DD has been automated in tools suchas ACP and CSI, and many commutation results have been factored through DD and often
generalised by it, e.g. Toyama’s famous modularity of confluence result; see the introductionof [2] for more examples. Still we think that (much) more leverage could be gotten out of DD.
Remark 1. A main feature of the TRS confluence tool CoLL [6] is that it is not built on
confluence but on commutation criteria. The idea is to (rule-based) decompose a TRS R
into a family (Ri )i of TRSs. Confluence of R follows by the Lemma of Hindley–Rosen from
commutation of all pairs (including the diagonal) Ri , Rj of family members. We suggest also
there employing DD, instead of the lemma of Hindley–Rosen, could be beneficial. In fact, an
example of such a decomposition based on DD was already given as [4, Thm. 5]. Whether/how
such decompositions could be found automatically remains to be investigated. Moreover, it
seems interesting to consider decompositions other than rule-based ones, e.g. ones obtained byinstantiation or by strategies.
Position 2. DD is the swiss-army-knife for commutation, its symmetries (factorisation), andits instances (confluence). Trying to extract appropriate families and orders on them for establishing these properties via DD, results often in (more) powerful yet (more) compact results.
How powerful is the DD technique exactly, for showing confluence and commutation?
Theorem 2.12 The DD technique is complete for confluence of rewrite systems. More precisely,
every countable13 confluent rewrite system →, is decreasing for some family and order.
As the name suggests, more than being a 1-dimensional confluence result, DD establishes a 2dimensional diagrammatic confluence result: Every peak b  a  c can be completed by somevalley b  d  c into a confluence diagram, by means of repeatedly adjoining locally decreasing
diagrams; even stronger, repeatedly adjoining such locally decreasing diagrams must terminate
after finitely many steps into a decreasing confluence diagram. We now show that countable
9 Note the reversal for the relations of the first family, turning commutation into factorisation.
10 2 lines vs. 8 lines respectively 3 lines vs. 3 pages.
11 Pous showed in 2005 that termination of (J+ · /+ )+ instead of of ←+ suffices; again DD applies, but using
step labelling instead of source-labelling [4, Example 17].
12 This was established independently by Ken Mano and the author (see Remark 2.3.29 in my PhD thesis).
The proofs employed a decomposition into a natural–number-indexed family. Recently Klop asked the question
whether smaller families suffice, upon which Endrullis, Klop and Overbeek showed that in fact doubletons do.
13 The case of uncountable systems, conjectured to be false in my PhD thesis, remains open.

3

Commutation symmetries

V. van Oostrom

confluence suffices even to obtain a 3-dimensional (decreasing) diagrammatic confluence result,by a process we dub cutting 14 faces, which will be discussed more extensively below.15
Lemma 1.16 Every countable confluent rewrite system → admits a residual system [7, Sect. 8.7](−→,
◦ 1, /) with → ⊆ −→◦ ⊆ .
Proof. By countable confluence → has a spanning forest F [2, Lem. 1]. Let the relation −→◦comprise the steps of → not in F , and the reductions of F . Viewing steps of an F -reduction
as its faces its transformation into a single −→-step◦can be viewed as cutting faces, in this caseresulting in a diamond : Define the residual %/φ of % : a −→◦ b after φ : a −→◦ c by cases on theirsources and targets to be % if c = a, 1 if a = b, and c −→◦ d otherwise with d the least common
descendant of b, c in F . One checks that the (designated) diamond property, i.e. if % : a −→◦ b,
φ : a −→
◦ c then %/φ : c −→◦ d, φ/% : b −→◦ d for some d, and the (3-dimensional) cube identity(%/φ)/(ψ/φ) = (%/ψ)/(φ/ψ) hold by uniqueness of least common descendants in F .
The process of tiling by 2-dimensional local diagrams, introduced in [3] and later resumed
by Melliès, for the purpose of establishing confluence and standardisation, need not entail the
3-dimensional cube property; the edges of the 6 plane surfaces obtained by 2-dimensional tilingneed not match up. It fails both for terms [7, Fig. 8.53] and (positive) braids [7, Sect. 8.9].
Position 3. It is of interest to study residual systems for commutation ( coloured cubes).
Is DD also complete for commutation? We raised this question in [4] and at ISR 2008.
It was summarily confuted, then and there, by two participants, Endrullis and Grabmayer:
α
γ

δ

α

δ
(β · δ)



β

α2

δ2

γ2

(β · δ)10ζ0(β · δ)1ζβδThe rewrite system on the left is not (and cannot be made) decreasing. Even stronger, although
the system commutes, that cannot be shown by tiling with local commutation diagrams, as it
embeds (omit , ζ) the standard counterexample against ‘local commutation ⇒ commutation’.
As in the previous section, cutting faces comes to the rescue: Looking at the commutation
diagram (2nd from left) for the local peak α J · .δ we see it is not yet a diamond since itneeds the 2-step reduction comprising β and δ. However, cutting the reduction into a fresh
face (step) we name (β · δ), the local diagram (3rd from left) cuts a better figure/diamond.17
Adjoining (β · δ) and, symmetrically, (α · γ) gives rise to new peaks, but we see these can also
be completed into diamonds (right diagram). The rewrite system obtained is decreasing forthe labels in the natural numbers ordered by ≤, as displayed in the rightmost two diagrams.
Cutting is a common process, e.g., parallel steps −→p p for TRSs and multi-steps −→◦ for HRSs
and braids [7] can be seen as being obtained by repeatedly cutting diagrams into diamonds.18
Position 4. Minimally19 cutting faces is useful to get diamonds, decreasing diagrams and cubes.
14 Our (tentative) naming is based on that used for processing raw diamonds. However, adjoining transitive
inferences (cutting corners), is at the basis of both our cuts and those in proof theory, where, e.g., Γ ` ∆ may
be obtained by cutting the occurrence of A between Γ ` A and A ` ∆.
15 We learned the technique of cutting faces in 1995 from Hans Zantema, for braids.
16 This result was obtained in 2008, in our collaboration with Patrick Dehornoy on the Z-property.
17 The diamond is still not square, but could be made so by adjoining empty reductions reified into steps.
18 Somewhat miracuously, in these 3 cases even cubes are obtained.
19 Cutting reductions into steps by need only; if I, . commutes, simply taking II, .. as steps yields a diamond.

4

Commutation symmetries

3

V. van Oostrom

Diamond symmetries in term rewriting

Commutation between term rewrite systems is standardly reduced to an analysis of their criticalpeaks, cf. [6]. Symmetry suggests the same applies to factorisation, but then for peaks withrespect to the reverse of the second system. Despite that standard term rewriting theory is not
well-adapted to reverse rules, cf. Example 1, it can often be easily adapted, as we illustrate:
Example 3. Factorisation holds in the untyped λ-calculus for I := →β , . := →η . Note thereverse P → λy.P y of the η-rule is not a higher-order pattern rule in the sense of Nipkow,
as its left-hand side P is a variable. Still, we do have a (single) critical peak à la Huet withthe β-rule: Q := (λy.(λx.M )y)N . (λx.M )N I M [x:=N ] =: R; in rewriting terminology, the.-step is said to create the I-step. Toward factorisation, note the critical peak can be completed
as Q I (λx.M )N I R. Observing the first I-step is affine (non-duplicating) we decompose I
into affine I1 and non-affine steps I2 . We claim that then all local peaks are decreasing for theorder I1 < / < I2 . For the above critical diagram this holds per construction of our order. A
non-critical, i.e. non creating, local peak . · Ii can be completed by Ii · .. by standard residual
theory, using that the η-rule is linear, which again yields a decreasing diagram.
Position 5. Extending Nipkow’s higher-order critical pair lemma to allow for variable-lhss (àla Huet) is useful. Lifting results should be unproblematic (exception: development-closedness).
Example 4. To show head,internal-factorisation for untyped λβ-calculus, first note that although critical peaks seem intricate as the reverse of the β-rule is not a pattern-rule (Example 1), here there are in fact none as a step creating a head-step outside it must be head itself, so
not internal. Next, note it suffices to show I, .-factorisation for I := →h and . := −→◦ i since→i ⊆ −→◦ i ⊆ i . Finally, we conclude by DD ordering I < / since . · I ⊆ I · −→◦ ⊆ I · II · .=where the 1st inclusion holds by Church–Rosser as the I-step must be a unique residual as →i steps can neither create (noted) nor replicate I-steps, and the 2nd20 by exhaustively (it stops
by Finite Developments) selecting I-steps from −→◦ until the residual is a .-step or empty.21
Position 6. Factorisation of term rewrite system( strategie)s is best22 analysed by a criticalpeak analysis between rules and reverse rules.

References[1] B. Accattoli. An abstract factorization theorem for explicit substitutions. In Proc. 23rd RTA,
volume 15 of LIPIcs, pages 6–21. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2012.
[2] N. Hirokawa, J. Nagele, V. van Oostrom, and M. Oyamaguchi. Confluence by critical pair analysis
revisited. In Proc. 27th CADE, volume 11716 of LNCS, pages 319–336. Springer, 2019.
[3] J.W. Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht, 1980.
[4] V. van Oostrom. Confluence by decreasing diagrams, converted. In Proc. 19th RTA, volume 5117
of LNCS, pages 306–320. Springer, 2008.
[5] V. van Oostrom and Y. Toyama. Normalisation by Random Descent. In Proc. 1st FSCD, volume 52of LIPIcs, pages 32:1–32:18. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016.
[6] K. Shintani and N. Hirokawa. Coll: A confluence tool for left-linear term rewrite systems. In Proc.
25th CADE, volume 9195 of LNCS, pages 127–136. Springer, 2015.
[7] Terese. Term Rewriting Systems. Cambridge University Press, 2003.
20 Thanks to the IWC reviewers for pointing out that by mistake I had oversimplified this (part of the) proof.
21 A similar analysis applies to strategies other than head, e.g. spine or left.
22 As observed by Geuvers in (the ‘Stellingen’ going with) his PhD thesis, the above critical peak between thereverse of η and β, was missed by Barendregt in the proof of Corollary 15.1.5 in his book The Lambda Calculus.

5