2014 dxdy logo

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

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


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


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Барендрегт 19.4.2
Сообщение23.11.2019, 21:33 
Заслуженный участник
Аватара пользователя


03/06/08
2147
МО
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$ имеет н.ф.$\}$ как раз не будет тем самым множеством?

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение23.11.2019, 22:21 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение25.11.2019, 00:47 


06/06/13
71
Разве $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$ не имеет н.ф.

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение25.11.2019, 02:14 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение25.11.2019, 07:49 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение25.11.2019, 11:44 
Заслуженный участник


31/12/15
922
Развернём икс с помощью эта-конверсии
$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)))  $

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение26.11.2019, 07:19 
Заслуженный участник
Аватара пользователя


03/06/08
2147
МО
Спасибо, механика примерно понятна.
upd

(но..)

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

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение27.11.2019, 13:37 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Барендрегт 19.4.2
Сообщение28.11.2019, 07:30 
Заслуженный участник
Аватара пользователя


03/06/08
2147
МО
Ну да, их и курю..

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

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



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

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


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

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