Изменения
→Пример использования
}}
==Пример использования==Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка <tex>L=\{p|p(\epsilon)=\perp\}</tex>См.{{Лемма|id=st2|statement= Язык <tex>Lтакже=\{p|p(\epsilon)=\perp\}</tex> неразрешим. |proof=Предположим обратное, тогда существует программа <tex>r</tex> разрещающая <tex>L</tex>.Рассмотрим следущую программу*[[Участник:<code> p(x) if r(p) return 1 while true<Shersh/code>Пусть <tex>p(\epsilon)=\perp</tex>. Тогда условие <tex>r(p)</tex> выполняется и <tex>p(\epsilon)=1</tex>. Противоречие. Если <tex>p(\epsilon) \ne \perp</tex>, то <tex>r(p)</tex> не выполняется и <tex>p(\epsilon)=\perp</tex>. Противоречие.}} Доказательство [[Свойства перечислимых языков. Теорема Успенского-Райса|теоремы Успенского-РайсаТеорема_о_рекурсии]] с использованием теоремы о рекурсии:{{Теорема|id=th3|statement=Язык никакого нетривиального свойства не является разрешимым.|proof=Пусть <tex>F \subset RE, \varnothing \not= F \not= RE</tex>. Предположим, что язык свойства <tex>F</tex> разрешается программой <tex>d</tex>.Пусть <tex>f \in L(F), g \not\in L(F)</tex>. Напишем следующую программу:<code> Q(x,y) if d(x) return g(y) else return f(y)</code>По теореме о рекурсии, <tex>\exists p \; \forall y \; p(y) = Q(p,y)</tex>. Если <tex>p \in L(F)</tex>, то <tex>Q(p,y) = g(y) \Rightarrow p(y) = g(y) \Rightarrow p \not\in L(F)</tex>. Если же <tex>p \not\in L(F)</tex>, то <tex>Q(p,y) = f(y) \Rightarrow p(y) = f(y) \Rightarrow p \in L(F)</tex>. В обоих случаях получаем противоречие.}}
==Источники==
