Нормальная форма, головная нормальная форма, разрешимость.

[пианист]

Барендрегт.
Запутался, что есть, все-таки, головная нормальная форма (гнф).
У Барендрегта это $\lambda \vec{x}. y\vec{N}$, но отсутствует уточнение, сколько в формуле может/должно быть $x$-ов и $N$-ов, а также, должен ли $y$ быть среди $x$-ов.
С одной стороны, в доказательстве теоремы Уодсворта, которая гласит, что наличие гнф равносильно разрешимости, вроде бы, предполагается, что да, $y$ это один их $x$-ов. С другой, Барендрегт утверждает, что нормальная форма (нф) есть гнф; но тогда, получается, что переменная $y$, очевидно, нф, стало быть, и гнф; однако в ней число $x$-ов и $N$-ов равно нулю, условие "$y$ это один их $x$-ов" не выполнено, доказательство теоремы Уодсворта, по видимости, не работает. Да и непонятно, что это за термы такие, чтобы $yN_1...N_k = I$

[george66]

И $x$-ов и $N$-ов может быть ноль, ограничений на них нет. Переменная является головной нормальной формой. Определение разрешимости на стр.178
1) замкнутый терм $M$ разрешим, если $MN_1\ldots N_k=I$ для некоторых $N_1,\ldots, N_k$
2) произвольный терм разрешим, когда его замыкание разрешимо (надо навесить лямбды на все свободные переменные).
Держите хорошую книжку (правда, в формате .ps)
https://mega.nz/file/T8w3CSgA#E4khkUles ... CcsJVF9OX8

[george66]

Сейчас попробую содержательно объяснить. Лямбда-терм бывает или
1) переменная
или
2) аппликация $MN$
или
3) абстракция $\lambda x.M$
Если терм аппликативный $MN$, посмотрим, какую форму имеет $M$ (переменная, аппликация или абстракция). Делая это рекурсивно, приходим к выводу, что аппликативный терм имеет один из двух видов
1) $yN_1\ldots N_k$ (в голове переменная, число $k$ может быть равно нулю)
2) $(\lambda x.M)NN_1\ldots N_k$ (в голове бета-редекс)
Произвольный же терм получается из 1) или 2) навешиванием произвольного количества лямбд (возможно, нулевого).

[пианист]

Спасибо!
я вот этот момент упустил:

george66 в сообщении #1489740 писал(а):

произвольный терм разрешим, когда его замыкание разрешимо

Отдельное спасибо за книжку, пробежался по оглавлению, интересно. Но это про типизированное $\lambda$?

[george66]

Там есть вводная глава про бестиповое, а потом типы (типы тоже интересно)

[пианист]

А, точно, вижу.
Карри-Говард, само собой, интересная штука. Но в типовом, насколько я понимаю, пропадают чудеса с неподвижной точкой :(