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

---

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

---