Search

• < Previous
• 1
• Next >

---

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

---

Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture

Benedetto Intrigila ; Giulio Manzonetto ; Andrew Polonsky.

The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between B\"ohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two lambda-terms whenever their B\"ohm trees&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;]

---