# Beta reduction and vacuous lambda abstraction [closed]

Suppose we have the following typed lambda term (where $$s$$ does not occur in E (which is of type $$s \to p$$) and $$s$$ and $$s'$$ have the same type), and want to apply $$\beta$$-reduction:

$$(\lambda s. E)\, s'$$

Every occurrence of $$s$$ in E must be replaced with $$s'$$. But suppose there are no occurrences of $$s$$ in $$E$$. In this case, does beta reduction lead to (1) or to (2)?

(1) $$E$$

(2) $$E\, s'$$

I can't see how this is fixed by the definition of beta-reduction.

Edit

I have completely rewritten the question to make it clearer.

• what is $\delta$, and how are you parenthesizing the applications? If $\delta$ is a variable/constant and you are using the usual convention where application is left-associative $((\delta\ y)\ (\lambda s.E))\ s'$ then there is no beta redex, i.e., the term is already in normal form (other than any beta redices that might occur in $M$). – Noam Zeilberger Jul 1 at 7:39
• (3) None of the above. – Andrej Bauer Jul 1 at 8:47
• @Noam Zeilberger I have completely rewritten the question to make it much clearer. – Joe Jul 1 at 9:16
• Well beta reduction is defined on lambda terms, E is not a lambda term but a meta variable. But we can proof that for any lambda term E, your term reduces to E. – Labbekak Jul 1 at 9:21
• @Labbekak In what sense is $E_{s \to p}$ not a lambda term? I'm just supposing $E$ is an arbitrary constant of type $s \to p$. It's not a term formed via lambda abstraction, is that all you mean? – Joe Jul 1 at 9:22

Substitution means replacement, not attachment. If there are no occurrences of $$s$$ to replace, then nothing will be replaced. So the answer is (1).
This follows unambiguously from the definition of substitution. The substitution $$[s'/s]$$ is recursively passed into the subterms of $$E$$, until the level of atoms (= constants and variables) is reached and the substitution is applied to each symbol. When the symbol is the variable $$s$$, it will get replaced by $$s'$$; when it is a different variable or a constant, it will remain unchanged, according to the definition of substitution. If all atomic symbols in $$E$$ are different from $$s$$, then at the end of the substitutoin operation no replacement will have happened, and the result is just $$E$$.