Доброго времени суток, Habr.
Сегодня мы обсудим некоторые математические аспекты quine-программ, да, тех самых, что выдают полную копию своего исходного кода.
Займемся некоторым формальным обоснованием данного явления.
(Далее подразумевается, что читатель знает некоторые понятия: машина Тьюринга, частично вычислимые функции, клиниевская нумерация, теорема о параметризации и s-m-n-теорема, или с помощью google получит первое представление об этом).
Интересующихся математикой приглашаю под кат.
Как мы узнаем далее: quine-программы — это следствие из теоремы о неподвижной точке, которая выполняется в тьюринг-полных языках программирования: императивные языки программирования (Pascal), функциональные (Haskell) и языки логического программирования (Prolog).
Теорема (о неподвижной точке). Для любой частично вычислимой функции $inline$f(x)$inline$ существует $inline$a \in \omega: \varphi_{f(a)} = \varphi_{a}$inline$.
Давайте докажем, что существуют quine-программы для машин Тьюринга.
Возьмем вычислимую функцию $inline$g(x,y)=x \Rightarrow$inline$ (по теореме о параметризации) $inline$\exists$inline$ вычислимая функция $inline$f(x): g(x,y)=\varphi_{f(x)}(y) \Rightarrow$inline$ (по теореме о неподвижной точке) $inline$\exists a \in \omega: \varphi_a = \varphi_{f(a)}$inline$
Пусть $inline$a$inline$ — код некоторой программы машины Тьюринга $inline$\Rightarrow \varphi_{a}(y)=\varphi_{f(a)}(y)=g(a,y)=a$inline$, то есть при любых входных данных функция $inline$\varphi_{a}(y)=a$inline$. Любая частично вычислимая функция может быть выполнена на некоторой машине Тьюринга, поэтому существует такая машина, выполняющая $inline$\varphi_a(y)$inline$ и при этом выводит свой код $inline$a$inline$. Это и есть quine-программа.
Таким образом, мы формально доказали данное явление.
Посмотреть на примеры quine-программ можно в данной статье.
Сегодня мы обсудим некоторые математические аспекты quine-программ, да, тех самых, что выдают полную копию своего исходного кода.
Займемся некоторым формальным обоснованием данного явления.
(Далее подразумевается, что читатель знает некоторые понятия: машина Тьюринга, частично вычислимые функции, клиниевская нумерация, теорема о параметризации и s-m-n-теорема, или с помощью google получит первое представление об этом).
Интересующихся математикой приглашаю под кат.
В каких языках существуют такие программы?
Как мы узнаем далее: quine-программы — это следствие из теоремы о неподвижной точке, которая выполняется в тьюринг-полных языках программирования: императивные языки программирования (Pascal), функциональные (Haskell) и языки логического программирования (Prolog).
Теорема о неподвижной точке
Теорема (о неподвижной точке). Для любой частично вычислимой функции $inline$f(x)$inline$ существует $inline$a \in \omega: \varphi_{f(a)} = \varphi_{a}$inline$.
Доказательство
Рассмотрим частично вычислимую функцию $inline$F(e, y, x) = \varphi^{2}_{e}(y,x)$inline$ — универсальная функция для двухместных частично вычислимых функций. По s-m-n-теореме существует вычислимая функция $inline$s(e,y):$inline$$$display$$\varphi^{2}_{e}(y,x) = \varphi_{s(e,y)}(x) (*).$$display$$ Теперь рассмотрим $inline$\varphi_{f(s(y,y))}(x)$inline$ — 2-местная частично вычислимая функция. $$display$$\Rightarrow \exists n \in \omega: \varphi_{f(s(y,y))}(x) = \varphi_{n}^{2}(y,x) (**).$$display$$ Положим $inline$e=n$inline$.
Из $inline$(*)$inline$ и $inline$(**) \Rightarrow \varphi_{f(s(y,y))}(x) = \varphi_{s(n,y)}(x)$inline$.
Положим $inline$y=n: \varphi_{f(s(n,n))} = \varphi_{s(n,n)}.$inline$
Обозначим $inline$s(n,n) = a: \varphi_{f(a)}=\varphi_{a}.$inline$ Что требовалось доказать.
Из $inline$(*)$inline$ и $inline$(**) \Rightarrow \varphi_{f(s(y,y))}(x) = \varphi_{s(n,y)}(x)$inline$.
Положим $inline$y=n: \varphi_{f(s(n,n))} = \varphi_{s(n,n)}.$inline$
Обозначим $inline$s(n,n) = a: \varphi_{f(a)}=\varphi_{a}.$inline$ Что требовалось доказать.
Существуют ли quine-программы?
Давайте докажем, что существуют quine-программы для машин Тьюринга.
Возьмем вычислимую функцию $inline$g(x,y)=x \Rightarrow$inline$ (по теореме о параметризации) $inline$\exists$inline$ вычислимая функция $inline$f(x): g(x,y)=\varphi_{f(x)}(y) \Rightarrow$inline$ (по теореме о неподвижной точке) $inline$\exists a \in \omega: \varphi_a = \varphi_{f(a)}$inline$
Пусть $inline$a$inline$ — код некоторой программы машины Тьюринга $inline$\Rightarrow \varphi_{a}(y)=\varphi_{f(a)}(y)=g(a,y)=a$inline$, то есть при любых входных данных функция $inline$\varphi_{a}(y)=a$inline$. Любая частично вычислимая функция может быть выполнена на некоторой машине Тьюринга, поэтому существует такая машина, выполняющая $inline$\varphi_a(y)$inline$ и при этом выводит свой код $inline$a$inline$. Это и есть quine-программа.
Таким образом, мы формально доказали данное явление.
Посмотреть на примеры quine-программ можно в данной статье.