patternMinor
Reduction of the Y combinator
Viewed 0 times
combinatorthereduction
Problem
The Y combinator expression is as follows:
$$ Y \equiv \lambda f .(\lambda x .f(xx) )) .(\lambda x .f(xx) ) $$
Now , if I am not wrong , then this expression can be reduced by seeing this as the argument:
$ .(\lambda x .f(xx))$ hence would lead to the consumption of first bound variable giving:
$$ (\lambda x .\lambda x .f(xx) (xx))$$
which is equivalent to $ \lambda xx .f(xx) (xx)$
which will yield $ f(xx) $.
But in my book I don't find the Y combinator being reduced to this and it made me feel that something is fishy with the reduction that I am doing .
Is there any mistake in this?
$$ Y \equiv \lambda f .(\lambda x .f(xx) )) .(\lambda x .f(xx) ) $$
Now , if I am not wrong , then this expression can be reduced by seeing this as the argument:
$ .(\lambda x .f(xx))$ hence would lead to the consumption of first bound variable giving:
$$ (\lambda x .\lambda x .f(xx) (xx))$$
which is equivalent to $ \lambda xx .f(xx) (xx)$
which will yield $ f(xx) $.
But in my book I don't find the Y combinator being reduced to this and it made me feel that something is fishy with the reduction that I am doing .
Is there any mistake in this?
Solution
You've misread the definition of $Y$. $(\lambda x.f(xx))) (\lambda x.f(xx))$ is the body of the function. You can put an additional pair of parentheses in the definition:
$$ Y = \lambda f. \color{red}{\mathbf{(}} (\lambda x.f(xx))) (\lambda x.f(xx)) \color{red}{\mathbf{)}}$$
Beware that different authors use different conventions for parentheses. But under the most common convention, $\lambda$ has lower precedence than application, so the body of a lambda goes until the next enclosing closing parenthesis. If a text uses a different convention, make sure to put parentheses accordingly.
You can reduce $Y$, but the argument $(\lambda x.f(xx)))$ is applied to $(\lambda x.f(xx))$. The $\lambda f. \ldots$ doesn't change since it isn't applied to anything.
$$\begin{align}
Y \;\; = \; & \lambda f. (\lambda \color{magenta}{x}.f(\color{magenta}{x}\color{magenta}{x}))) \color{magenta}{(\lambda x.f(xx)))} \\
\rightarrow_\beta \; & \lambda f. f \left( (\lambda x.f(xx))) (\lambda x.f(xx))) \right) \\
\end{align}$$
Let $\Omega_f = (\lambda x.f(xx)) (\lambda x.f(xx))$, so that $Y = \lambda f. \Omega_f$. The reduction above is $\lambda f. \Omega_f \rightarrow_\beta \lambda f. f \Omega_f$. That's $\Omega_f \rightarrow_\beta f \Omega_f$ under the context $\lambda f. []$. There's an infinite chain of reductions
$$
Y = \lambda f. \Omega_f
\rightarrow_\beta \lambda f. f \Omega_f
\rightarrow_\beta \lambda f. f (f \Omega_f)
\rightarrow_\beta \lambda f. f (f (f \Omega_f))
\rightarrow_\beta \ldots
$$
This is how the recursion combinator works. But this won't do anything “useful” until $f$ is replaced by a lambda so that the $f \Omega_f$ part can be reduced.
If you apply $Y$ to a function $g$, a redex appears at the top level.
$$ \begin{align}
Y g \;\; = \;\; & \left( \color{green}{\lambda f}. (\lambda x.\color{green}{f}(xx))) (\lambda x.\color{green}{f}(xx)) \right) \color{green}{g} \\
\rightarrow_\beta \; & (\color{darkblue}{\lambda x}. g(\color{darkblue}{x} \color{darkblue}{x})) \color{darkblue}{(\lambda x. g(x x))} \\
\rightarrow_\beta \; & g \left( (\lambda x. g(x x)) (\lambda x. g(x x)) \right) \\
\leftarrow_\beta \; & g \left( \left( \color{brown}{\lambda f}. (\lambda x. \color{brown}{f}(x x)) (\lambda x. \color{brown}{f}(x x)) \right) \color{brown}{g} \right) \\
= \; & g (Y g)
\end{align}$$
$$ Y = \lambda f. \color{red}{\mathbf{(}} (\lambda x.f(xx))) (\lambda x.f(xx)) \color{red}{\mathbf{)}}$$
Beware that different authors use different conventions for parentheses. But under the most common convention, $\lambda$ has lower precedence than application, so the body of a lambda goes until the next enclosing closing parenthesis. If a text uses a different convention, make sure to put parentheses accordingly.
You can reduce $Y$, but the argument $(\lambda x.f(xx)))$ is applied to $(\lambda x.f(xx))$. The $\lambda f. \ldots$ doesn't change since it isn't applied to anything.
$$\begin{align}
Y \;\; = \; & \lambda f. (\lambda \color{magenta}{x}.f(\color{magenta}{x}\color{magenta}{x}))) \color{magenta}{(\lambda x.f(xx)))} \\
\rightarrow_\beta \; & \lambda f. f \left( (\lambda x.f(xx))) (\lambda x.f(xx))) \right) \\
\end{align}$$
Let $\Omega_f = (\lambda x.f(xx)) (\lambda x.f(xx))$, so that $Y = \lambda f. \Omega_f$. The reduction above is $\lambda f. \Omega_f \rightarrow_\beta \lambda f. f \Omega_f$. That's $\Omega_f \rightarrow_\beta f \Omega_f$ under the context $\lambda f. []$. There's an infinite chain of reductions
$$
Y = \lambda f. \Omega_f
\rightarrow_\beta \lambda f. f \Omega_f
\rightarrow_\beta \lambda f. f (f \Omega_f)
\rightarrow_\beta \lambda f. f (f (f \Omega_f))
\rightarrow_\beta \ldots
$$
This is how the recursion combinator works. But this won't do anything “useful” until $f$ is replaced by a lambda so that the $f \Omega_f$ part can be reduced.
If you apply $Y$ to a function $g$, a redex appears at the top level.
$$ \begin{align}
Y g \;\; = \;\; & \left( \color{green}{\lambda f}. (\lambda x.\color{green}{f}(xx))) (\lambda x.\color{green}{f}(xx)) \right) \color{green}{g} \\
\rightarrow_\beta \; & (\color{darkblue}{\lambda x}. g(\color{darkblue}{x} \color{darkblue}{x})) \color{darkblue}{(\lambda x. g(x x))} \\
\rightarrow_\beta \; & g \left( (\lambda x. g(x x)) (\lambda x. g(x x)) \right) \\
\leftarrow_\beta \; & g \left( \left( \color{brown}{\lambda f}. (\lambda x. \color{brown}{f}(x x)) (\lambda x. \color{brown}{f}(x x)) \right) \color{brown}{g} \right) \\
= \; & g (Y g)
\end{align}$$
Context
StackExchange Computer Science Q#89119, answer score: 6
Revisions (0)
No revisions yet.