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


(λ x. + x 1) [x -> 2]
  • $\begingroup$ Note: Is x a metavariable? $\endgroup$ – nekketsuuu Feb 3 '17 at 11:26
  • 4
    $\begingroup$ 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. $\endgroup$ – chi Feb 3 '17 at 11:58
  • $\begingroup$ I did not get what you mean. $\endgroup$ – 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)$.

| cite | improve this answer | |
  • $\begingroup$ I think @chi's comment is very nice! Please check it too :) $\endgroup$ – nekketsuuu Feb 3 '17 at 12:15
  • 1
    $\begingroup$ 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.) $\endgroup$ – Derek Elkins left SE Feb 3 '17 at 23:54
  • $\begingroup$ @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. $\endgroup$ – nekketsuuu Feb 5 '17 at 0:33
  • $\begingroup$ @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(?) $\endgroup$ – Derek Elkins left SE Feb 7 '17 at 4:39
  • $\begingroup$ @DerekElkins Oh I misunderstood about the last sentence of your comment. Thank you. $\endgroup$ – nekketsuuu Feb 7 '17 at 10:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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