# Deriving the fixed point for $\omega$ (i.e. $\lambda x.xx$) and proving it to be so

I am studying the simply typed $\lambda$-calculus, and I am struggling a bit with really understanding fixed-points and the $\mathbf Y$ combinator. I have read or skimmed all the questions on here that appear related to mine, but none of them seem to address my particular point of difficulty.

1. Find the fixed-point for $\omega$, where $\omega = \lambda x.xx$.
2. Prove that it is the fixed-point.

In my course, they say that $\xi$ is a fixed point for a function $f$ when $\xi$ <~~> $f \xi$, where ~~> means "$\beta$-reduces to". In my course material, and in Hankin's An Introduction to Lambda Calculi for Computer Scientists, I have learned that the $\mathbf Y$ combinator is "a term which, when applied to another term, is equal to the fixed point of the given term" (Hankin 90). So, I think $\mathbf Y \omega = \xi = \omega \xi$ and finding the fixed-point for $\omega$ should be as simple as reducing $\mathbf Y \omega$.

$$\mathbf Y \omega \\ \to (\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))\ \omega \\ \to (\lambda x.\omega(xx))(\lambda x.\omega(xx))$$

So, if I understand correctly, then $\xi = (\lambda x.\omega(xx))(\lambda x.\omega(xx)) = \omega \xi$. Now that I think I have found $\xi$ for this case, it is time to verity that $\xi$ <~~> $\omega \xi$. First, verifying $\xi$ ~~> $\omega \xi$ is very easy, and is a matter of one reduction:

$$(\lambda x.\omega(xx))(\lambda x.\omega(xx)) \\ \to \omega((\lambda x.\omega(xx))(\lambda x.\omega(xx)))$$

Finally, I think I should also show that $\omega \xi$ ~~> $\xi$, but I cannot figure out how this could be done. If I start trying, it seems I get an irreducible term right away:

$$\omega(\lambda x.\omega(xx))(\lambda x.\omega(xx)) \\ \to (\lambda x.xx)((\lambda x.\omega(xx))(\lambda x.\omega(xx))) \\ \to ((\lambda x.\omega(xx))(\lambda x.\omega(xx)))((\lambda x.\omega(xx))(\lambda x.\omega(xx))) \\ \to \omega((\lambda x.\omega(xx))(\lambda x.\omega(xx)))\omega((\lambda x.\omega(xx))(\lambda x.\omega(xx))) \\ \to \omega(\omega((\lambda x.\omega(xx))(\lambda x.\omega(xx))))\omega(\omega((\lambda x.\omega(xx))(\lambda x.\omega(xx)))) \\ ...$$

So I do not see how one could demonstrate that $\omega \xi$ ~~> $\xi$, and I am worried that I must be misunderstanding something fundamental. Especially when I consider that taking just the first part of $\xi$, it is obvious that $\omega(\lambda x.\omega(xx))$ ~~> $\xi$:

$$\omega(\lambda x.\omega(xx)) \\ \to (\lambda x.xx)(\lambda x.\omega(xx)) \\ \to (\lambda x.\omega(xx))(\lambda x.\omega(xx))$$

So maybe I have misidentified the fixed point in the first place? In which case, how is $\mathbf Y$ supposed to work?

Any help in figuring out how to resolve this, and especially in helping me correct my understanding, will be very much appreciated.