2014 dxdy logo

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

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




Начать новую тему Ответить на тему
 
 конечности бета-редукционного графа
Сообщение04.12.2017, 09:37 


04/12/17
1
В $\lambda$-исчислении существует стандартный способ доказательства противоречия, через вторую теорему о неподвижной точке:
$\forall F  \exists X  X =_\beta F \underline{X}$, так же верно $\forall F  \exists X  X \to\to_\beta F \underline{X}$, где $ \underline{X}$ означает геделев номер терма $X$.
Я попробовал его применить здесь.

Пусть А - множество термов с бесконечным графом. Допустим существует алгоритм определения, тогда существует и вычислимая характерестическая функция разрешающее множество геделевых номеров термов с бесконечным графом. Она определена в $\lambda$-исчислении термом F. Получаем:
$M \in A \Rightarrow F \underline{M} = \underline{1},  M \notin A \Rightarrow F \underline{M} = \underline{0}$
Положим теперь $G \equiv \lambda x. если Zero(Fx)$, то $M_1$, иначе $M_0$, где $M_1 \in A, M_0 \notin A$
Тогда $M \in A \Rightarrow G \underline{M} = M_0, M \notin A \Rightarrow G \underline{M} = M_1$
Тут возникает проблема, что с помошью этой конструкции можно доказать противоречие для данной задачи только в случае $X \notin A$, где мы показываем, что $X \to\to_\beta F \underline{X} \in A$ , чего не может быть, потому что в результате $\beta$-редукции у терма не мог возникнуть бесконечный граф.
В противоположном случае для $X \in A$ противоречия не получается, потому что в результате теоремы мы только знаем, что $X$ можно редуцировать до терма с конечным графом, а это вполне нормально.

Можно ли тут что-то придумать или это доказывается вообще другим образом?
https://math.stackexchange.com/question ... dr-d-theta

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

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



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

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


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

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