Qual é o significado de $\omega$ no cálculo lambda?

Question

Embora eu tenha certeza de que a resposta à minha pergunta deve ser trivial, ainda estou lutando com a definição exata de $\omega$e, consequentemente, as definições de $\omega_2 \dotsb \omega_n$, no Lambda Calculus.

Pelo que entendi, as definições gerais são: $\omega = \lambda x.xx$ e $I = \lambda x.x$.

Mas então, o que é $\omega(\omega)$( isso resulta em um loop de pilha de chamadas de função em expansão infinita? ), e como exatamente$\omega_3 I$ Reduzir para $I$ (como em: o que "chamadas de lambda" em que ordem?).

Embora muitos outros conceitos no cálculo lambda façam muito sentido para mim - como a construção do comportamento booleano, como você pode essencialmente construir todo o 'mundo' a partir disso, e suas implicações filosóficas - sinto que estou perdendo alguns compreensão essencial.

Answer 1

Aviso Legal. O OP não forneceu a definição de$\omega_n$ para qualquer $n \in \mathbb{N}^+$. Eu acho que o OP se refere à seguinte definição

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

e minha resposta baseia-se nesta suposição. Em particular,$\omega = \omega_2 = \lambda x.xx$ e $I = \omega_1 = \lambda x.x$.

---

O ponto de partida é a definição de $\beta$-redução :

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

Onde $M[N/x]$ é uma meta-notação para o termo obtido pela substituição $N$ para as ocorrências gratuitas de $x$ dentro $M$.

Dada esta definição, $\omega$é um duplicador : quando aplicado a qualquer argumento$N$, a função $\omega$ copia o argumento duas vezes e substitui-o por cada uma das duas ocorrências de $x$ dentro $xx$:

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

Como consequência, é claro que $\omega \omega$ (o termo $\omega$aplicado a si mesmo), reduz a si mesmo e cria um loop infinito. De fato,

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

A ideia é que em $\omega\omega$, a função $\omega$ chama o argumento $\omega$, duplica-o (substitui $x$ com $\omega$ em cada ocorrência de $x$ dentro $xx$) para obter novamente $\omega \omega$.

Considere agora $\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}

e a redução pára aqui porque $I$ é normal.

Observe que no $\lambda$-a aplicação de cálculo destina-se a ser associativa à esquerda: um termo $MNL$ deve ser lido como $(MN)L$, e não como$M(NL)$. Em particular, nos exemplos acima,$xxx = (xx)x$ e $III = (II)I$.