Barendregt's Lemma
Abstract
Barendregt’s Lemma in its original form is a statement on Combinatory Logic that holds also for the lambda calculus and gives important insight into the syntactic interplay between substitution and reduction. Its origin lies in undefinablity proofs, but there are other applications as well. It is connected to the so-called Square Brackets Lemma, introduced by van Daalen in proofs of strong normalization of typed lambda calculi and of the Hyland–Wadsworth labelled lambda calculus. In the generalization of the latter result to higher-order rewriting systems, finite family developments, van Oostrom introduced the property “Invert”, which is also related.
In this short note we state the lemma, try to put it in perspective, and discuss the mentioned connections. We also present a yet unpublished alternative proof of SN of the Hyland–Wadsworth labelled lambda calculus, using a computability argument.
Full text