next up previous contents index
Next: Synthesis of (lambda(f) ...) Up: Multiplication of the numbers Previous: Substitution of `two' and   Contents   Index

Synthesis of the inner (lambda(f) ...) and `x' in [26]

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}

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}


domain access counter Georg P. Loczewski 2004-03-05