Search

• < Previous
• 1
• Next >

---

Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples

Joerg Endrullis ; Clemens Grabmayer ; Dimitri Hendriks ; Jan Willem Klop ; Vincent van Oostrom.

We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing&nbsp;[&hellip;]

---

Discriminating Lambda-Terms Using Clocked Boehm Trees

Joerg Endrullis ; Dimitri Hendriks ; Jan Willem Klop ; Andrew Polonsky.

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 Boehm Trees are inadequate when we deal with terms having the same Boehm Tree (BT). This is the case in particular for fixed&nbsp;[&hellip;]

---

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;]

---

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;]

---