Алгоритм для определения конечности бета-редукционного графа

[dmitryf]

В $\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$ можно редуцировать до терма с конечным графом, а это вполне нормально.

Можно ли тут что-то придумать или это доказывается вообще другим образом?

[Mysterious Light]

Я не очень силён в таком вопросе, но осмелюсь предложить:

может, взять какой-то конкретный (т.е. подобрать контрпример) $X$, у которого в принципе нет конечных подграфов с н.ф., например, $(\lambda x.xx)(\lambda x.xx)$ или что-то аналогичное? Тогда по Черчу-Россеру и Вашему суждению $X$ будет редуцироваться через $F\underline{X}$ до н.ф., которой у неё впомине не было.