Барендрегт 19.4.2

[пианист]

19.4.2. Пусть $J = \Theta (\lambda jxy.x(jy))$. Показать, что $D_{\infty} \vDash I = J$.
Получить отсюда, что ни для какого множества $E \subseteq D_{\infty}$ не может выполняться
$[[M]]^{D_{\infty}} \in E \Leftrightarrow M$ имеет н.ф.
для всех $M \in \Lambda^0$

Чет торможу ;(
Непонятно даже, что, собс-но, утверждается - разве $\{[[M]]^{D_{\infty}} | M \in \Lambda^0, M$ имеет н.ф.$\}$ как раз не будет тем самым множеством?

[george66]

Вы как бы выписали подмножество $\Lambda_0$, а требуется подмножество $D_\infty$. На множестве термов есть эквивалентность "равенство в модели $D_\infty$". Предлагается найти подмножество фактора по этой эквивалентности. Или такое подмножество $\Lambda_0$, которое вместе с любым своим термом включает все равные ему (в $D_\infty$). Терм $J$ не имеет нормальной формы, но в модели равен $I$.

[3D Homer]

Разве $E=\{[[M]]^{D_{\infty}} | M \in \Lambda^0, M$ имеет н.ф.$\}$ есть подмножество $\Lambda_0$?

Но это множество не будет "тем самым", по описанной причине: $[[I]]^{D_\infty}\in E$, следовательно $[[J]]^{D_\infty}=[[I]]^{D_\infty}\in E$, но $J$ не имеет н.ф.

[george66]

Говоря проще: в модели $D_\infty$ терм, не имеющий нормальной формы ($J$), может быть равен терму в нормальной форме ($I$). Поэтому свойство "иметь нормальную форму" не имеет смысла для элементов модели.

[пианист]

Кажется, понял.
Свойство "иметь н.ф." не выдерживает перехода к (проективному) пределу?
Ну, это представляется достаточно логичным..

[george66]

Развернём икс с помощью эта-конверсии
$x=\lambda y.x(y) $
Теперь игрек в скобках развернём с помощью эта-конверсии
$x=\lambda y.x(\lambda z.yz) $
Теперь зэт (крайний справа) развернём
$x=\lambda y.x(\lambda z.y(\lambda a.za)) $
Дальше $a$ развернём и так пока не надоест.
Теперь $Jx$ повычисляем (и получим то же самое )
$Jx = (\lambda jxy.x(jy))Jx = \lambda y.x(Jy) = \lambda y.x(\lambda z.y(Jz))=\lambda y.x(\lambda z.y(\lambda a.z(Ja))) $

[пианист]

Спасибо, механика примерно понятна.
upd

(но..)

но как-то не получается заставить интуицию переваривать штуки типа
$D \leftarrow [D \rightarrow D] \leftarrow [[D \rightarrow D] \rightarrow [D \rightarrow D]] \leftarrow ...$

[george66]

Это как $0.999999\ldots = 1$
В модели термы сравниваются по последовательности аппроксимаций. Про деревья Бёма почитайте ( в той же книжке).

[пианист]

Ну да, их и курю..