2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

Если Вы зададите новый вопрос в существующей теме, то в случае нарушения оформления или других правил форума Ваше сообщение и все ответы на него могут быть удалены без предупреждения.

Не ищите на этом форуме халяву, правила запрещают участникам публиковать готовые решения стандартных учебных задач. Автор вопроса обязан привести свои попытки решения и указать конкретные затруднения.

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему
 
 лямбда-исчисление, редукционный граф
Сообщение25.08.2015, 19:01 


11/10/10
72
Начал разбираться с лямбда-исчислением, хотел уточнить некоторые тривиальные вещи. Сначала пара задачек из "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$

это верно?

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

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

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

 Профиль  
                  
 
 Re: лямбда-исчисление, редукционный граф
Сообщение25.08.2015, 20:07 
Заслуженный участник


27/04/09
28128
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''$.

 Профиль  
                  
 
 Posted automatically
Сообщение25.08.2015, 21:09 
Супермодератор
Аватара пользователя


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

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

 Профиль  
                  
 
 Posted automatically
Сообщение26.08.2015, 07:43 
Супермодератор
Аватара пользователя


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

 Профиль  
                  
 
 Re: лямбда-исчисление, редукционный граф
Сообщение26.08.2015, 12:49 


11/10/10
72
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$ применяется к ближайшему терму, что ко всему выражению.

 Профиль  
                  
 
 Re: лямбда-исчисление, редукционный граф
Сообщение26.08.2015, 14:27 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: лямбда-исчисление, редукционный граф
Сообщение26.08.2015, 14:53 


11/10/10
72
Xaositect в сообщении #1048051 писал(а):
Ну вот например во втором графе у $I(\Omega)$ будет петля, а в первом на соответствующем месте стоит $I W W$ и петли не будет.


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

 Профиль  
                  
 
 Re: лямбда-исчисление, редукционный граф
Сообщение26.08.2015, 15:35 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: лямбда-исчисление, редукционный граф
Сообщение26.08.2015, 18:38 


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 9 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group