Publications on Confluence

2020

Decreasing Diagrams for Confluence and Commutation
Jörg Endrullis, Jan Willem Klop, and Roy Overbeek
Logical Methods in Computer Science , Volume 16, Issue 1 (2020)
summary paper bib doi

Summary

Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be used to obtain such a hierarchy.
The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract rewrite systems. It is complete for countable systems, and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps with labels from a well-founded order in order to conclude confluence of the underlying unlabelled relation. Hence it is natural to ask how the size of the label set influences the strength of the technique. In particular, what class of abstract rewrite systems can be proven confluent using decreasing diagrams restricted to 1 label, 2 labels, 3 labels, and so on?
Surprisingly, we find that two labels suffice for proving confluence for every abstract rewrite system having the cofinality property, thus in particular for every confluent, countable system. Secondly, we show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse.
Thirdly, investigating the possibility of a confluence hierarchy, we determine the first-order (non-)definability of the notion of confluence and related properties, using techniques from finite model theory. We find that in particular Hanf's theorem is fruitful for elegant proofs of undefinability of properties of abstract rewrite systems.

This paper is an extended version of Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems (FSCD 2018).

See research for an overview of my research on confluence.
Bibtex
```
@article{confluence:decreasing:diagrams:2020,
  title = {{Decreasing Diagrams for Confluence and Commutation}},
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Overbeek, Roy},
  doi = {10.23638/LMCS-16(1:23)2020},
  journal = {{Logical Methods in Computer Science}},
  volume = {{Volume 16, Issue 1}},
  year = {2020},
  keywords = {rewriting, confluence},
  type = {journal}
}
```
Digital Object Identifier
```
10.23638/LMCS-16(1:23)2020
```

2019

Confluence of the Chinese Monoid
Jörg Endrullis, and Jan Willem Klop
In: The Art of Modelling Computational Systems, pp. 206–220, Springer (2019)
summary paper bib doi

Summary

The Chinese monoid, related to Knuth’s Plactic monoid, is of great interest in algebraic combinatorics. Both are ternary monoids, generated by relations between words of three symbols. The relations are, for a totally ordered alphabet, if cba = cab = bca if a ≤ b ≤ c. In this note we establish confluence by tiling for the Chinese monoid, with the consequence that every two words u, v have extensions to a common word: ∀ u,v. ∃ x,y. ux = vy.
Our proof is given using decreasing diagrams, a method for obtaining confluence that is central in abstract rewriting theory. Decreasing diagrams may also be applicable to various related monoid presentations.
We conclude with some open questions for the monoids considered.

See research for an overview of my research on confluence.
Bibtex
```
@inproceedings{confluence:chinese:monoid:2019,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem},
  title = {{Confluence of the Chinese Monoid}},
  booktitle = {The Art of Modelling Computational Systems},
  series = {LNCS},
  volume = {11760},
  pages = {206--220},
  publisher = {Springer},
  year = {2019},
  doi = {10.1007/978-3-030-31175-9\_12},
  keywords = {rewriting,confluence},
  type = {conference}
}
```
Digital Object Identifier
```
10.1007/978-3-030-31175-9_12
```
Braids via Term Rewriting
Jörg Endrullis, and Jan Willem Klop
Theoretical Computer Science , 777 , pp. 260–295 (2019)
summary paper bib doi

Summary

We present a brief introduction to braids, in particular simple positive braids, with a double emphasis: first, we focus on term rewriting techniques, in particular, reduction diagrams and decreasing diagrams. The second focus is our employment of the colored braid notation next to the more familiar Artin notation. Whereas the latter is a relative, position dependent, notation, the former is an absolute notation that seems more suitable for term rewriting techniques such as symbol tracing. Artin's equations translate in this notation to simple word inversions. With these points of departure we treat several basic properties of positive braids, in particular related to the word problem, confluence property, projection equivalence, and the congruence property. In our introduction the beautiful diamond known as the permutohedron plays a decisive role.
Bibtex
```
@article{rewriting:braids:2019,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem},
  title = {Braids via term rewriting},
  journal = {Theoretical Computer Science},
  volume = {777},
  pages = {260--295},
  year = {2019},
  doi = {10.1016/j.tcs.2018.12.006},
  keywords = {rewriting,confluence},
  type = {journal}
}
```
Digital Object Identifier
```
10.1016/j.tcs.2018.12.006
```

2018

Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems
Jörg Endrullis, Jan Willem Klop, and Roy Overbeek
In: Proc. Conf. on Formal Structures for Computation and Deduction (FSCD 2018), pp. 14:1–14:15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
summary paper bib doi

Summary

The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract reduction systems. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps.

In this paper we investigate how the size of the label set influences the strength of the technique. Surprisingly, we find that two labels suffice for proving confluence of every confluent, countable system. In contrast, for proving commutation of rewrite relations, it turns out that the strength of the technique increases with more labels.

While decreasing diagrams is complete for proving confluence of countable systems, the technique is not complete for commutation. In our paper De Bruijn's Weak Diamond Property Revisited we give a counterexample to the completeness of decreasing diagrams for commutation.

See research for an overview of my research on confluence.
Bibtex
```
@inproceedings{confluence:decreasing:diagrams:2018,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Overbeek, Roy},
  title = {{Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems}},
  booktitle = {Proc.\ Conf.\ on Formal Structures for Computation and Deduction (FSCD~2018)},
  volume = {108},
  pages = {14:1--14:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2018},
  doi = {10.4230/LIPIcs.FSCD.2018.14},
  keywords = {rewriting, confluence},
  type = {conference}
}
```
Digital Object Identifier
```
10.4230/LIPIcs.FSCD.2018.14
```

2013

De Bruijn’s Weak Diamond Property Revisited
Jörg Endrullis, and Jan Willem Klop
Indagationes Mathematicae , 24 (4) , pp. 1050–1072 (2013)
summary paper bib doi

Summary

In this paper we revisit an unpublished but influential technical report from 1978 by N.G. de Bruijn, written in the framework of the Automath project. This report describes a technique for proving confluence of abstract reduction systems, called the weak diamond property. It paved the way for the powerful technique developed by Van Oostrom to prove confluence of abstract reduction systems, called decreasing diagrams.
We first revisit in detail De Bruijn’s old proof, providing a few corrections and hints for understanding. We find that this original criterion and proof technique are still worthwhile. Next, we establish that De Bruijn’s confluence criterion can be used to derive the decreasing diagrams theorem (the reverse was already known). We also provide a short proof of decreasing diagrams in the spirit of De Bruijn. We finally address the issue of completeness of this method.

See research for an overview of my research on confluence.
Bibtex
```
@article{confluence:weak:diamond:2013,
  author = {Endrullis, J\"{o}rg and Klop, Jan Willem},
  title = {{De Bruijn’s Weak Diamond Property Revisited}},
  journal = {Indagationes Mathematicae},
  volume = {24},
  number = {4},
  pages = {1050 -- 1072},
  year = {2013},
  doi = {10.1016/j.indag.2013.08.005},
  note = {In memory of N.G. (Dick) de Bruijn (1918–2012)},
  keywords = {rewriting, confluence},
  type = {journal}
}
```
Digital Object Identifier
```
10.1016/j.indag.2013.08.005
```

2011

Levels of Undecidability in Rewriting
Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans Zantema
Information and Computation , 209 (2) , pp. 227–245 (2011)
summary paper bib doi

Summary

Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.

In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.

Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.

This paper is an extended version of Degrees of Undecidability in Term Rewriting (CSL 2009).
Bibtex
```
@article{rewriting:undecidability:levels:2011,
  author = {Endrullis, J\"{o}rg and Geuvers, Herman and Simonsen, Jakob Grue and Zantema, Hans},
  title = {{Levels of Undecidability in Rewriting}},
  journal = {Information and Computation},
  volume = {209},
  number = {2},
  pages = {227--245},
  year = {2011},
  doi = {10.1016/j.ic.2010.09.003},
  keywords = {rewriting, undecidability, termination, confluence},
  type = {journal}
}
```
Digital Object Identifier
```
10.1016/j.ic.2010.09.003
```

2009

Degrees of Undecidability in Term Rewriting
Jörg Endrullis, Herman Geuvers, and Hans Zantema
In: Proc. Conf. on Computer Science Logic (CSL 2009), pp. 255–270, Springer (2009)
summary paper bib doi

Summary

Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.

In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.

Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.

We refer to Levels of Undecidability in Rewriting (Information and Computation 2011) for an extended journal version of this paper.
Bibtex
```
@inproceedings{rewriting:undecidability:degrees:2009,
  author = {Endrullis, J\"{o}rg and Geuvers, Herman and Zantema, Hans},
  title = {{Degrees of Undecidability in Term Rewriting}},
  booktitle = {Proc.\ Conf.\ on Computer Science Logic (CSL~2009)},
  volume = {5771},
  pages = {255--270},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-04027-6\_20},
  keywords = {rewriting, undecidability, termination, confluence},
  type = {conference}
}
```
Digital Object Identifier
```
10.1007/978-3-642-04027-6_20
```

2020

Summary

Bibtex

Digital Object Identifier

2019

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

2018

Summary

Bibtex

Digital Object Identifier

2013

Summary

Bibtex

Digital Object Identifier

2011

Summary

Bibtex

Digital Object Identifier

2009

Summary

Bibtex

Digital Object Identifier