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

---

Transforming Outermost into Context-Sensitive Rewriting

Joerg Endrullis ; Dimitri Hendriks.

We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on 'context extension', each outermost rewrite step is modeled by exactly&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;]

---