Search

• < Previous
• 1
• Next >

---

Decreasing Diagrams for Confluence and Commutation

Jörg Endrullis ; Jan Willem Klop ; Roy Overbeek.

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&nbsp;[&hellip;]

---

Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

Jörg Endrullis ; Helle Hvid Hansen ; Dimitri Hendriks ; Andrew Polonsky ; Alexandra Silva.

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 setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence.&nbsp;[&hellip;]

---

Star Games and Hydras

Jörg Endrullis ; Jan Willem Klop ; Roy Overbeek.

The recursive path ordering is an established and crucial tool in term rewriting to prove termination. We revisit its presentation by means of some simple rules on trees (or corresponding terms) equipped with a 'star' as control symbol, signifying a command to make that tree (or term) smaller in the&nbsp;[&hellip;]

---

Termination of Graph Transformation Systems Using Weighted Subgraph Counting

Roy Overbeek ; Jörg Endrullis.

We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which include toposes and therefore many graph categories of interest),&nbsp;[&hellip;]

---