# Publications in 2018

## 2018

- Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable SystemsJörg Endrullis, Jan Willem Klop, and Roy OverbeekIn: Proc. Conf. on Formal Structures for Computation and Deduction (FSCD 2018), pp. 14:1–14:15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
# Abstract

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.

@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} }

- Coinductive Foundations of Infinitary Rewriting and Infinitary Equational LogicJörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra SilvaLogical Methods in Computer Science , 14 (1) (2018)
# Abstract

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.

The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework suitable for formalizations in theorem provers. To wit, we provide the first formalization of the compression lemma in Coq.

This paper is an extended version of A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (RTA 2015). We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).

@article{infintary:rewriting:coinductive:2018, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic}}, journal = {Logical Methods in Computer Science}, volume = {14}, number = {1}, year = {2018}, doi = {10.23638/LMCS-14(1:3)2018}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {journal} }