-2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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$). $\endgroup$ – Noam Zeilberger Jul 1 at 7:39
  • $\begingroup$ (3) None of the above. $\endgroup$ – Andrej Bauer Jul 1 at 8:47
  • $\begingroup$ @Noam Zeilberger I have completely rewritten the question to make it much clearer. $\endgroup$ – Joe Jul 1 at 9:16
  • $\begingroup$ 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. $\endgroup$ – Labbekak Jul 1 at 9:21
  • $\begingroup$ @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? $\endgroup$ – Joe Jul 1 at 9:22
-1
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.