Next: Synthesis of (lambda(f) ...)
Up: Multiplication of the numbers
Previous: Substitution of `two' and
Contents
Start
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'.
![\begin{lstlisting}[language=Scm]{}
(lambda(x)
((lambda(f)
(lambda(x)
(f(f x))))
((lambda(f)
(lambda(x0)
(f(f(f x0)))))
x))) [27]
\end{lstlisting}](img215.gif)
Having applied alpha-conversion the synthesis can be done.
![\begin{lstlisting}[language=Scm]{}
(lambda(x)
((lambda(f)
(lambda(x)
(f(f x))))
(lambda(x0)
(x(x(x x0)))))) [28]
\end{lstlisting}](img216.gif)
Georg P. Loczewski
2004-03-05