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
```
Patch Graph Rewriting
Roy Overbeek, and Jörg Endrullis
In: Proc. Conf. on Graph Transformation (ICGT 2020), pp. 128–145, Springer (2020)
summary paper bib doi

Summary

The basic principle of graph rewriting is the stepwise replacement of subgraphs inside a host graph. A challenge in such replacement steps is the treatment of the patch graph, consisting of those edges of the host graph that touch the subgraph, but are not part of it.
We introduce patch graph rewriting, a visual graph rewriting language with precise formal semantics. The language has rich expressive power in two ways. First, rewrite rules can flexibly constrain the permitted shapes of patches touching matching subgraphs. Second, rules can freely transform patches. We highlight the framework’s distinguishing features by comparing it against existing approaches.
Bibtex
```
@inproceedings{graph:rewriting:patch:2020,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  title = {Patch Graph Rewriting},
  booktitle = {Proc.\ Conf.\ on Graph Transformation (ICGT~2020)},
  series = {LNCS},
  volume = {12150},
  pages = {128--145},
  publisher = {Springer},
  year = {2020},
  doi = {10.1007/978-3-030-51372-6\_8},
  keywords = {rewriting},
  type = {conference}
}
```
Digital Object Identifier
```
10.1007/978-3-030-51372-6_8
```

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
```
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva
Logical Methods in Computer Science , 14 (1) (2018)
summary paper bib doi

Summary

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).
Bibtex
```
@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}
}
```
Digital Object Identifier
```
10.23638/LMCS-14(1:3)2018
```

2017

Clocked Lambda Calculus
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
Mathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)
summary paper bib doi

Summary

We introduce the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps. This calculus consists of the following two rules: \[ \begin{aligned} (\lambda x.M) N &\to \tau( M[x = N] ) \\ \tau(M)N &\to \tau(MN) \end{aligned} \] The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent, and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees), which we call clocked Böhm trees. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@article{clocked:lambda:calculus:2017,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
  title = {{Clocked Lambda Calculus}},
  journal = {Mathematical Structures in Computer Science},
  volume = {27},
  number = {5},
  pages = {782--806},
  year = {2017},
  doi = {10.1017/S0960129515000389},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}
```
Digital Object Identifier
```
10.1017/S0960129515000389
```

2015

Proving Non-Termination by Finite Automata
Jörg Endrullis, and Hans Zantema
In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 160–176, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
summary paper bib doi

Summary

We present a new technique to prove non-termination of term rewriting. The basic idea is tofind a non-empty regular language of terms that is weakly closed under rewriting and does not containnormal forms. It is automated by representing the language by a tree automaton with a fixednumber of states, and expressing the mentioned requirements in a SAT formula. Satisfiabilityof this formula implies non-termination. Our approach succeeds for many examples where allearlier techniques fail, for instance for the S-rule from combinatory logic.

See research for an overview of my research on termination.
Bibtex
```
@inproceedings{termination:automata:2015,
  author = {Endrullis, J\"{o}rg and Zantema, Hans},
  title = {{Proving Non-termination by Finite Automata}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2015)},
  volume = {36},
  pages = {160--176},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2015},
  doi = {10.4230/LIPIcs.RTA.2015.160},
  keywords = {rewriting, termination, automata},
  type = {conference}
}
```
Digital Object Identifier
```
10.4230/LIPIcs.RTA.2015.160
```
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning
Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva
In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 143–159, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
summary paper bib doi

Summary

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.

We refer to Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic (LMCS 2018) for an extended journal version of this paper.

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).
Bibtex
```
@inproceedings{infintary:rewriting:coinductive:2015,
  author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra},
  title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA 2015)},
  volume = {36},
  pages = {143--159},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2015},
  doi = {10.4230/LIPIcs.RTA.2015.143},
  keywords = {rewriting, infinitary rewriting, coinduction},
  type = {conference}
}
```
Digital Object Identifier
```
10.4230/LIPIcs.RTA.2015.143
```

2014

Discriminating Lambda-Terms Using Clocked Boehm Trees
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
Logical Methods in Computer Science , 10 (2) (2014)
summary paper bib doi
Summary

As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible. Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree. This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.

Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus, and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.

To prove such beta-inconvertibilities, we refine the concept of Böhm trees: we introduce clocked Böhm trees's with annotations that convey information of the tempo in which the Böhm trees are produced. Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms. An analogous approach pertains to Levy-Longo trees and Berarducci trees.

We illustrate applicability of our refined Böhm trees at the following examples:
- We show how to \( \beta \)-discriminate a large number of fixed-point combinators.
- We answer a question of Gordon Plotkin: Is there a fixed point combinator \( Y \) such that \[ Y ( \lambda z. f zz ) =_\beta Y ( \lambda x. Y ( \lambda y. f xy )) \]
We further increase the discrimination power of the technique by enhancing the precision of the clock, arriving at a notion that we call atomic clocks.

This paper is an extended version of Modular Construction of Fixed Point Combinators and Clocked Böhm Trees (LICS 2010).

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@article{lambda:clocks:2014,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
  title = {{Discriminating Lambda-Terms Using Clocked Boehm Trees}},
  journal = {Logical Methods in Computer Science},
  volume = {10},
  number = {2},
  year = {2014},
  doi = {10.2168/LMCS-10(2:4)2014},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}
```
Digital Object Identifier
```
10.2168/LMCS-10(2:4)2014
```

Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples

Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom

Logical Methods in Computer Science , 10 (2:7) , pp. 1–33 (2014)

paper bib doi

Bibtex

@article{infinitary:weakly:orthogonal:2014,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent},
  title = {{Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples}},
  journal = {Logical Methods in Computer Science},
  volume = {10},
  number = {2:7},
  pages = {1--33},
  year = {2014},
  doi = {10.2168/LMCS-10(2:7)2014},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}

Digital Object Identifier

10.2168/LMCS-10(2:7)2014

On the Complexity of Stream Equality

Jörg Endrullis, Dimitri Hendriks, Rena Bakhshi, and Grigore Rosu

Journal of Functional Programming , 24 (2-3) , pp. 166–217 (2014)

paper bib doi

Bibtex

@article{complexity:stream:equality:2014,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Bakhshi, Rena and Rosu, Grigore},
  title = {{On the Complexity of Stream Equality}},
  journal = {Journal of Functional Programming},
  volume = {24},
  number = {2-3},
  pages = {166--217},
  year = {2014},
  doi = {10.1017/S0956796813000324},
  keywords = {rewriting, undecidability, streams},
  type = {journal}
}

Digital Object Identifier

10.1017/S0956796813000324

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
```

SAT Compilation for Termination Proofs via Semantic Labelling

Alexander Bau, Jörg Endrullis, and Johannes Waldmann

In: Proc. Workshop on Termination (WST 2007) (2013)

paper bib

Bibtex

@inproceedings{termination:sat:compilation:2014,
  author = {Bau, Alexander and Endrullis, J\"{o}rg and Waldmann, Johannes},
  title = {{SAT compilation for Termination Proofs via Semantic Labelling}},
  booktitle = {Proc.\ Workshop on Termination (WST~2007)},
  year = {2013},
  keywords = {rewriting, termination},
  type = {workshop}
}

Digital Object Identifier

Clocks for Functional Programs
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
In: The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday, pp. 97–126, Springer (2013)
summary paper bib doi

Summary

The contribution of this paper is twofold.

First, we derive a complete characterization of all simply-typed fixed-point combinator (fpc) generators using Barendregt's Inhabitation Machines. A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is. The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator. For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]

Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators. Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \). This question remains open as the proof by Benedetto Intrigila contains a gap. We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:

Conjecture

We conjecture that for any fixed-point combinator \( Y \) and simply-typed \( \lambda\mu \)-terms \( s,t \) it holds that \[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \] where \(s_Y, t_Y\) are the untyped lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).

This conjecture immediately implies a negative answer to Statman's question.

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
```
@inproceedings{lambda:clocks:functional:programs:2013,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
  title = {{Clocks for Functional Programs}},
  booktitle = {The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday},
  pages = {97--126},
  year = {2013},
  doi = {10.1007/978-3-642-40355-2\_8},
  series = {LNCS},
  volume = {8106},
  publisher = {Springer},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}
```
Digital Object Identifier
```
10.1007/978-3-642-40355-2_8
```

Circular Coinduction in Coq Using Bisimulation-Up-To Techniques

Jörg Endrullis, Dimitri Hendriks, and Martin Bodin

In: Proc. Conf. on Interactive Theorem Proving (ITP 2013), pp. 354–369, Springer (2013)

paper bib doi

Bibtex

@inproceedings{circular:coinduction:2013,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Bodin, Martin},
  title = {{Circular Coinduction in Coq Using Bisimulation-Up-To Techniques}},
  booktitle = {Proc.\ Conf.\ on Interactive Theorem Proving (ITP~2013)},
  volume = {7998},
  pages = {354--369},
  publisher = {Springer},
  series = {LNCS},
  year = {2013},
  doi = {10.1007/978-3-642-39634-2\_26},
  keywords = {rewriting, coinduction, formal verification},
  type = {conference}
}

Digital Object Identifier

10.1007/978-3-642-39634-2_26

2012

Automatic Sequences and Zip-Specifications

Clemens Grabmayer, Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Lawrence S. Moss

In: Proc. Symp. on Logic in Computer Science (LICS 2012), pp. 335–344, IEEE Computer Society (2012)

paper bib doi

Bibtex

@inproceedings{streams:zip:2012,
  author = {Grabmayer, Clemens and Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Moss, Lawrence S.},
  title = {{Automatic Sequences and Zip-Specifications}},
  booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2012)},
  pages = {335--344},
  publisher = {{IEEE} Computer Society},
  year = {2012},
  doi = {10.1109/LICS.2012.44},
  keywords = {rewriting, streams, automata},
  type = {conference}
}

Digital Object Identifier

10.1109/LICS.2012.44

Highlights in Infinitary Rewriting and Lambda Calculus

Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop

Theoretical Computer Science , 464 , pp. 48–71 (2012)

paper bib doi

Bibtex

@article{infinitary:highlights:2012,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
  title = {{Highlights in Infinitary Rewriting and Lambda Calculus}},
  journal = {Theoretical Computer Science},
  volume = {464},
  pages = {48--71},
  year = {2012},
  doi = {10.1016/j.tcs.2012.08.018},
  keywords = {rewriting, infinitary rewriting, lambda calculus},
  type = {journal}
}

Digital Object Identifier

10.1016/j.tcs.2012.08.018

On the Complexity of Equivalence of Specifications of Infinite Objects

Jörg Endrullis, Dimitri Hendriks, and Rena Bakhshi

In: Proc. Int. Conf. on Functional Programming (ICFP 2012), pp. 153–164, ACM (2012)

paper bib doi

Bibtex

@inproceedings{complexity:stream:equality:2012,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Bakhshi, Rena},
  title = {{On the Complexity of Equivalence of Specifications of Infinite Objects}},
  booktitle = {Proc.\ Int.\ Conf.\ on Functional Programming (ICFP~2012)},
  pages = {153--164},
  publisher = {{ACM}},
  year = {2012},
  doi = {10.1145/2364527.2364551},
  keywords = {rewriting, undecidability, streams},
  type = {conference}
}

Digital Object Identifier

10.1145/2364527.2364551

2011

2010

2009

2008

2007

Productivity of Stream Definitions
Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem Klop
In: Proc. Symp. on Fundamentals of Computation Theory (FCT 2007), pp. 274–287, Springer (2007)
summary paper bib doi

Summary

We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called `productive' if it can be evaluated continually in such a way that a uniquely determined stream in constructor normal form is obtained as the limit. Whereas productivity is undecidable for stream definitions in general, we show that it can be decided for `pure' stream definitions. For every pure stream definition the process of its evaluation can be modelled by the dataflow of abstract stream elements, called `pebbles', in a finite `pebbleflow net(work)'. And the production of a pebbleflow net associated with a pure stream definition, that is, the amount of pebbles the net is able to produce at its output port, can be calculated by reducing nets to trivial nets.

An extended journal version of this paper is available from Productivity of Stream Definitions (TCS 2010).

See research for an overview of my research on productivity.
Bibtex
```
@inproceedings{productivity:streams:2007,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Isihara, Ariya and Klop, Jan Willem},
  title = {{Productivity of Stream Definitions}},
  booktitle = {Proc.\ Symp.\ on Fundamentals of Computation Theory (FCT~2007)},
  number = {4639},
  pages = {274--287},
  publisher = {Springer},
  series = {LNCS},
  year = {2007},
  doi = {10.1007/978-3-540-74240-1\_24},
  keywords = {rewriting, infinitary rewriting, productivity},
  type = {conference}
}
```
Digital Object Identifier
```
10.1007/978-3-540-74240-1_24
```

Root Stabilisation Using Dependency Pairs

Jörg Endrullis, and Jeroen Ketema

In: Proc. Workshop on Termination (WST 2007), pp. 17–21 (2007)

paper bib

Bibtex

@inproceedings{termination:root:2007,
  author = {Endrullis, J\"{o}rg and Ketema, Jeroen},
  title = {{Root Stabilisation Using Dependency Pairs}},
  booktitle = {Proc.\ Workshop on Termination (WST~2007)},
  pages = {17--21},
  year = {2007},
  keywords = {rewriting, infinitary rewriting, termination},
  type = {workshop}
}

Digital Object Identifier

2006

Matrix Interpretations for Proving Termination of Term Rewriting
Jörg Endrullis, Johannes Waldmann, and Hans Zantema
In: Proc. Int. Joint Conf. on Automated Reasoning (IJCAR 2006), pp. 574–588, Springer (2006)
summary paper bib doi

Summary

We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights). It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular non-total well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows to prove termination and relative termination. A modification of the latter in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation.
By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. Our implementation performs well on the Termination Problem Data Base: better than 5 out of 6 tools that participated in the 2005 termination competition in the category of term rewriting.

An extended journal version of this paper is available from Matrix Interpretations for Proving Termination of Term Rewriting (Journal of Automated Reasoning 2008).

See research for an overview of my research on termination.
Bibtex
```
@inproceedings{termination:matrix:2006,
  author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans},
  title = {{Matrix Interpretations for Proving Termination of Term Rewriting}},
  booktitle = {Proc.\ Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2006)},
  volume = {4130},
  pages = {574--588},
  publisher = {Springer},
  series = {LNCS},
  year = {2006},
  doi = {10.1007/11814771\_47},
  keywords = {rewriting, termination, automata},
  type = {conference}
}
```
Digital Object Identifier
```
10.1007/11814771_47
```
Decomposing Terminating Rewrite Relations
Jörg Endrullis, Dieter Hofbauer, and Johannes Waldmann
In: Proc. Workshop on Termination (WST 2006), pp. 39–43 (2006)
summary paper bib
Summary

In this paper we are concerned with automatically proving termination of string rewriting systems (or word rewriting systems). We introduce an efficient technique for constructing automata that serve as certificates of match-boundedness, and thereby termination. Previously constructions have either been inefficient or incomplete:
- Match-Bounded String Rewriting Systems by Alfons Geser, Dieter Hofbauer and Johannes Waldmann. The construction in this paper is complete but very inefficient.
- On tree automata that certify termination of left-linear term rewriting systems by Alfons Geser, Dieter Hofbauer, Johannes Waldmann and Hans Zantema. The construction in this paper is efficient but incomplete.
See research for an overview of my research on termination.
Bibtex
```
@inproceedings{termination:matchbounds:2006,
  author = {Endrullis, J\"{o}rg and Hofbauer, Dieter and Waldmann, Johannes},
  title = {{Decomposing Terminating Rewrite Relations}},
  booktitle = {Proc.\ Workshop on Termination (WST~2006)},
  pages = {39--43},
  year = {2006},
  keywords = {rewriting, termination, automata},
  type = {workshop}
}
```
Digital Object Identifier

2020

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

2019

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

2018

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

2017

Summary

Bibtex

Digital Object Identifier

2015

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

2014

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

2013

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

2012

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

2011

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

Summary

Bibtex

Digital Object Identifier

2010

Summary

Bibtex

Digital Object Identifier

Bibtex

Digital Object Identifier

Summary

Bibtex