2014 dxdy logo

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

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки
01/01/18 20:50 UTC: Перешли на HTTPS в тестовом режиме. О проблемах пишите в ЛС cepesh.





Начать новую тему Ответить на тему
 
 конечности бета-редукционного графа
Сообщение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 сообщение ] 

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



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

Сейчас этот форум просматривают: Xaositect


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

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