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

CC BY-SA 4.0
2020-07-01T09:53:36.000Z
2020-07-01T09:53:36.000Z
Natalie Clarius
<p>Suppose we have the following typed lambda term (where <span class="math-container">$s$</span> does not occur in E (which is of type <span class="math-container">$s \to p$</span>) and <span class="math-container">$s$</span> and <span class="math-container">$s'$</span> have the same type), and want to apply <span class="math-container">$\beta$</span>-reduction:</p>
<p><span class="math-container">$(\lambda s. E)\, s'$</span></p>
<p>Every occurrence of <span class="math-container">$s$</span> in E must be replaced with <span class="math-container">$s'$</span>. But suppose there are no occurrences of <span class="math-container">$s$</span> in <span class="math-container">$E$</span>. In this case, does beta reduction lead to (1) or to (2)?</p>
<p>(1) <span class="math-container">$E$</span></p>
<p>(2) <span class="math-container">$E\, s'$</span></p>
<p>I can't see how this is fixed by the definition of beta-reduction.</p>
<hr />
<p>Edit</p>
<p>I have completely rewritten the question to make it clearer.</p>

CC BY-SA 4.0
2020-07-01T07:39:38.833Z
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
CC BY-SA 4.0
2020-07-01T08:47:54.573Z
(3) None of the above.
Andrej Bauer
CC BY-SA 4.0
2020-07-01T09:16:38.030Z
@Noam Zeilberger I have  completely rewritten the question to make it much clearer.
Joe
CC BY-SA 4.0
2020-07-01T09:21:51.867Z
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
CC BY-SA 4.0
2020-07-01T09:22:54.893Z
@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
CC BY-SA 4.0
2020-07-01T10:31:38.453Z
Yes sorry, I'm not an expert, I'm not sure if what I say is accurate. But I meant that a lambda term is a variable, a lambda or an application, and E is none of those.
Labbekak
CC BY-SA 4.0
2020-07-01T12:32:06.280Z
@Labbekak: If $a: \alpha$ and $x: \beta$, then $\lambda x. a: \beta \to \alpha$ is a term in the simply typed lambda calculus. So $\lambda s. E.$ is a term.
Joe
CC BY-SA 4.0
2020-07-01T21:44:19.317Z
Was the question closed because it is not "research-level"? So it would have been ok to ask this on math stack exchange instead?
Joe
<lambda-calculus><typed-lambda-calculus>
Beta reduction and vacuous lambda abstraction
Joe
# Beta reduction and vacuous lambda abstraction

(Asked by: username_0 on 2020-07-01)

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.

**Tags:** lambda-calculus, typed-lambda-calculus

> **Comments:**
> **username_1**: 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$).  
> **username_2**: (3) None of the above.  
> **username_0**: @username_1 I have  completely rewritten the question to make it much clearer.  
> **username_3**: 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.  
> **username_0**: @username_3 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?  
> **username_3**: Yes sorry, I'm not an expert, I'm not sure if what I say is accurate. But I meant that a lambda term is a variable, a lambda or an application, and E is none of those.  
> **username_0**: @username_3: If $a: \alpha$ and $x: \beta$, then $\lambda x. a: \beta \to \alpha$ is a term in the simply typed lambda calculus. So $\lambda s. E.$ is a term.  
> **username_0**: Was the question closed because it is not "research-level"? So it would have been ok to ask this on math stack exchange instead?  

---

## 1 answers

### Answer by username_4 on 2020-07-01. Score: -1 | Accepted answer

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$.


---

