The meaning of $\omega$ in the lambda calculus

computabilitycomputer sciencediscrete mathematicslambda-calculus

Although I am sure the answer to my question must be trivial, I am still struggling with the exact definition of $\omega$, and consequently the definitions of $\omega_2 \dotsb \omega_n$, in the Lambda Calculus.

As far as I understood, the general definitions are: $\omega = \lambda x.xx$ and $I = \lambda x.x$.

But then, what is $\omega(\omega)$ (does it result in an infinitely expanding stack loop of function calls?), and how exactly does $\omega_3 I$ reduce to $I$ (as in: what "lambda calls" in what order?).

Although many other concepts in lambda calculus make a lot of sense to me -such as the construction of boolean behaviour, how you can essentially build the whole 'world' from that, and its philosophical implications- I feel like I am missing out on some essential understanding.

Best Answer

Disclaimer. The OP didn't provide the definition of $\omega_n$ for any $n \in \mathbb{N}^+$. I guess the OP refers to the following definition

$$ \omega_n = \lambda x. \overbrace{x \dots x}^{n \ \text{times}} $$

and my reply relies on this assumption. In particular, $\omega = \omega_2 = \lambda x.xx$ and $I = \omega_1 = \lambda x.x$.


The starting point is the definition of $\beta$-reduction:

$$(\lambda x.M)N \to_\beta M[N/x]$$

where $M[N/x]$ is a meta-notation for the term obtained by substituting $N$ for the free occurrences of $x$ in $M$.

Given this definition, $\omega$ is a duplicator: when applied to any argument $N$, the function $\omega$ copies the argument twice and substitute it for each of the two occurrences of $x$ in $xx$:

$$\omega N = (\lambda x.xx) N \to_\beta (xx)[N/x] = NN$$

As a consequence, it is clear that $\omega \omega$ (the term $\omega$ applied to itself), reduces to itself and create and infinite loop. Indeed,

\begin{align} \omega \omega = (\lambda x.xx) (\lambda x.xx) &\to_\beta (xx) [\lambda x. xx/x] = (\lambda x.xx) (\lambda x.xx) \\ &\to_\beta (xx) [\lambda x. xx/x] = (\lambda x.xx) (\lambda x.xx) \\\ &\to_\beta \dots \end{align}

The idea is that in $\omega\omega$, the function $\omega$ calls the argument $\omega$, duplicates it (it replaces $x$ with $\omega$ in each occurrence of $x$ in $xx$) so as to obtain again $\omega \omega$.

Consider now $\omega_3 I$:

\begin{align} \omega_3 I = (\lambda x.xxx)I &\to_\beta (xxx)[I/x] = III = (\lambda x.x)II\\ &\to_\beta x[I/x]I = II = (\lambda x.x)I \\ &\to_\beta x[I/x] = I \end{align}

and the reduction stops here because $I$ is normal.

Note that in the $\lambda$-calculus application is intended to be left-associative: a term $MNL$ must be read as $(MN)L$, and not as $M(NL)$. In particular, in the examples above, $xxx = (xx)x$ and $III = (II)I$.

Related Question