лямбда-исчисление, редукционный граф

[dmitryf]

Начал разбираться с лямбда-исчислением, хотел уточнить некоторые тривиальные вещи. Сначала пара задачек из "Introduction to Lambda Calculus H. Barendregt".

Построить редукционный граф для следующих термов:

1. $(\lambda x.Ixx)(\lambda x.Ixx)$
2. $(\lambda x.I(xx))(\lambda x.I(xx))$

где $I$ это комбинатор $\lambda x.x$.

На сколько я понимаю графы будут одинаковыми, потому что расстановка скобочек меняет только к чему будет применяться $I$, либо к $x$, либо к $xx$, но результирующий терм от этого не меняется:

1. $((\lambda x.x)x)x \to xx$
2. $(\lambda x.x)(xx) \to xx$

это верно?

Еще есть более сложная задача, к которой я пока не пойму как подступиться:

"Существует ли лямбда-терм , не имеющий нормальной формы, бета-редукционный граф которого конечен и не одержит циклов нечетной длины?"

Привести пример пока не получилось, похоже надо доказывать отсутствие через индукцию или перебор каких-то вариантов?

[arseniiv]

dmitryf в сообщении #1047767 писал(а):

На сколько я понимаю графы будут одинаковыми, потому что расстановка скобочек меняет только к чему будет применяться $I$, либо к $x$, либо к $xx$, но результирующий терм от этого не меняется:

1. $((\lambda x.x)x)x \to xx$
2. $(\lambda x.x)(xx) \to xx$

это верно?

Это верно, но графы получатся разные, потому что мы можем редуцировать не только каждый из термов в композиции, но и саму композицию, т. к. левый терм — абстракция. Сравните результаты этого для каждого случая:

$$\begin{array}{llll} (1)& (\lambda x.Ixx)(\lambda x.Ixx) &\to& I(\lambda x.Ixx)(\lambda x.Ixx) ,\\ (2)& (\lambda x.I(xx))(\lambda x.I(xx)) &\to& I((\lambda x.I(xx))(\lambda x.I(xx))) .\\ \end{array}$$

Граф для второго терма в конце выходит «более интересный».

Можно для упрощения сравнения графов (и писанины вообще) назвать $W=\lambda x.xx$, $W'=\lambda x.Ixx$, $W''=\lambda x.I(xx)$ и соответственно $\Omega=WW$, $\Omega'=W'W'$, $\Omega''=W''W''$.

[Deggial]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
Причина переноса: формулы не оформлены $\TeX$ом

dmitryf
Наберите все формулы и термы $\TeX$ом.
Инструкции по оформлению формул здесь или здесь (или в этом видеоролике).
См. также тему Что такое карантин, и что нужно делать, чтобы там оказаться.
После исправлений сообщите в теме Сообщение в карантине исправлено, и тогда тема будет возвращена.

[Deggial]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»
Вовзращено

[dmitryf]

arseniiv в сообщении #1047781 писал(а):

Это верно, но графы получатся разные, потому что мы можем редуцировать не только каждый из термов в композиции, но и саму композицию, т. к. левый терм — абстракция. Сравните результаты этого для каждого случая:

$$\begin{array}{llll} (1)& (\lambda x.Ixx)(\lambda x.Ixx) &\to& I(\lambda x.Ixx)(\lambda x.Ixx) ,\\ (2)& (\lambda x.I(xx))(\lambda x.I(xx)) &\to& I((\lambda x.I(xx))(\lambda x.I(xx))) .\\ \end{array}$$

Граф для второго терма в конце выходит «более интересный».

Можно для упрощения сравнения графов (и писанины вообще) назвать $W=\lambda x.xx$, $W'=\lambda x.Ixx$, $W''=\lambda x.I(xx)$ и соответственно $\Omega=WW$, $\Omega'=W'W'$, $\Omega''=W''W''$.

Да, я понимаю, что можно редуцировать саму композицию, но разницу все равно не вижу. Там получается:

$\Omega' \to I(W')W'$
$\Omega' \to \Omega'$
$\Omega' \to I(W)W$
$\Omega' \to \Omega$

$I(W')W' \to \Omega'$
$I(W')W' \to II\Omega'$
$I(W')W' \to I\Omega'$
$I(W')W' \to II\Omega$
$I(W')W' \to I\Omega$
...


то же самое для второго случая, только еще скобки будут стоять:

$\Omega'' \to I(\Omega
$\Omega'' \to \Omega
$\Omega'' \to I(\Omega)$
$\Omega'' \to \Omega$

$I\Omega'' \to \Omega''$
$I\Omega'' \to I(I(\Omega''))$
$I\Omega'' \to I(\Omega'')$
$I\Omega'' \to I(I(\Omega))$
$I\Omega'' \to I(\Omega)$
...

То есть я не понимаю разницы, что $I$ применяется к ближайшему терму, что ко всему выражению.

[Xaositect]

Ну вот например во втором графе у $I(\Omega)$ будет петля, а в первом на соответствующем месте стоит $I W W$ и петли не будет.

[dmitryf]

Xaositect в сообщении #1048051 писал(а):

Ну вот например во втором графе у $I(\Omega)$ будет петля, а в первом на соответствующем месте стоит $I W W$ и петли не будет.

А с чем связано, что я не могу закольцевать в первом случае $WW$ ?

[Xaositect]

В $IWW = (IW)W$ есть единственный редекс: $\underline{IW}W$. Первое $W$ на второе $W$ тут подействовать не может, оно в скобках.
А в $I(WW)$ у нас 2 редекса - $\underline{I(WW)}$ и $I(\underline{WW})$.

[dmitryf]

Кажется я понял, просто аппликация левоассоциативна! Спасибо