Барендрегт 6.1.3. - 6.1.5.

[пианист]

В книжечке Барендрегта, в начале 6 главы можно прочесть следующее соображение

Цитата:

Заметим, что $Yf \twoheadrightarrow f(YF)$ не имеет места. Поэтому (выделение мое - п.) полезны следующие обозначения

6.1.4. Определение (Тьюринг [1937a]). Пусть $A \equiv \lambda xy.y(xxy)$. Положим $\Theta \equiv AA$.

6.1.5. Следствие. $\Theta F \twoheadrightarrow F(\Theta F)$

Здесь $Y$ это $\lambda F.((\lambda x.F(xx))(\lambda x.F(xx)))$, комбинатор неподвижной точки.
Чет туплю. Почему, собс-но, должно $Yf \twoheadrightarrow f(YF)$? И в каком смысле надо понимать следующее далее по тексту "поэтому"?
Методом механической сверки двух термов понял только, что когда выводим соотношение для $Y$, используем только бету, а для $\Theta$ нужна еще эта.
upd Насчет эты ошибка, не нужна, только бета.

[arseniiv]

В маленькой книжке или в монографии? По идее, в монографии должно быть лучше описано.

[пианист]

Мир, 1985 - это какая?

-- Пн авг 19, 2019 19:14:04 --

По размышлении. Наверное, в книжке просто ачепятка, и надо читать "неверно, что $YF \twoheadrightarrow F(YF)$"
Т.е., типа, редукцию $YF$ к $F(YF)$ можно только значком $=$, а $\Theta F$ к $F(\Theta F)$ - значком $\twoheadrightarrow$
Тоже не совсем понятно, но уже не так сильно.

[arseniiv]

А, это монография должна быть.

пианист в сообщении #1411140 писал(а):

Почему, собс-но, должно $\xymatrix{ YF\ar@{->>}[r]&f(YF)}$? И в каком смысле надо понимать следующее далее по тексту "поэтому"?

Судя по всему, только лишь для удобства, ну и «поэтому» чтобы сделать эту редукцию возможной.

Я сначала думал о другом (версии комбинаторов, пригодные для языков с call by value), но оказалось, что это ортогонально различию $Y$ и $\Theta$.

-- Пн авг 19, 2019 21:58:47 --

То есть видимо несмотря на уже доказанное наличие свойства Чёрча—Россера всё равно хочется иметь больше редукций $A\twoheadrightarrow B$ или $B\twoheadrightarrow A$, чем равенств $A = B$. Может быть, на случай некоторого расширенного исчисления, где это свойство не будет иметь места, может просто так хочется.

-- Пн авг 19, 2019 22:19:33 --

А, нет, это свойство там позже доказывается, в главе 11. Монографии они такие.

[пианист]

Спасибо за наводки!

(Оффтоп)

И за стрелку ;)

[george66]

Хочется, чтобы не просто было равенство
$YF=F(YF)$
а чтобы при вычислении $YF$ получалось $F(YF)$ (что и выражает "ёлочка" слева направо). Для $Y$ это не получается, поэтому вводят более удобный комбинатор неподвижной точки $\Theta$

[пианист]

Извиняюсь за невежество, а в чем разница?
Никак не могу уловить различие этих термов ;(
$YF \to \lambda x.F(xx) \lambda x.F(xx) \to F(YF)$
$\Theta F \to \lambda z.z ((\lambda xy.y(xxy)) (\lambda xy.y(xxy)) z) F \to F(\Theta F)$
Только в первом случае мы сначала $F$ подставляем, потом "крокодила", а во втором наоборот.

(индульгенция)

Если что, книжко читаю сильно не подряд.

Интересно еще, почему $Y$ назван парадоксальным?

[george66]

$YF$ это $(\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))F$

Оно не редуцируется к

$F((\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))F)$

(это $F(YF)$ без всяких редукций)

$\Theta F$ это $(\lambda x.\lambda f. f(xxf))(\lambda x.\lambda f. f(xxf))F$

За два шага оно редуцируется к $F(\Theta F)$ После первого шага получается

$(\lambda f.f(\Theta f))F$

Парадоксальным назвали потому, что в те времена компьютеров не было и к зацикливанию не привыкли (в математике оно не встречалось).

-- 21.08.2019, 16:04 --

пианист в сообщении #1411440 писал(а):

$YF \to \lambda x.F(xx) \lambda x.F(xx) \to F(YF)$

Последняя стрелка неверна. Правильно так

$YF \to \lambda x.F(xx) \lambda x.F(xx) \to F(\lambda x.F(xx) \lambda x.F(xx))\leftarrow F(YF)$

[пианист]

Аааа! "Это же Ниагара!" :)
Спасибо!!
Я как-то машинально, на подсознании стрелку в другую сторону развернул.

[arseniiv]

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

Парадоксальным назвали потому, что в те времена компьютеров не было и к зацикливанию не привыкли (в математике оно не встречалось).

Я думал, что так назвали из-за необходимого участия такого комбинатора в аналоге парадокса лжеца, делающем одну из систем, изучавшихся Карри, противоречивой.

(Стрелка)

пианист в сообщении #1411273 писал(а):

И за стрелку ;)

О, мне самому пришлось про неё спрашивать Detexify (лень было открывать список символов распространённых пакетов, он уж совсем большой). Странно, правда, что этой и нескольких подобных стрелок нет в форумной теме про набор.