0

I am currently reading about the lambda calculus as well as the Y combinator. I know that for any function $f$, $Yf$ is a fixed-point of $f$, that is $f(Yf) = Yf$. In order to wrap my head around this, I came up with the following example:

$Y := \lambda f. (\lambda x. f(x, x)) (\lambda x. f(x, x))$

$i : = \lambda n. n$

In order to exemplify the equasion $f(Yf) = Yf$, I tried to get from $i(Yi)$ to $Yi$, which only really required one step:

$i(Yi) = \lambda n. n (\lambda f. (\lambda x. f(x, x)) (\lambda x. f(x, x)) \lambda n.n) = \lambda f. (\lambda x. f(x, x)) (\lambda x. f(x, x)) \lambda n.n = Yi$

However, I can't seem to get from $Yi$ to $i(Yi)$. I guess I am not applying $\beta$-reduction correctly. If someone could show me how to get there, I would be so greatful.

Thank you in advance!

  • There's a derivation here. Please note that you don't need syntactic equality (two terms being the same symbol for symbol), only that they are equivalent. – dtldarek May 14 '15 at 16:30
  • Inside $Y$, the subterm $f(x,x)$ looks wrong. It should be $f(x x)$ where $x$ is applied to itself. Most importantly, this is not calling $f$ with two arguments. – chi May 15 '15 at 18:48

1 Answers1

0

Since $i$ is the identity, you have $(Y) i = (\lambda n . n) (Y) i$, which you can rewrite as $(i)(Y)i$, or in your notation, $i (Y i)$.

With lambda calculus, I would bracket the thing to be evaluated. So $Y$ would be expressed as "$\lambda f . (\lambda x . (f) (x) x) \lambda x . (f) (x) x$". Then $\beta$-reduce $(Y)i$ a few times (I'll repeat the LHS for later clarity).

$$ \begin{align} (Y) i &= (\lambda f . (\lambda x . (f) (x) x) \lambda x . (f) (x) x) i \\ (Y) i &= (\lambda x . (i) (x) x) \lambda x . (i) (x) x \\ (Y) i &= (i) (\lambda x . (i) (x) x) \lambda x . (i) (x) x \end{align} $$

Now define $E$ as the expression on the right hand side of the second line. The second line now looks like $(Y)i = E$.

Then the third line looks like $(Y)i = (i)E$, which by definition of $E$ from the second line, expands to $(Y)i = (i)(Y)i$, as required.

Lawrence
  • 311
  • Hi, thanks for your help. Actually, I know you can rewrite it like that. However, I wanted to get there by stupidly applying reduction rules, like a computer would do. That is what I fail to do... :P –  May 14 '15 at 15:42
  • @baerenfaenger

    I see. I've edited my answer to give a derivation that includes some β-reduction.

     – Lawrence May 15 '15 at 09:10