Next: Synthesis of (lambda(f) ...)
Up: Multiplication of the numbers
Previous: Substitution of `two' and
Here we have a conflict between a free and a lambda-bound variable which has to
be dissolved by applying alpha-conversion.
The variables concerned are the lambda-bound variable `x' and the variable `x'
of the outer environment.
According to the rule for alpha-conversion in the lambda-calculus the lambda-bound
variable in such a conflict has to be renamed. We have renamed `x' into `x0'.
Having applied alpha-conversion the synthesis can be done.
Georg P. Loczewski