# Difference between beta reduction and substitution

I can not see the difference between beta reduction and substitution.

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) 2


the result would be

+ 2 1


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

(λ 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) 2


and

(λ x. + x 1) [x -> 2]

• Note: Is x a metavariable? – nekketsuuu Feb 3 '17 at 11:26
• You seem to be confusing application with substitution. Application is part of the lambda-calculus syntax, substitution is not. Substitution lives in the "math world" of the theory which defines the calculus semantics, but is not a notation which can be used by the "lambda programmer", so to speak. Perhaps confusingly, it is a meta operator which modifies the syntax, so it is written next to lambda-terms to operate on them. E.g. I can define an operator $c(P)$ which given a C program $P$, returns the C program $P$ after incrementing constants in it. Then, $c$ is not part of the C language. – chi Feb 3 '17 at 11:58
• I did not get what you mean. – zero_coding Feb 3 '17 at 12:31

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

• I think @chi's comment is very nice! Please check it too :) – nekketsuuu Feb 3 '17 at 12:15
• Just to muddy the waters, there are lambda calculi with explicit substitutions for which substitution is an object language level operation (as opposed to a meta-operation). In those, a single step of $\beta$-reduction will produce an explicit substitution which is unequivocally distinct from the redex. (Note, it is not necessarily the case that $(\lambda x.M)N \neq M[x\mapsto N]$ in the normal (non-explicit substitution) lambda calculus, though it usually is.) – Derek Elkins left SE Feb 3 '17 at 23:54
• @DerekElkins Is there any variant of the λ-calculus without explicit substitution which treats $(\lambda x. M)N = M[x \mapsto N]$ (syntactically)? If so, I think β-reductions would be unnecessary in the calculus. – nekketsuuu Feb 5 '17 at 0:33
• @nekketsuuu I'm not quite sure what you mean. It sounds like you want to consider two terms equal if they are $\beta$-equivalent. This would kind of defeat the point. Also as $\beta$-equivalence is undecidable, this would be awkward. But maybe Böhm trees would interest you(?) – Derek Elkins left SE Feb 7 '17 at 4:39
• @DerekElkins Oh I misunderstood about the last sentence of your comment. Thank you. – nekketsuuu Feb 7 '17 at 10:12