Викиконспекты - Вклад участника [ru]

Теорема о рекурсии

2016-12-03T10:30:55Z

217.66.158.24: /* Теорема о неподвижной точке */

==Теорема о рекурсии==

{{Теорема
|id=th1
|author=Клини
|about=о рекурсии / ''Kleene's recursion theorem''
|statement= Пусть <tex>V(n, x)</tex> {{---}} вычислимая функция. Тогда найдётся такая вычислимая <tex>p</tex>, что <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>.
|proof=
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. Предположим, что у нас в распоряжении есть функция <tex>getSrc()</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так:

<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {...}
}
</code>
Теперь нужно определить функцию <tex>getSrc()</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>getOtherSrc()</tex>, состоящую из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так.
<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}

string getOtherSrc() {...}
}
</code>

Теперь <tex>getOtherSrc()</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex>
<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}

string getOtherSrc() {
return " p(y){ // Возвращаем весь предыдущий код
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}";
}
}
</code>

}}
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.

Приведем так же альтернативую формулировку теоремы и альтернативное (неконструктивное) доказательство.

==Теорема о неподвижной точке==
{{Теорема
|id=th2
|author=Роджерс
|about=о неподвижной точке / ''Rogers' fixed-point theorem''
|statement= Пусть <tex>U</tex> {{---}} [[Диагональный_метод|универсальная функция]] для класса вычислимых функций одного аргумента, <tex>h</tex> {{---}} всюду определённая [[Вычислимые_функции|вычислимая функция]] одного аргумента. Тогда найдется такое <tex>n</tex>, что <tex>U_n=U_{h(n)}</tex>, то есть <tex>n</tex> и <tex>h(n)</tex> - номера одной функции.
|proof=
Начнём с доказательства леммы.
{{Лемма
|statement= Пусть на натуральных числах задано отношение эквивалентности <tex>\equiv</tex>. Тогда следующие два утверждения не могут быть выполнены одновременно: 
# Пусть <tex>f</tex> {{---}} вычислимая функция. Тогда существует всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>, то есть такая <tex>g</tex>, что <tex>D(g)=N</tex> и <tex>\forall x</tex> такого, что <tex>f(x) \ne \perp</tex>, выполнено <tex>f(x) \equiv g(x)</tex>.
# Найдётся такая всюду определенная вычислимая <tex>h</tex>, что <tex>\forall n </tex> выполнено <tex>h(n) \not\equiv n</tex>.
|proof=
Приведем доказательство от противного. Пусть оба утверждения выполнены. 
Определим функцию <tex>f</tex> так: <tex>f(x)=U(x,x)</tex>. Заметим, что никакая всюду вычислимая функция не отличается от <tex>f</tex> всюду. Согласно первому утверждению найдётся всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>. Определим функцию <tex>t</tex> так: <tex>t(x)=h(g(x))</tex>, где <tex>h</tex> {{---}} функция из второго утверждения. Если <tex>f(x) \ne \perp</tex>, то <tex>f(x)=g(x) \ne h(g(x))=t(x)</tex>, то есть <tex>f(x) \ne t(x)</tex>. Если <tex>f(x)= \perp</tex>, то <tex>f(x) \ne t(x)</tex>, так как <tex>t</tex> всюду определена. Значит, <tex>f</tex> всюду отлична от <tex>t</tex>, получили противоречие.
}}
Теперь определим отношение <tex>\equiv</tex> так: <tex>x \equiv y \Leftrightarrow U_x = U_y</tex>. Покажем, что для него выполнено первое утверждение леммы. Для заданной <tex>f</tex> определим <tex>V(n,x) = U(f(n), x)</tex>. Так как <tex>U</tex> {{---}} универсальная функция, то найдётся такая всюду определенная вычислимая функция <tex>s</tex>, что <tex>V(n,x) = U(s(n), x)</tex>. Тогда <tex>\forall x </tex> и <tex> n </tex> будет выполнено <tex>U(f(n), x) = U(s(n), x)</tex>. Значит, <tex>\forall n </tex> <tex> s(n) \equiv f(n)</tex>, то есть <tex>s</tex> {{---}} всюду определенное <tex>\equiv</tex> {{---}} продолжение <tex>f</tex>.
Значит, для нашего отношения эквивалентности второе утверждение леммы не верно, то есть для любого вычислимого всюду определенного <tex>h</tex> <tex> \exists n</tex> такое, что <tex>U_{h(n)} = U_n</tex>.
}}
Другими словами, нельзя найти алгоритма, преобразующего программы, который бы по каждой программе давал другую (не эквивалентную ей).

==Пример использования==
Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка <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
</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>.

В обоих случаях получаем противоречие.
}}

==Источники==
* [[wikipedia:Kleene's_recursion_theorem | Wikipedia {{---}} Kleene's recursion theorem]]
* ''Верещагин Н. К., Шень А.'' '''Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции''' — М.: МЦНМО, 1999 - С. 176
* ''Kleene, Stephen'' '''On notation for ordinal numbers''' - The Journal of Symbolic Logic, 1938 - С. 150-155

Теорема о рекурсии

2016-12-03T10:27:51Z

217.66.158.24: /* Теорема о неподвижной точке */

==Теорема о рекурсии==

{{Теорема
|id=th1
|author=Клини
|about=о рекурсии / ''Kleene's recursion theorem''
|statement= Пусть <tex>V(n, x)</tex> {{---}} вычислимая функция. Тогда найдётся такая вычислимая <tex>p</tex>, что <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>.
|proof=
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. Предположим, что у нас в распоряжении есть функция <tex>getSrc()</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так:

<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {...}
}
</code>
Теперь нужно определить функцию <tex>getSrc()</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>getOtherSrc()</tex>, состоящую из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так.
<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}

string getOtherSrc() {...}
}
</code>

Теперь <tex>getOtherSrc()</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex>
<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}

string getOtherSrc() {
return " p(y){ // Возвращаем весь предыдущий код
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}";
}
}
</code>

}}
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.

Приведем так же альтернативую формулировку теоремы и альтернативное (неконструктивное) доказательство.

==Теорема о неподвижной точке==
{{Теорема
|id=th2
|author=Роджерс
|about=о неподвижной точке / ''Rogers' fixed-point theorem''
|statement= Пусть <tex>U</tex> {{---}} [[Диагональный_метод|универсальная функция]] для класса вычислимых функций одного аргумента, <tex>h</tex> {{---}} всюду определённая [[Вычислимые_функции|вычислимая функция]] одного аргумента. Тогда найдется такое <tex>n</tex>, что <tex>U_n=U_{h(n)}</tex>, то есть <tex>n</tex> и <tex>h(n)</tex> - номера одной функции. Другими словами, нельзя найти алгоритма, преобразующего программы, который бы по каждой программе давал другую (не эквивалентную ей).
|proof=
Начнём с доказательства леммы.
{{Лемма
|statement= Пусть на натуральных числах задано отношение эквивалентности <tex>\equiv</tex>. Тогда следующие два утверждения не могут быть выполнены одновременно: 
# Пусть <tex>f</tex> {{---}} вычислимая функция. Тогда существует всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>, то есть такая <tex>g</tex>, что <tex>D(g)=N</tex> и <tex>\forall x</tex> такого, что <tex>f(x) \ne \perp</tex>, выполнено <tex>f(x) \equiv g(x)</tex>.
# Найдётся такая всюду определенная вычислимая <tex>h</tex>, что <tex>\forall n </tex> выполнено <tex>h(n) \not\equiv n</tex>.
|proof=
Приведем доказательство от противного. Пусть оба утверждения выполнены. 
Определим функцию <tex>f</tex> так: <tex>f(x)=U(x,x)</tex>. Заметим, что никакая всюду вычислимая функция не отличается от <tex>f</tex> всюду. Согласно первому утверждению найдётся всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>. Определим функцию <tex>t</tex> так: <tex>t(x)=h(g(x))</tex>, где <tex>h</tex> {{---}} функция из второго утверждения. Если <tex>f(x) \ne \perp</tex>, то <tex>f(x)=g(x) \ne h(g(x))=t(x)</tex>, то есть <tex>f(x) \ne t(x)</tex>. Если <tex>f(x)= \perp</tex>, то <tex>f(x) \ne t(x)</tex>, так как <tex>t</tex> всюду определена. Значит, <tex>f</tex> всюду отлична от <tex>t</tex>, получили противоречие.
}}
Теперь определим отношение <tex>\equiv</tex> так: <tex>x \equiv y \Leftrightarrow U_x = U_y</tex>. Покажем, что для него выполнено первое утверждение леммы. Для заданной <tex>f</tex> определим <tex>V(n,x) = U(f(n), x)</tex>. Так как <tex>U</tex> {{---}} универсальная функция, то найдётся такая всюду определенная вычислимая функция <tex>s</tex>, что <tex>V(n,x) = U(s(n), x)</tex>. Тогда <tex>\forall x </tex> и <tex> n </tex> будет выполнено <tex>U(f(n), x) = U(s(n), x)</tex>. Значит, <tex>\forall n </tex> <tex> s(n) \equiv f(n)</tex>, то есть <tex>s</tex> {{---}} всюду определенное <tex>\equiv</tex> {{---}} продолжение <tex>f</tex>.
Значит, для нашего отношения эквивалентности второе утверждение леммы не верно, то есть для любого вычислимого всюду определенного <tex>h</tex> <tex> \exists n</tex> такое, что <tex>U_{h(n)} = U_n</tex>.
}}

==Пример использования==
Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка <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
</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>.

В обоих случаях получаем противоречие.
}}

==Источники==
* [[wikipedia:Kleene's_recursion_theorem | Wikipedia {{---}} Kleene's recursion theorem]]
* ''Верещагин Н. К., Шень А.'' '''Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции''' — М.: МЦНМО, 1999 - С. 176
* ''Kleene, Stephen'' '''On notation for ordinal numbers''' - The Journal of Symbolic Logic, 1938 - С. 150-155

Теорема о рекурсии

2016-12-02T19:50:02Z

217.66.158.24: /* Источники */

==Теорема о рекурсии==

{{Теорема
|id=th1
|author=Клини
|about=о рекурсии / ''Kleene's recursion theorem''
|statement= Пусть <tex>V(n, x)</tex> {{---}} вычислимая функция. Тогда найдётся такая вычислимая <tex>p</tex>, что <tex>\forall y</tex> <tex>p(y) = V(p, y)</tex>.
|proof=
Приведем конструктивное доказательство теоремы.
Пусть есть вычислимая <tex>V(x,y)</tex>. Будем поэтапно строить функцию <tex>p(y)</tex>. Предположим, что у нас в распоряжении есть функция <tex>getSrc()</tex>, которая вернет код <tex>p(y)</tex>. Тогда саму <tex>p(y)</tex> можно переписать так:

<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {...}
}
</code>
Теперь нужно определить функцию <tex>getSrc()</tex>. Предположим, что внутри <tex>p(y)</tex> мы можем определить функцию <tex>getOtherSrc()</tex>, состоящую из одного оператора <tex>return</tex>, которая вернет весь предшествующий ей код. Тогда <tex>p(y)</tex> перепишется так.
<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}

string getOtherSrc() {...}
}
</code>

Теперь <tex>getOtherSrc()</tex> определяется очевидным образом, и мы получаем '''итоговую версию''' функции <tex>p(y)</tex>
<code>
p(y){
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}

string getOtherSrc() {
return " p(y){ // Возвращаем весь предыдущий код
V(x,y) {...}

main() {
return V(getSrc(), y)
}

string getSrc() {
string src = getOtherSrc();
return src + "string getOtherSrc() {" + "\n" + "return" + src + "\n" + "}";
}";
}
}
</code>

}}
Если говорить неформально, теорема о рекурсии утверждает, что внутри программы можно использовать ее код. Это упрощает доказательство некоторых теорем.

Приведем так же альтернативую формулировку теоремы и альтернативное (неконструктивное) доказательство.

==Теорема о неподвижной точке==
{{Теорема
|id=th2
|author=Роджерс
|about=о неподвижной точке / ''Rogers' fixed-point theorem''
|statement= Пусть <tex>U</tex> {{---}} [[Диагональный_метод|универсальная функция]], <tex>h</tex> {{---}} всюду определённая [[Вычислимые_функции|вычислимая функция]]. Тогда найдется такое <tex>n</tex>, что <tex>U_n=U_{h(n)}</tex>.
Другими словами: нельзя найти алгоритма, преобразующего программы, который бы по каждой программе давал другую (не эквивалентную ей).
|proof=
Начнём с доказательства леммы.
{{Лемма
|statement= Пусть на натуральных числах задано отношение эквивалентности <tex>\equiv</tex>. Тогда следующие два утверждения не могут быть выполнены одновременно: 
# Пусть <tex>f</tex> {{---}} вычислимая функция. Тогда существует всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>, то есть такая <tex>g</tex>, что <tex>D(g)=N</tex> и <tex>\forall x</tex> такого, что <tex>f(x) \ne \perp</tex>, выполнено <tex>f(x) \equiv g(x)</tex>.
# Найдётся такая всюду определенная вычислимая <tex>h</tex>, что <tex>\forall n </tex> выполнено <tex>h(n) \not\equiv n</tex>.
|proof=
Приведем доказательство от противного. Пусть оба утверждения выполнены. 
Определим функцию <tex>f</tex> так: <tex>f(x)=U(x,x)</tex>. Заметим, что никакая всюду вычислимая функция не отличается от <tex>f</tex> всюду. Согласно первому утверждению найдётся всюду определённое вычислимое <tex>\equiv</tex> {{---}} продолжение <tex>g</tex> функции <tex>f</tex>. Определим функцию <tex>t</tex> так: <tex>t(x)=h(g(x))</tex>, где <tex>h</tex> {{---}} функция из второго утверждения. Если <tex>f(x) \ne \perp</tex>, то <tex>f(x)=g(x) \ne h(g(x))=t(x)</tex>, то есть <tex>f(x) \ne t(x)</tex>. Если <tex>f(x)= \perp</tex>, то <tex>f(x) \ne t(x)</tex>, так как <tex>t</tex> всюду определена. Значит, <tex>f</tex> всюду отлична от <tex>t</tex>, получили противоречие.
}}
Теперь определим отношение <tex>\equiv</tex> так: <tex>x \equiv y \Leftrightarrow U_x = U_y</tex>. Покажем, что для него выполнено первое утверждение леммы. Для заданной <tex>f</tex> определим <tex>V(n,x) = U(f(n), x)</tex>. Так как <tex>U</tex> {{---}} универсальная функция, то найдётся такая всюду определенная вычислимая функция <tex>s</tex>, что <tex>V(n,x) = U(s(n), x)</tex>. Тогда <tex>\forall x </tex> и <tex> n </tex> будет выполнено <tex>U(f(n), x) = U(s(n), x)</tex>. Значит, <tex>\forall n </tex> <tex> s(n) \equiv f(n)</tex>, то есть <tex>s</tex> {{---}} всюду определенное <tex>\equiv</tex> {{---}} продолжение <tex>f</tex>.
Значит, для нашего отношения эквивалентности второе утверждение леммы не верно, то есть для любого вычислимого всюду определенного <tex>h</tex> <tex> \exists n</tex> такое, что <tex>U_{h(n)} = U_n</tex>.
}}

==Пример использования==
Используя теорему о рекурсии, приведём простое доказательство неразрешимости языка <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
</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>.

В обоих случаях получаем противоречие.
}}

==Источники==
* [[wikipedia:Kleene's_recursion_theorem | Wikipedia {{---}} Kleene's recursion theorem]]
* ''Верещагин Н. К., Шень А.'' '''Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции''' — М.: МЦНМО, 1999 - С. 176
* ''Kleene, Stephen'' '''On notation for ordinal numbers''' - The Journal of Symbolic Logic, 1938 - С. 150-155