A Problem on Easy Terms in λ-Calculus
Benedetto Intrigila · Fundamenta Informaticae · 1991
We say that a closed term M is easy in the λ β η-calculus if for every term N the theory λ β η + { M = N } is consistent. The main result of the paper is to show that, for a certain term P, the term P( ω ω) is easy, while P ω is not. It follows that the easiness of a given M does not imply either easiness or non-easiness of PM, contradicting an earlier conjecture.