Symmetries of commutation diamonds
Vincent van Oostrom
http://cl-informatik.uibk.ac.at

Tiling the plane
Tiling peaks
with diamondswith right-faceted diamondswith multi-faceted diamonds
Making diamonds decreasing,⌘-factorisation
spine,vertebrae-factorisation
self-commutation of some term rewrite system
Take-aways

tiling the plane (Hao Wang 1961)
decision problem
given set of tiles, can it tile the plane?

tiling the planedecision problem
given set of tiles, can it tile the plane?

tiling the planedecision problem
given set of tiles, can it tile the plane?

conjecture
any solution will be periodic, so decidabletiling the planedecision problem
given set of tiles, can it tile the plane?

refutation
no, aperiodic tiling; simulate Turing machine (halting i↵ plane not tiled; Berger 1966)diamonds (Newman 1942, Hindley 1964, Rosen 1973)
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}⇣ is repetition of !; problem equivalent to Church–Rosser (1[ !2 )⇤ ✓ ⇣2 · 1 ⌘diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}commutation diamond (1· !2 ✓ !2 · 1)

no critical peaks between T1 , T2 , and for non-critical peaks:I·!✓!·(rules linear)
I

·!✓!·

(rules linear)diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}commutation diamond (1· !2 ✓ !2 · 1)

no critical peaks between T1 , T2 , and for non-critical peaks:
I
·!✓!·
I

·!✓!·

m n
more precisely n1 · !m2 ✓ !2 · 1
and random descent (reductions to common reduct have same length)diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds

diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}a.k.a. preponement, postponement, commutation over, separation; problem equivalent
to (!1 [ !2 )⇤ ✓ ⇣2 · ⇣1 ; note !2 , !1 -factorisation is 1 , !2 -commutation

factorisation diamond (!1 · !2 ✓ !2 · !1 )no critical peaks between T1 1 , T2 , and for non-critical peaks:
I ! · ! ✓ ! · ! (rules linear)
I !·!✓!·!

(rules linear)diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}a.k.a. preponement, postponement, commutation over, separation; problem equivalent
to (!1 [ !2 )⇤ ✓ ⇣2 · ⇣1 ; note !2 , !1 -factorisation is 1 , !2 -commutation

factorisation diamond (!1 · !2 ✓ !2 · !1 )no critical peaks between T1 1 , T2 , and for non-critical peaks:
I !·!✓!·!
I !·!✓!·!

no critical peaks between T1 1 , T2 means no overlap between rhss of T1 and lhss of T2 :T1 does not create T2 . commutation is factorisation up to symmetry.

diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {a ! b}

I T2 = {f (x) ! g (f (x)), f (x) ! h(x)}a.k.a. preponement, postponement, commutation over, separation; problem equivalent
to (!1 [ !2 )⇤ ✓ ⇣2 · ⇣1 ; note !2 , !1 -factorisation is 1 , !2 -commutation

factorisation diamond (!1 · !2 ✓ !2 · !1 )no critical peaks between T1 1 , T2 , and for non-critical peaks:
I !·!✓!·!
I !·!✓!·!

commutation and factorisation of given rewrite system independenta ! b, a ! c has !,!-factorisation, no !,!-commutationb ! a, a ! c has !,!-commutation, no !,!-factorisation

diamonds

diamonds

right-faceted diamonds (Hindley 1964, Huet 1978)
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = { y .P y ! P} (⌘-reduction in -calculus, as HRS rule)
I T2 = {( x.M(x)) N ! M(N)} ( -reduction in -calculus, as HRS rule)
is replicating, not linear; moreover 2 critical peaks; no diamonds

right-faceted diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = { y .P y ! P}

I T2 = {( x.M(x)) N ! M(N)}commutation right-faceted diamond (1I

x.M(x)I PN
I· !2 ✓ !2 · 1 ⌘)y .( x.M(x)) y ! y .M(y )( y .P y ) N ! P N(trivial critical peak, up to ↵)(trivial critical peak)· ! ✓ ! · ⌘ (non-critical peaks; ⌘ linear,

replicating)right-faceted diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = { y .P y ! P}

I T2 = {( x.M(x)) N ! M(N)}commutation right-faceted diamond (1I

x.M(x)I PN
I· !2 ✓ !2 · 1 ⌘)y .( x.M(x)) y ! y .M(y )( y .P y ) N ! P N·!✓!·⌘

mmore precisely 1 ⌘ · !m· 1 ⌘; valleys for critical peaks not rectangular;
2 ✓ !2resolved by adjoining empty !1 ,!2 steps (technique 1 )right-faceted diamonds
splitting point
facetsright-faceted diamonds

right-faceted diamonds
scale vertically to fit

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds
scale vertically to fit

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds

right-faceted diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {P ! y .P y } (⌘-expansion in -calculus)
I T2 = {( x.M(x)) N ! M(N)}
2 critical peaks (between T1 1 and T2 ); no diamonds

right-faceted diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {P ! y .P y }I T2 = {( x.M(x)) N ! M(N)}factorisation right-faceted diamond (!1 · !2 ✓ !2 · ⇣1 )I

x.M(x) ! y .( x.M(x)) y ! y .M(y )I P N ! ( y .P y ) N ! P N
I !·!✓!·⇣

right-faceted diamonds
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = {P ! y .P y }I T2 = {( x.M(x)) N ! M(N)}factorisation right-faceted diamond (!1 · !2 ✓ !2 · ⇣1 )I

x.M(x) ! y .( x.M(x)) y ! y .M(y )I P N ! ( y .P y ) N ! P N
I !·!✓!·⇣, ⌘ 1 -factorisation is ⌘, -commutation

right-faceted diamonds

right-faceted diamondsmulti-faceted diamonds (Newman 42, de Bruijn 1978, vO 1994)
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {b ! a, a ! c}
I T2 = {a ! b, b ! d}both right- and left-faceted diamondsmulti-faceted diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {b ! a, a ! c}
I T2 = {a ! b, b ! d}commutation multi-faceted diamond (1critical peaks between T1 , T2 :I·!✓
· (right faceted)I· !2 ✓ ⇣2 · 1 ⌘)· ! ✓ ! · !(left-faceted)

Counterexample c 1(Kleene).

a1

2 b ! d to local commutation =) commutation2

multi-faceted diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {b ! a, a ! c, d ! e}
I T2 = {a ! b, b ! d, c ! e}commutation multi-faceted diamond (1critical peaks between T1 , T2 :
I
·!✓
·
I

· !2 ✓ ⇣2 · 1 ⌘)·!✓!·!

Counterexample c 1 a 1 2 b !2 d to local commutation =) commutation(Kleene). Adjoining c !2 e 1 d shows even if commutation holds, that need not be
provable by local commutation tiling (reusing Endrullis, Grabmayer)multi-faceted diamonds
commutation problem (1 ⌘ · ⇣2 ✓ ⇣2 · 1 ⌘?)for term rewrite systems T1 and T2
I T1 = {b ! a, a ! c, d ! e}
I T2 = {a ! b, b ! d, c ! e}commutation multi-faceted diamond (1· !2 ✓ ⇣2 · 1 ⌘)critical peaks between T1 , T2 :I·!✓!· ·
(adjoining empty !-step to get rectangular tile)
I·!✓!·!·(adjoining empty-step to get rectangular tile)

Counterexample c 1 a 1 2 b !2 d to local commutation =) commutation(Kleene). Adjoining c !2 e 1 d shows even if commutation holds, that need not be
provable by local commutation tiling (reusing Endrullis, Grabmayer)multi-faceted diamonds

horizontal
verticalsplitting pointmulti-faceted diamondsmulti-faceted diamondsmulti-faceted diamondsmulti-faceted diamondsmulti-faceted diamondsmulti-faceted diamonds

1multi-faceted diamonds

1multi-faceted diamonds
splitting
I if tiling is infinite, there is an infinite reduction through infinitely many horizontal
and vertical splitting points (alternatingly)multi-faceted diamonds
splitting
I if tiling is infinite, there is an infinite reduction through infinitely many horizontal
and vertical splitting points (alternatingly)
I local commutation =) commutation, if !1 [ !2 terminating (Newman 1942,+
Backhouse & Doornbos 1994), even if just !+1 · !2 terminating (Pous 2005)multi-faceted diamonds
splitting
I if tiling is infinite, there is an infinite reduction through infinitely many horizontal
and vertical splitting points (alternatingly)
I local commutation =) commutation, if !1 [ !2 terminating (Newman 1942,+
Backhouse & Doornbos 1994), even if just !+1 · !2 terminating (Pous 2005)
I extended Kleene example commuting but not terminating . . . ? Avoid splitting byadjoining certain reductions in valleys as single steps (technique 1; faceting).

multi-faceted diamonds
splitting
I if tiling is infinite, there is an infinite reduction through infinitely many horizontal
and vertical splitting points (alternatingly)
I local commutation =) commutation, if !1 [ !2 terminating (Newman 1942,+
Backhouse & Doornbos 1994), even if just !+1 · !2 terminating (Pous 2005)
I extended Kleene example commuting but not terminating . . . ? Avoid splitting byadjoining certain reductions in valleys as single steps (technique 1; faceting).
I cb (adjoined to T1 for c·b)
a ! d (adjoined to T2 for a ! · ! d)multi-faceted diamonds
splitting
I if tiling is infinite, there is an infinite reduction through infinitely many horizontal
and vertical splitting points (alternatingly)
I local commutation =) commutation, if !1 [ !2 terminating (Newman 1942,+
Backhouse & Doornbos 1994), even if just !+1 · !2 terminating (Pous 2005)
I extended Kleene example commuting but not terminating . . . ? Avoid splitting byadjoining certain reductions in valleys as single steps (technique 1; faceting).
I c
b
a!d
I new critical peaks:
c
b!d
c
a!d

multi-faceted diamonds
splitting
I if tiling is infinite, there is an infinite reduction through infinitely many horizontal
and vertical splitting points (alternatingly)
I local commutation =) commutation, if !1 [ !2 terminating (Newman 1942,+
Backhouse & Doornbos 1994), even if just !+1 · !2 terminating (Pous 2005)
I extended Kleene example commuting but not terminating . . . ? Avoid splitting byadjoining certain reductions in valleys as single steps (technique 1; faceting).
I c
b
a!d
I new critical peaks:cb ! d joinable by c ! e
d into diamondca ! d joinable by c ! e
d into diamond
4 tiles in total, all (square) diamondsmulti-faceted diamonds
adjoineddiamondface cut, so no
splitting pointmulti-faceted diamonds
adjoineddiamondface cut, so no
splitting pointmulti-faceted diamonds
questioncharacterise shape of multi-faceted diamonds such that tiling always terminates?

multi-faceted diamonds
questioncharacterise shape of multi-faceted diamonds such that tiling always terminates?

1

note colors alternate (between red and yellow) along infinite reductionmulti-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reductionmulti-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reduction

any well-founded order; here rainbow color ordermulti-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reduction

middle facet in valley same color as opposite facet in peakmulti-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reduction

facets before middle, smaller color than adjacent facet in peakmulti-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reduction

facets after middle, smaller color than either facet in peakmulti-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reduction

tiling peaks terminates for any set of decreasing diamonds (de Bruijn 1978)multi-faceted diamonds
idea
order the facets in valley below peak such that colors decrease along infinite reduction

tiling peaks terminates for any set of decreasing diagrams (de Bruijn 1978),⌘-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = { y .P y ! P}

I T2 = {( x.M(x)) N ! M(N)},⌘-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = { y .P y ! P}

I T2 = {( x.M(x)) N ! M(N)}factorisation decreasing diamond?
I ( y .( x.M(x)) y ) N ! ( x.M(x)) N ! M(N) (⌘ 1 , critical peak)( y .( x.M(x)) y ) N ! ( x.M(x)) N ! M(N) (valley of left-faceted diamond)I ! · ! ✓ ! · ⇣ (non-critical peaks; right faceted diamonds),⌘-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for term rewrite systems T1 and T2
I T1 = { y .P y ! P}

I T2 = {( x.M(x)) N ! M(N)}factorisation decreasing diamond?
I ( y .( x.M(x)) y ) N ! ( x.M(x)) N ! M(N)( y .( x.M(x)) y ) N ! ( x.M(x)) N ! M(N)I !·!✓!·⇣

firstin critical valley is specialisation ofI ( x.M(x)) N ! M(N)I ( x.M(x)) N ! M(N)(technique 2; Hirokawa et al. 2019)

if x occurs  1 times in M
if x occurs > 1 times in M

renders al diamonds decreasing,⌘-factorisation
criticalduplicating

affinenon-criticalspine,vertebrae-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for rewrite systems T1 and T2 on the set of -terms
I T1 = ! may contract any -redex at vertebrae position
I T2 = ! may contract any -redex at spine positionnote ! = ! [ !

(62 1⇤ )(2 1⇤ )

spine,vertebrae-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for rewrite systems T1 and T2 on the set of -terms
I T1 = ! may contract any -redex at vertebrae position
I T2 = ! may contract any -redex at spine position

factorisation decreasing diamond for !, !?
I no critical peaks(! cannot create !; spine closed under prefix)

I ! · ! ✓ ! · ⇣ (non-critical peak; ! cannot replicate !)note ⇣ here is development of residuals of ! after ! (both from source)spine,vertebrae-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for rewrite systems T1 and T2 on the set of -terms
I T1 = ! may contract any -redex at vertebrae position
I T2 = ! may contract any -redex at spine position

factorisation decreasing diamond for !, !?
I no critical peaks

I ! · ! ✓ ! · ⇣ (non-critical peak; ! cannot replicate !)example( x.x x) (( y .y ) z) ! ( x.x x) z ! z z factorises to( x.x x) (( y .y ) z) ! ( y .y ) z (( y .y ) z) ! z (( y .y ) z) ! z z
may yield multiple !, !-steps =) choose to facet !-developments as !

spine,vertebrae-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for rewrite systems T1 and T2 on the set of -terms
I T1 = ! may contract any -redex at vertebrae position
I T2 = ! may contract any -redex at spine position

factorisation decreasing diamond for !, !?
I still no critical peaks

I ! · ! ✓ ! · ⇣ ✓ ! · ⇣ · ! (non-critical peak; is decreasing diamond)development of !-step is !-reduction (cf. Melliès’ segmentation property)

spine,vertebrae-factorisation
factorisation problem (⇣1 · ⇣2 ✓ ⇣2 · ⇣1 ?)for rewrite systems T1 and T2 on the set of -terms
I T1 = ! may contract any -redex at vertebrae position
I T2 = ! may contract any -redex at spine position

factorisation decreasing diamond for !, !?
I still no critical peaks

I ! · ! ✓ ! · ⇣ ✓ ! · ⇣ · ! (non-critical peak; is decreasing diamond)

adaptations
same critical peak analysis works for head,internal-factorisation for -reduction:
I head-steps have unique origin along internal steps (head-positions closed underprefix; if rhs of step overlaps/is above head-redex then step is itself head)I developing a set of internal redexes yields internal reductionself-commutation of some term rewrite systemsome term rewrite systemI three rules of which the 1st is (self-)replicating, the other two !, ! linearself-commutation of some term rewrite systemsome term rewrite systemI three rules of which the 1st is (self-)replicating, the other two !, ! linear

I for non-critical peaks facet developments of 1st as !, ordered above !,!-steps

self-commutation of some term rewrite systemsome term rewrite systemI three rules of which the 1st is (self-)replicating, the other two !, ! linear

I for non-critical peaks facet developments of 1st as !, ordered above !,!-steps
I for critical peaks:

fourth diagram then not decreasing, but only linear specialisation ! of ! neededself-commutation of some term rewrite systemsome term rewrite systemI three rules of which the 1st is (self-)replicating, the other two !, ! linear

I for non-critical peaks facet developments of 1st as !, ordered above !,!-steps
I critical peaks after adjoining linear specialisation !:fifth diagram not decreasing, but ! [ ! [ ! terminating (SOL, Hamana 2020)

self-commutation of some term rewrite systemsome term rewrite systemI three rules of which the 1st is (self-)replicating, the other two !, ! linear

I for non-critical peaks facet developments of 1st as !, ordered above !,!-steps
I critical peaks after adjoining linear specialisation !:fifth diagram not decreasing, but ! [ ! [ ! terminating (SOL, Hamana 2020)

I source labelling these (all still ordered below !), all decreasing =) confluencetake-aways
I commutation = factorisation, up to symmetry

take-aways
I commutation = factorisation, up to symmetry
I for structured (string, term, . . . ) rewrite systems, analysed via critical peaks, i.e.
overlaps between left- respectively right-hand sides of 1st, left-hand sides of 2ndtake-aways
I commutation = factorisation, up to symmetry
I for structured (string, term, . . . ) rewrite systems, analysed via critical peaks, i.e.
overlaps between left- respectively right-hand sides of 1st, left-hand sides of 2nd
I two techniques for making diagrams decreasing
1. faceting: adjoining certain reductions in valleys as rules (parallel steps, developments
for term rewriting, left-divisors of Garside-element for braids, empty reductions)
2. specialisation: adjoining rules in context,substitution as rulestake-aways
I commutation = factorisation, up to symmetry
I for structured (string, term, . . . ) rewrite systems, analysed via critical peaks, i.e.
overlaps between left- respectively right-hand sides of 1st, left-hand sides of 2nd
I two techniques for making diagrams decreasing
1. faceting: adjoining certain reductions in valleys as rules
2. specialisation: adjoining rules in context,substitution as rules

I diagrammatic: every peak filled by local commutation diagrams if decreasing

take-aways from Newman 1942
I that rewriting is not about relations, but steps
I his lemma and its homotopic strengthening: for terminating and locally confluent
rewrite system all diagrams (cycles) deformable into the empty diagram (cf.
Squier 1987, Kraus & von Raumer 2020)
I diamond property and random descent (Toyama 1992, vO 2007, T & vO 2016)
I axiomatic residuals (Hindley, Glauert & Khasidashvili, Melliès, Terese)(↵-equivalence error in application to -calculus; but expect it applies to TRSs)
I interest in least upperbounds (left to future work; cf. orthogonality in term
rewriting or braids; faceting by least way to extend co-initial steps)