Some new results on easy lambda-terms (Q1314346): Difference between revisions

This paper is devoted to easy terms, that is \(\lambda\)-terms \(X\) such that for each \(\lambda\)-term \(Y\) the equation \(X= Y\) is consistent. Two methods are used for investigating such terms. First a sufficient condition for the consistency of certain equations \(X= Y\) is given, based on some Church-Rosser extensions of the \(\lambda\)-calculus. Then, the use of continuity properties of Böhm trees provides a means to ensure the above sufficient condition. The authors exploit these tools to give examples of easiness, investigate the more general notion of ``normal form easiness'', and provide a very detailed study of the relations between the two notions.