3
$\begingroup$

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?

$\endgroup$
6
$\begingroup$

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}$$

$\endgroup$
  • $\begingroup$ @Giles : Thanks a lot , now it makes things clear $\endgroup$ – Agnivesh Singh Mar 10 '18 at 5:46
  • $\begingroup$ Actually, there is a way to reduce $Y$, since $\to_\beta$ reduces under lambdas. In certain reduction strategies, this is disallowed, but reducing under lambdas is allowed in the standard theory (e.g. Barendregt's). So, writing $Z$ for $\lambda x.f(xx)$, we have $Y=\lambda f.ZZ \to_\beta \lambda f.f(ZZ) \to_\beta f(f(ZZ)) \to_\beta \ldots$ without ever reaching normal form. Of course, the result of this reduction is not that useful, albeit one can see it as a hint about a fixed point being computed. Passing an additional argument $g$ as you did makes it much clearer, though. $\endgroup$ – chi Mar 10 '18 at 21:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.