Church-Rosser λ-theories, Infinite λ-terms and Consistency Problems
Alessandro Berarducci, Benedetto Intrigila · 1996
Abstract We treat a general technique to obtain Church-Rosser extensions of the λβ-calculus, based on the notion of “confining class” and on an infinitary version of λ-calculus. We apply the technique to find a large class of terms which can be consistently equated to every other term, and we also show that many equations between λ-terms can be consistently added to the the λβ--calculus.