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]
x
a metavariable? $\endgroup$ – nekketsuuu Feb 3 '17 at 11:26