gotchaMinor
Difference between beta reduction and substitution
Viewed 0 times
substitutionbetadifferencebetweenreductionand
Problem
I can not see the difference between beta reduction and substitution.
For example:
Here I can do the substitution, replace the variable x through 2(lambda expression) and result is:
An example of beta reduction:
the result would be
For me, there are no difference between them, but there is a rule, I can not substitute the lambda expression, when the metavariable is bound
Only free variables can be substitute it.
What is the difference between the diction:
and
For example:
(+ x 1) [x -> 2]Here I can do the substitution, replace the variable x through 2(lambda expression) and result is:
(+ 2 1)An example of beta reduction:
(λ x. + x 1) 2the result would be
+ 2 1For me, there are no difference between them, but there is a rule, I can not substitute the lambda expression, when the metavariable is bound
(λ x. + x 1) [x -> 2] No possible to substitute it.Only free variables can be substitute it.
What is the difference between the diction:
(λ x. + x 1) 2and
(λ x. + x 1) [x -> 2]Solution
The $\beta$ reduction is defined by using capture-avoidng substitution. That is,
$$
(\lambda x. M)N \longrightarrow_\beta M[x \mapsto N]
$$
So it's the definition. Under the $\beta$-equivalence, $(\lambda x. M)N \equiv_\beta M[x \mapsto N]$, but syntactically, $(\lambda x. M)N \neq M[x \mapsto N]$.
Note that substitution is a meta-operation on $\lambda$-calculus terms (normally).
A $\lambda$-calculus term $M$ is whether a variable $x$,
a lambda abstraction $(\lambda x. M')$, or an application $M_1 M_2$.
That's it.
There is no substitution.
Substitution is a map on $\lambda$-calculus terms.
Therefore, for example, a term $({+}~x~y)[x \mapsto z]$ is syntactically equal to $({+}~z~y)$.
There is no reduction.
In contrast to this, $(\lambda x. {+}~x~y)~z$ is not syntactically equal to $({+}~z~y)$, although it can be reduced to $({+}~x~y)$.
Also, $(\lambda x. {+}~x~1)~2$ is different from $(\lambda x. {+}~x~1)[x \mapsto 2]$. The latter is equal to $(\lambda x. {+}~x~1)$.
$$
(\lambda x. M)N \longrightarrow_\beta M[x \mapsto N]
$$
So it's the definition. Under the $\beta$-equivalence, $(\lambda x. M)N \equiv_\beta M[x \mapsto N]$, but syntactically, $(\lambda x. M)N \neq M[x \mapsto N]$.
Note that substitution is a meta-operation on $\lambda$-calculus terms (normally).
A $\lambda$-calculus term $M$ is whether a variable $x$,
a lambda abstraction $(\lambda x. M')$, or an application $M_1 M_2$.
That's it.
There is no substitution.
Substitution is a map on $\lambda$-calculus terms.
Therefore, for example, a term $({+}~x~y)[x \mapsto z]$ is syntactically equal to $({+}~z~y)$.
There is no reduction.
In contrast to this, $(\lambda x. {+}~x~y)~z$ is not syntactically equal to $({+}~z~y)$, although it can be reduced to $({+}~x~y)$.
Also, $(\lambda x. {+}~x~1)~2$ is different from $(\lambda x. {+}~x~1)[x \mapsto 2]$. The latter is equal to $(\lambda x. {+}~x~1)$.
Context
StackExchange Computer Science Q#69790, answer score: 6
Revisions (0)
No revisions yet.