Search

• < Previous
• 1
• Next >

---

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

---

Fixed point combinators as fixed points of higher-order fixed point generators

Andrew Polonsky.

Corrado B\"ohm once observed that if $Y$ is any fixed point combinator (fpc), then $Y(\lambda yx.x(yx))$ is again fpc. He thus discovered the first "fpc generating scheme" -- a generic way to build new fpcs from old. Continuing this idea, define an $\textit{fpc generator}$ to be any sequence of&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;]

---

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

---

On sets of terms having a given intersection type

Andrew Polonsky ; Richard Statman.

Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair&nbsp;[&hellip;]

---