Reduction Under Substitution

Abstract

The Reduction-under-Substitution Lemma (RuS) , due to van Daalen [Daa80] , provides an answer to the following question concerning the lambda calculus: given a reduction $M[{x}:={L}] \twoheadrightarrow N$, what can we say about the contribution of the substitution to the result N. It is related to a not very well-known lemma that was conjectured by Barendregt in the early 70’s, addressing the similar question as to the contribution of the argument M in a reduction $FM \twoheadrightarrow N$. The origin of Barendregt’s Lemma lies in undefinablity proofs, whereas van Daalen’s interest came from its application to the so-called Square Brackets Lemma, which is used in proofs of strong normalization.

In this paper we compare various forms of RuS. We strengthen RuS to multiple substitution and context filling and show how it can be used to give short and perspicuous proofs of undefinability results. Most of these are known as consequences of Berry’s Sequentiality Theorem, but some fall outside its scope. We show that RuS can also be used to prove the sequentiality theorem itself. To that purpose we give a further adaptation of RuS, now also involving “bottom” reduction rules, sending unsolvable terms to a bottom element and in the limit producing Böhm trees.