Занимательное квайноводство. Часть I.

Июль, 2020 Аннотация

В этом сообщении (в первой части серии сообщений), после краткого введения в некоторые основы теории вычислимости, в основном описываются результаты простого эксперимента по автоматизированному конструированию квайна с использованием второй рекурсивной теоремы Клини.

В качестве целевого языка выбран язык поточного редактора [GNU] sed. Изложение, однако, не специфично для этого языка и может трактоваться в более широком контексте. Фактически, в предлагаемом цикле сообщений излагаются некоторые подходы к систематическому конструированию квайнов.

Содержание:

Введение в квайнологию
Вводные замечания
- Теорема об универсальной функции
- S-m-n теорема Клини
Неподвижные точки вычислимых функций
Главный эксперимент
Промежуточные итоги
Дополнительная теория
Немного о пределах познаваемости
Другие подходы и «слегка открытые» вопросы
Заключение
Ссылки

Введение в квайнологию

Всем известно «стандартное» упражнение в программировании, заключающееся в написании программы, печатающей свой собственный текст. За такими самореплицирующимися программами достаточно давно закрепилось название «квайн» (также встречаются варианты написания/произношения «куайн», «квин», «куин») введенное в известной книге Хофштадтера [26] в честь философа Куайна (Уиллард Ван Орман Куайн = Willard Van Orman Quine) и его «парадокса Куайна» [15].

Сами квайны при этом появились раньше. Может быть их историю следовало бы вести с работ фон Неймана по самореплицирующимся [клеточным] автоматам [9, 48] или даже с работ Чёрча и Хаскеля…

Квайны являются немного парадоксальными программами, в соответствии с бытовой интуицией не могущими существовать, – ведь может показаться, что программа не может вывести текст, имеющий длину, равную длине самой программы (должно остаться место для кода, выполняющего печать). И тем не менее они существуют (и не требуют сжатия данных, которое, в соответствии с фундаментальной теоремой компрессии, не всегда возможно).

Более того, теория вычислимости говорит, что квайны можно написать на любом [достаточно выразительном] языке программирования. На деле, конечно, сложность написания и размер результирующего кода сильно варьируются от языка к языку.

В качестве примеров квайнов можно привести такие поделки (авторы мне не известны):

Квайн на lisp:

((lambda (x)
  (list x (list (quote quote) x)))
(quote
  (lambda (x)
    (list x (list (quote quote) x)))))

Квайн на стековом rpn-языке форт (forth):

s" 2dup 115 emit 34 emit 32 emit type 34 emit type cr bye"
2dup 115 emit 34 emit 32 emit type 34 emit type cr bye

(Это одна длинная строка, могущая отображаться на нескольких экранных строках.)

Квайн на экспериментальном функциональном стековом rpn-языке joy [32]:

"dup.putchars.10 putch."
dup.putchars.10 putch.

Квайн для $\text{[math]}$ -исчисления(почти то же, что и выше на lisp):

$\text{[math]}$

В стандартной библиотеке языка C есть функция форматированного вывода printf, которая может быть использована [в качестве суррогата $\text{[math]}$ -функции] для внедрения текста программы в него самого; что-то вроде printf(f, f), только с учетом технических сложностей с вложенными кавычками для обрамления строк. По этому принципу построен такой известный однострочный миниквайн на C (здесь не указан заголовочный файл stdio.h, в котором определена printf, но в таком виде этот код всё-равно компилируется и работает):

char*f="char*f=%c%s%c;main(){printf(f,34,f,34,10);}%c";main(){printf(f,34,f,34,10);}

Многие квайны (в т.ч. большинство из приведенных выше) злоупотребляют экранированием строк, специальными кодами символов (зависящими от используемой в системе кодировки, e.g. ASCII) и библиотечными функциями подстановки (замены подстрок), «скрывающими» существенную часть происходящих процессов. «Идеологически» более чистым подходом представляется ограничение строковых манипуляций конкатенацией строк при одновременной минимизации экранирований. Неплохим образчиком подобной стратегии написания квайнов является квайн (на pascal’е) от Dan Hoey (взятый мною из [50]):

program s;const bbb='program s;const bbb';a='a';b='b';bb=');writeln(';
aa='''';ab='=''';ba=''';';
aaa='begin writeln(bbb,ab,bbb,ba,a,ab,a,ba,b,ab,b,ba,b,b,ab,bb,ba';
aba='a,a,ab,aa,aa,ba,a,b,ab,ab,aa,ba,b,a,ab,aa,ba,ba';
abb='a,a,a,ab,aaa,ba);writeln(a,b,a,ab,aba,ba);writeln(a,b,b,ab,abb,ba';
baa='b,a,a,ab,baa,ba);writeln(b,a,b,ab,bab,ba);writeln(aaa,bb';
bab='aba,bb);writeln(abb);writeln(bb,baa);writeln(bb,bab)end.';
begin writeln(bbb,ab,bbb,ba,a,ab,a,ba,b,ab,b,ba,b,b,ab,bb,ba);writeln(
a,a,ab,aa,aa,ba,a,b,ab,ab,aa,ba,b,a,ab,aa,ba,ba);writeln(
a,a,a,ab,aaa,ba);writeln(a,b,a,ab,aba,ba);writeln(a,b,b,ab,abb,ba
);writeln(b,a,a,ab,baa,ba);writeln(b,a,b,ab,bab,ba);writeln(aaa,bb
);writeln(aba,bb);writeln(abb);writeln(bb,baa);writeln(bb,bab)end.

(N.B., на самом деле этот квайн записывается в одну строку.)

Неплохое введение в написание квайнов можно найти, например, в [1, 30]; а неплохую коллекцию – в [30, 18].

Искусство versus ремесло

Основной причиной проведения небольшого эксперимента, ставшего основой настоящего сообщения, явилось желание написать, или, точнее говоря, попробовать написать квайн на входном языке поточного редактора sed. Применение поисковых систем для поиска уже имеющихся решений привело к обнаружению квайна quine.sed [17] из «музея квайнов» [18] (автор: Tsuyusato Kitsune):

s/^/s11^113311;h;s221[1]221122g;s112[2]11222211g;G;s11^22([^3]*22)3322([^22n]*22).22(.*22)$1122122322211/;h;s\1[1]\/\g;s/2[2]/\\/g;G;s/^\([^3]*\)33\([^\n]*\).\(.*\)$/\1\3\2/

(N.B., это одна строка текста.)

Вряд ли у меня вышло бы улучшить (например, сократить) этот квайн. Более того, самостоятельная попытка написать нечто подобное тоже не увенчалась успехом. Поэтому было принято решение действовать более систематичным образом и воспользоваться уже имеющимся в распоряжении математики арсеналом готовых теоретических средств.

Вторая рекурсивная теорема Клини имеет своим следствием утверждение о существовании квайна для любого языка программирования, а конструктивный характер её доказательства дает готовый рецепт для написания такого «саморепликатора» (ниже об этом будет написано подробнее).

Стандартные пособия по теории вычислимости нередко не ограничиваются лишь утверждениями о существовании квайнов, и даже приводят конкретные примеры их конструирования, правда, выбирая при этом, как правило, «удобные» языки программирования, например, прагматические реализации $\text{[math]}$ -исчисления, такие как lisp и его производные.

Попадались интересные исключения, e.g. [35, 36], но для слишком абстрактных машин. Поэтому я решил повторить классический эксперимент с конструированием квайна на основе доказательства рекурсивной теоремы Клини, но выполнить этот эксперимент на языке sed (кстати, всё-равно оказавшемся достаточно удобным для этой задачи, в основном из-за возможности объединения скриптов их конкатенацией).

Обновление (август, 2020): Уже после написания черновика этого сообщения, примеры применения второй рекурсивной теоремы Клини к практическим языкам программирования всё-таки отыскались на просторах интернета. В [53] можно найти генератор квайнов на JavaScript (ECMAScript), а в [54] – похожий генератор, но для C++. Причем в последнем примере, указанная утилита позиционируется как достаточно общий инструмент для добавления рефлексивных возможностей к языку, с ограниченной штатной рефлексией (i.e., сгенерированная программа может как просто печатать свой собственный текст, так и вычислять произвольные функции от него, скажем, находить свою длину).

Возможно читателю также будет интересна аналогичная утилита [55], преобразующая произвольную программу на C в квайн.

Результаты эксперимента говорят о возможности автоматической, или «нетворческой» генерации квайнов, в том числе и на sed.

Эффективность и выбор названия серии сообщений.

Быть может некоторым показалось бы несколько более благозвучным слово вроде «квайноделия», но «квайноводство» подходит куда лучше… От части потому, что, как и обещают стандартные вводные курсы по теории вычислимости, квайны, конструируемые прямым применением [второй рекурсивной] теоремы Клини, обычно получаются, мягко говоря, «неэффективными», как по времени, так и по пространству. Ещё одной метрикой эффективности может быть отношения объёмов данных и кода; специально я не исследовал этот вопрос, так что не могу сказать как с этим обстоят дела у автоматически сгенерированных квайнов, но неверняка неоптимально. :)

Постановка задачи

Пусть квайн хранится в исполняемом файле quine, полученным компиляцией его исходного текста из файла quine.source. Для меня достаточно чисто формального выполнения следующего теста:

./quine any_argument > quine.output
diff quine.source quine.output

или аналогичного теста для интерпретируемого языка (здесь interpreter – исполняемый файл интерпретатора или аналогичная внутренняя команда оболочки):

interpreter quine.source any_argument > quine.output
diff quine.source quine.output

Для sed это соответствует следующему тесту:

echo any_argument | sed -f quine.sed > quine.output
diff quine.sed quine.output

Проверку на тривиальность (в частности, на пустоту) можно выполнять и «вручную» (из-за плохой формализуемости и некоторой субъективности).

То есть, квайн конечного размера (скажем, помещающийся на жесткий диск) должен напечать свой собственный текст за конечное (и разумное время). Абсолютно не важно, будут ли исходный текст и скомпилированная программа весить несколько килобайт или несколько мегабайт. Гораздо важнее, чтобы квайн был истинным, т.е. был непустым, «содержательным», и не использовал «нечестные» рефлексивные возможности (вроде чтения своего исходного текста из файла).

Вводные замечания

В теории вычислимости особо важное место занимают несколько интересных теорем о вычислимых функциях. В этом сообщении я хотел бы кратко рассказать об этих теоремах и о некоторых их применениях.

Для некоторой программы с текстом $\text{[math]}$ соответствующую ей (частичную) вычислимую функцию обычно обозначают как $\text{[math]}$ , однако, воизбежание нагромождения нижних индексов далее будет использоваться несколько более удобное обозначение, широко применяющееся при изучении семантики языков программирования, а именно $\text{[math]}$ .

Обычно, в теории алгоритмов (теории вычислимости, теории рекурсии) говорят о [гёделевском] номере программы, а не о её тексте, но далее будет использоваться более наглядное и привычное, по крайней мере для программистов, слово текст, иногда даже исходный код, без прямого отсыла к понятию нумерации из теории вычислимости. Более того, вразрез с традиционным словоупотреблением, в настоящем сообщении нередко программа и её текст будут отождествляться, – здесь это просто одно и то же. (Краткости и простоты ради, это сообщение будет вообще несколько неформальным и не строгим.)

При одновременном рассмотрении нескольких языков программирования, как, например, при работе с трансляторами, можно указывать язык программирования в нижнем индексе семантических скобок, e.g., $\text{[math]}$ . (Кстати, в литературе встречается и более необычная нотация, например, вообще не используюшая какие-либо индексы и скобки, для экономии места.)

Символом $\text{[math]}$ будет обозначено незавершающееся вычисление, т.е. $\text{[math]}$ – это значение бесконечного цикла. Равенство $\text{[math]}$ есть сокращение для $\text{[math]}$ . (Подразумевается, что для некоторых $\text{[math]}$ , может выполнятся $\text{[math]}$ и $\text{[math]}$ .)

Теорема об универсальной функции

Сначала хотелось бы упомянуть теорему о существовании универсальной программы, а фактически о возможности написания интерпретаторов для любых подходящих (Тьюринг-полных) языков программирования, причем подразумевается, что интерпретатор пишется на его же входном языке. Более формально, эта теорема утверждает, что существуют вычислимая функция — универсальная функция — $\text{[math]}$ , а также соответствующая ей программа-интерпретатор $\text{[math]}$ , такие, что для любой программы $\text{[math]}$ , интерпретатор может быть запущен с несколькими аргументами, первый из которых равен $\text{[math]}$ , а оставшиеся суть просто аргументы для этой программы. Так запущенный интерпретатор должен возвратить тот же результат, что и сама программа $\text{[math]}$ при тех же аргументах.

То есть, $\text{[math]}$ .

Набросок доказательства.

Доказательство может проводится просто предъявлением готового интерпретатора в виде машины Тьюринга, т.е. путем построение т.н. универсальной машины Тьюринга, симулирующей работу любой другой машины Тьюринга. Понятно, что можно использовать и любую другую модель вычислений, e.g., $\text{[math]}$ -исчисление. Но здесь, для краткости, аргументация будет менее конструктивной и более абстрактной.

Естественно считать программами куски текста (i.e., строки) на некотором языке программирования. Пусть на строках определён обычный порядок $\text{[math]}$ , а именно, для строк $\text{[math]}$ и $\text{[math]}$ выполняется $\text{[math]}$ если $\text{[math]}$ (i.e., сравниваются длины) или, в случае $\text{[math]}$ , если $\text{[math]}$ лексикографически предшествует $\text{[math]}$ . Т.о., все программы можно отсортировать относительно $\text{[math]}$ , получив в результате упорядоченную последовательность $\text{[math]}$ . Будем считать, что для любой программы $\text{[math]}$ можно построить специализированное вычислительное устройство $\text{[math]}$ , преобразующее входные данные $\text{[math]}$ в выходные $\text{[math]}$ (эта нотация, по-факту, означает запуск устройства $\text{[math]}$ с аргументом $\text{[math]}$ ).

Теперь можно определить функцию $\text{[math]}$ . Полнота по Тьюрингу позволяет утверждать, что для любой вычислимой функции $\text{[math]}$ существует вычислительное устройство $\text{[math]}$ , такое, что $\text{[math]}$ ; а раз в последовательности $\text{[math]}$ есть вычислительные устройства для всех программ, то найдётся число $\text{[math]}$ , такое, что $\text{[math]}$ . Получается, что $\text{[math]}$ , т.е., функция $\text{[math]}$ может использоваться вместо любой вычислимой функции $\text{[math]}$ если известен её номер $\text{[math]}$ ; другими словами, $\text{[math]}$ – универсальная функция.

Осталось показать, что $\text{[math]}$ вычислима. Для этого надо написать интерпретатор $\text{[math]}$ и сконструирвать соответствующее вычислительное устройство $\text{[math]}$ , по первому аргументу $\text{[math]}$ командной строки извлекающее устройство с индексом $\text{[math]}$ из последовательности $\text{[math]}$ и запускающее его, передавая ему при запуске остальные свои аргументы. Т.е., должно выполняться $\text{[math]}$ . Видно, что $\text{[math]}$ – устройство, вычисляющее $\text{[math]}$ , а $\text{[math]}$ – программа, это делающая. Таким образом, $\text{[math]}$ – вычислимая универсальная функция. $\text{[math]}$

N.B., сама теорема не зависит от языка программирования и требует лишь его полноты по Тьюрингу, т.е. возможности написать для любой вычислимой функции программу, её вычисляющую; да, звучит немного тавтологично, и, тем не менее, есть языки не являющиеся Тьюринг-полными: на них нельзя реализовать некоторые программы, легко пишущиеся на каком-нибудь универсальном, Тьюринг-полном языке. Существуют ли программы, не могущие быть перенесены на машину Тьюринга или любую эквивалентную ей машину, но могущие выполняться на каком-нибудь другом компьютере – интересный философский вопрос; тезис Чёрча-Тьюринга говорит, что нет, таких программ не существует (и действительно, все известные теоретические конструкции более мощных компьютеров конфликтуют с теми или иными физическими законами и в это вселенной работать не могут).

А вот существование вычислимой универсальной функции, по-видимому, не влечёт за собой полноты по Тьюрингу – если взять некоторый подходящий неуниверсальный язык, то можно действовать как в вышеприведенном наброске доказательства, т.е. можно сгенерировать и отсортировать все программы [для этого языка] и вычислительные устройства, а потом определить функцию, выбирающую и использующую нужное устройство по его номеру. Если выбранный язык будет достаточно богат, чтобы на нём можно было выразить такой выбор и запуск, то мы получим вычислимую универсальную функцию, правда, универсальную не для всех вычислимых функций, а только для функций, реализуемых на таком языке.

Фактически, теорема об универсальной функции говорит, что частичная (т.е. не являющаяся всюду определённой) функция $\text{[math]}$ от аргументов $\text{[math]}$ сама является вычислимой (или т.н. частично рекурсивной) функцией $\text{[math]}$ от аргументов $\text{[math]}$ (добавился ещё один аргумент).

Использование теоремы об универсальной функции в данном сообщении будет весьма ограниченным; здесь без неё можно было бы и обойтись (если не считать теорему Роджерса, см. ниже). И всё-же она в определённые моменты будет важна. Кроме этого, стоит обратить внимание на использованное в доказательстве разделение на программы (тексты программ), вычислительные устройства и их номера, – нам пришлось использовать устройства, чтобы подчеркнуть механистичность и физическую реализуемость вычислений, текстовое представление программ, чтобы иметь возможность сортировать и нумеровать программы/устройства, и, наконец, пришлось выбрать конкретный (но не единственный) способ такой нумерации с помощью сортировки по возрастанию относительно порядка $\text{[math]}$ .

В дальнейшем такое разделение представлений будет лишним и поэтому, как я уже говорил ранее, тексты программ, программы и их номера будут отождествляться. Сам конкретный способ нумерации можно будет считать заданием языка программирования, хотя на практике же удобно отождествлять язык программирования с семантической функцией $\text{[math]}$ , сопоставляющей программе $\text{[math]}$ функцию $\text{[math]}$ , где $\text{[math]}$ – множество, над которым определены вычислимые функции (в большинстве случаев можно считать $\text{[math]}$ ) или с парой $\text{[math]}$ . (В следующей части этой серии сообщений, я постараюсь уделить должное внимание понятию нумерации, но здесь оно свою полезность, похоже, пока исчерпало.)

N.B., Также подразумевается, что паре значений $\text{[math]}$ можно сопоставить взаимно однозначным образом $\text{[math]}$ (причем отображение $\text{[math]}$ вычислимо). Это позволяет определять функции с большим количеством аргументов через функции с меньшим количеством, например $\text{[math]}$ . Т.о., теоретически можно вообще обходиться только одноместными функциями, но из соображений удобства, к такому минимализму прибегать, надеюсь, не придётся.

S-m-n теорема Клини

Другой, не менее важной теоремой является т.н. $\text{[math]}$ -теорема (известная также как теорема о параметризации или итеративная теорема) [14, 3], утверждающая, что может быть написана программа, уменьшающая количество аргументов путем фиксации значений некоторых из них: для программы $\text{[math]}$ , реализующей функцию $\text{[math]}$ с $\text{[math]}$ аргументами и для заданных значений $\text{[math]}$ для первых $\text{[math]}$ аргументов существует программа $\text{[math]}$ для специализированной $\text{[math]}$ -местной функции, удовлетворяющая $\text{[math]}$ для любых $\text{[math]}$ .

Также существует вычислимая (примитивно рекурсивная при определённом выборе языка программирования) всюду определённая функция, — собственно, $\text{[math]}$ -функция, — преобразующая программу $\text{[math]}$ в программу $\text{[math]}$ .

То есть, для программы $\text{[math]}$ выполняется $\text{[math]}$ .

Далее пригодится частный случай $\text{[math]}$ с фиксацией всего одного из двух аргументов.

Нетрудно видеть, что $\text{[math]}$ теорема, по-существу, реализует частичные вычисления (специализацию программ) [4, 5], т.е. дает возможность выполнить часть вычислений, зависящих от фиксируемого аргумента(-ов), заранее, до выполнения программы (что может быть использовано, например, для оптимизации кода). Есть некоторое сходство между частичной специализацией и каррингом из функционального программирования.

Доказательство $\text{[math]}$ теоремы конструктивно и может быть основано на явном выписывании программы (или на явном построении машины Тьюринга), присваивающей определенные значения исключаемым аргументам и обеспечивающей запуск программы при поступлении недостающих данных (такого тривиального алгоритма недостаточно для написания оптимизирующего специализатора; но он может быть улучшен).

(Само доказательство здесь приводится не будет, а интересующимся рекомендуется обратиться к первоисточникам или более современным материалам по теории вычислимости.)

Стоит отметить, что вышеприведенные теоремы во многом схожи, и даже в некотором смысле «взаимо-обратны» – теорема об универсальной функции преобразует «статический» параметр — программу — в «динамический» аргумент, который может затем принимать любое значение; $\text{[math]}$ -теорема, напротив, преобразует динамический аргумент в статический, приписывая ему априори заданное значение.

Эта симметрия хорошо видна если выписать ключевые уравнения обоих теорем одно под другим (здесь, для краткости, используется $\text{[math]}$ -функция):

$\text{[math]}$

В некотором смысле, они при этом всё-же различны – кроме структурных различий формул, $\text{[math]}$ -функцию можно считать примитивно рекурсивной (для её реализации не обязательно нужен универсальный язык программирования).

Неподвижные точки вычислимых функций

Далее описывается теорема о существовании неподвижных точек вычислимых функций, известная также как вторая рекурсивная теорема Клини [14]; здесь приводится несколько упрощенная её версия, впрочем, полностью достаточная для решения поставленных задач.

Вторая рекурсивная теорема Клини.

Для любой вычислимой функции $\text{[math]}$ существует программа $\text{[math]}$ («неподвижная точка»), такая, что

$\text{[math]}$

Доказательство.

Напишем программу $\text{[math]}$ , такую, что $\text{[math]}$ . Тогда $\text{[math]}$ .

Действительно, если запустим $\text{[math]}$ для какого-нибудь аргумента $\text{[math]}$ , то получим $\text{[math]}$ . По определению $\text{[math]}$ -функции, $\text{[math]}$ . Теперь применим определение для $\text{[math]}$ и получим, что $\text{[math]}$ . Понятно, что эта цепочка равенств по транзитивности приводит к $\text{[math]}$ . $\text{[math]}$

В данном сообщении особый интерес представляет частный случай $\text{[math]}$ , порождающий квайны: легко видеть, что при этом $\text{[math]}$ , то есть программа $\text{[math]}$ при запуске печатает сама себя, как и положено квайну.

Иногда пригождается другая версия этой теоремы (при определенном выборе языка, строго говоря, не эквивалентная теореме Клини; см. [39]), предложенная в [19]:

Теорема Роджерса.

Для любой всюду определённой вычислимой функции $\text{[math]}$ существует неподвижная точка $\text{[math]}$ , т.е. такая программа $\text{[math]}$ , что $\text{[math]}$ .

Доказательство.

Определим функцию $\text{[math]}$ так, что

$\text{[math]}$
Теперь напишем программу $\text{[math]}$ , такую, что $\text{[math]}$ выполняется
$\text{[math]}$
Утверждается, что $\text{[math]}$ – есть искомая неподвижная точка.

Подстановка (3) в правую часть (2) дает $\text{[math]}$ и $\text{[math]}$ . Последнее уравнение при обозначении $\text{[math]}$ уже соответствует определению неподвижной точки из условия этой теоремы, т.е., $\text{[math]}$ . $\text{[math]}$

N.B., во второй теореме Клини о рекурсии мы можем выбрать любую вычислимую функцию $\text{[math]}$ , даже если она не определена для некоторых значений аргументов (т.е. если соответствующая этой функции программа зависает при таких входных данных); в теореме Роджерса мы можем выбрать только всюду определённую функцию $\text{[math]}$ , иначе в выражении $\text{[math]}$ не было бы смысла при некоторых $\text{[math]}$ .

Из теоремы Клини и теоремы об универсальной функции следует теорема Роджерса, а из теоремы Роджерса и $\text{[math]}$ -теоремы – теорема Клини. (Но есть нюансы [39].)

Для применения теоремы Роджерса к случаю с квайнами, удобно, следуя [2], ввести оператор $\text{[math]}$ , для данного аргумента конструирующий программу, печатающую этот аргумент. Т.е. определение оператора $\text{[math]}$ выглядит как $\text{[math]}$ [и почти соответствует одноименному оператору из, e.g., lisp’а].

Квайны суть неподвижные точки этого оператора [в смысле формулировки теоремы Роджерса].

Доказательство.

Пусть $\text{[math]}$ – неподвижная точка $\text{[math]}$ , т.е. $\text{[math]}$ выполняется $\text{[math]}$ Подстановка определения $\text{[math]}$ в это уравнение дает $\text{[math]}$ . Но $\text{[math]}$ и есть определение квайна. $\text{[math]}$

Примечание.

Вообще, в математике, неподвижной точкой функции $\text{[math]}$ обычно называют значение $\text{[math]}$ , такое, что $\text{[math]}$ (i.e., $\text{[math]}$ оставляет $\text{[math]}$ неизменным). Поэтому «неподвижные точки» из теорем 1 и 2 не совсем соответствуют такому общепринятому определению.

Тем не менее, термин неподвижная точка хорошо отражает суть этих теорем – некоторое преобразование не меняет значение аргумента, т.е. оставляет его неподвижным (более того, из $\text{[math]}$ следует $\text{[math]}$ , i.e. неподвижные точки по Роджерсу очень близки к обычному определению; обратное, впрочем, неверно: рассмотренные теоремы о неподвижной точке вовсе не гарантируют наличия обычной неподвижной точки $\text{[math]}$ , такой, что $\text{[math]}$ ).

Я лишь намереваюсь, в рамках этой серии сообщений, для удобства ввести обозначения для этих «нестандартных» неподвижных точек, а именно, пусть операторы $\text{[math]}$ и $\text{[math]}$ обозначают неподвижные точки [функции $\text{[math]}$ ] из теорем Клини и Роджерса, соответственно. В контексте, требующем работы с несколькими неподвижными точками, эти операторы будут обозначать множества неподвижных точек. Обозначение $\text{[math]}$ будет использоваться для множества традиционных неподвижных точек, $\text{[math]}$ . А так как, в общем случае, неподвижная точка не является единственной, запись типа $\text{[math]}$ пусть означает $\text{[math]}$ (и аналогично для $\text{[math]}$ , $\text{[math]}$ ).

Финальное замечание, полностью оправдывающее название «неподвижная точка» для операторов $\text{[math]}$ и $\text{[math]}$ : введем оператор $\text{[math]}$ , где $\text{[math]}$ – некоторое двуместное отношение. Тогда $\text{[math]}$ . Другие типы неподвижных точек можно теперь тоже определять через $\text{[math]}$ при должном выборе отношения $\text{[math]}$ . Например, пусть отношение $\text{[math]}$ сравнивает программы по их эффекту, т.е., $\text{[math]}$ . Тогда $\text{[math]}$ . (N.B., как обычно, запись $\text{[math]}$ есть сокращение для $\text{[math]}$ ).

Главный эксперимент

В [42] приведен следующий эксперимент по квайногенерации на lisp (автор кода мне не известен):

(define g (quote (lambda (x y) x))) ; g(x, y) = x

(define s11 (quote (lambda (f x) (list (quote lambda)
    (quote (y)) (list f x (quote y)))))) ; from s-m-n theorem

(define m (list (quote lambda) (quote (x y))
    (list g (list s11 (quote x) (quote x)) (quote y))))

(define quine (eval (list s11 m m)))

; tests
(eval (list quine nil))
(eval (list g quine nil))

(В [47] можно найти невероятную коллекцию аналогичных экспериментов со второй рекурсивный теоремой Клини, выполненных на языке scheme, диалекте lisp’а.)

Этот фрагмент кода просто воспроизводит доказательство второй рекурсивной теоремы Клини. Аналогичным образом я действовал и при повторении этого эксперимента на sed. Соответствующий код может быть найден в GitHub-репозитории [46]. Конкретно, в репозитории содержится ряд скриптов, *.sed и *.sh, назначение каждого из которых рассмотренно ниже.

Редактор sed направляет данные со стандартного ввода в основной буфер редактирования (т.н. the pattern space). И т.к. мне не известен способ передачи традиционных аргументов командной строки скрипту для этого редактора, то именно чтение со стандартного ввода было применено в качестве единственного механизма передачи аргументов. При этом, из-за необходимости передачи нескольких аргументов, понадобилось либо ввести разделитель/терминатор (e.g. нулевой байт), либо приписывать значение длины перед каждым аргументом. Как ни странно, изначально был выбран второй метод, в основном из-за отсутствия необходимости в экранировании разделителя.

Итак, далее приведен перечень скриптов с их кратким описанием:

construct-input.sh принимает на вход список файлов со значениями аргументов и формирует пакет аргументов из них, т.е. читает эти значения и посылает на стандартный вывод, снабдив заголовками (длинами). Формат пакета данных с аргументами выглядит так:
```
<длина аргумента 1>...<длина аргумента n><аргумент 1>...<аргумент n>
```
Длина каждого аргумента представлена двоичным шестнадцатиразрядным числом (т.е. этот формат не отличается универсальностью, но этого хватает для практического применения).
Скрипт s11.sed [тривиально] реализует $\text{[math]}$ -функцию. Этот сценарий принимает исходную программу $\text{[math]}$ в первом аргументе и фиксируемый аргумент $\text{[math]}$ для неё – во втором своем аргументе. Результатом работы скрипта будет другая программа, полученная путем приписывания к $\text{[math]}$ небольшого «инъектора» – фрагмента кода, встраивающего ранее принятый аргумент $\text{[math]}$ (и теперь являющийся частью инъектора) перед новым аргументом $\text{[math]}$ (который будет передан формируемой программе при её запуске). После модификации пакета аргументов, инъектор передаёт управление программе $\text{[math]}$ так, что она «видит» пару аргументов $\text{[math]}$ и $\text{[math]}$ , несмотря на то, что при запуске ей был передан единственный аргумент $\text{[math]}$ .

Небольшая техническая сложность заключается в необходимости экранирования специальных символов в аргументе $\text{[math]}$ при формировании инъектора (с $\text{[math]}$ , встроенным в него). Экранирование производится в соответствии с синтаксисом регулярных выражений sed, путем добавления символа\ перед некоторыми символами, вроде того же \ или перевода строки \n.
minifier.sed используется для удаления ненужных символов (пустые строки, комментарии). При генерации квайна этот скрипт применяется для опционального «сжатия» скриптов s11.sed и duplicate-first.sed, что впоследствии уменьшает размер и увеличивает скорость работы результирующего квайна.
is-quine.sh – простой shell-скрипт, проверяющий переданный ему в аргументах sed-скрипт и определяющий, является ли он квайном.
generate.sh производит «минификацию» скриптов s11.sed и duplicate-first.sed, после чего запускает generate-q.sh, а после его завершения проверяет готовый продукт — квайн в файле q.sed — с помощью скрипта is-quine.sh
duplicate-first.sed принимает два аргумента $\text{[math]}$ и $\text{[math]}$ и заменяет второй первым, т.е., игнорирует $\text{[math]}$ и формирует пакет из двух одинаковых аргументов $\text{[math]}$ и $\text{[math]}$ .
generate-e.sh конструирует программу $\text{[math]}$ из доказательства теоремы Клини. Для этого [минифицированный, сжатый] код программы duplicate-first.sed добавляется в начало [тоже сжатого] s11.sed и объединённый код сохраняется в e.sed. При запуске $\text{[math]}$ , как и требуется, будет выполняться $\text{[math]}$ , т.е. сначала второй аргумент будет заменен первым (с помощью кода из duplicate-first.sed), затем управление будет передано коду $\text{[math]}$ -функции из s11.sed.
generate-q.sh сначала запускает generate-e.sh для создания e.sed, потом запускает s11.sed (или его сжатую версию, хотя здесь это не имеет значения) передав ему в качестве обоих его аргументов содержимое только что сгенерированного e.sed. (N.B., generate-e.sh использовал содержимое s11.sed для генерации e.sed на его основе; в данном же случае, скрипту generate-q.sh не требуется доступ к тексту s11.sed, но лишь возможность его выполнения; по той же причине здесь не используется duplicate-first.sed)
first-only.sed из двух переданных ему аргументов возвращает только первый. Реализует $\text{[math]}$ -комбинатор из комбинаторной логики и $\text{[math]}$ -исчисления. В дистрибутив/репозиторий включен просто для демонстрации, хотя, в соответствии с доказательством теоремы Клини, является реализацией функции $\text{[math]}$ , позже использовавшейся для доказательства существования квайна.
concat.sed возвращет объединённые значения обоих аргументов; никакие заголовки в результат не включаются. На деле, concat.sed включен в репозиторий только для демонстрации – скрипт generate-e.sh не использует concat.sed, а производит объединение текстов просто последовательным копированием оных в целевой файл.

(Заметьте, последние два скрипта, first-only.sed и concat.sed концептуально не являются лишними и они могли бы быть использованы, но по-факту, в ходе оптимизации, были заменены аналогичными средствами командной оболочки, – для эффективности.)

Для генерации квайна достаточно запустить ./generate.sh, в результате чего в том же каталоге [через некоторое время] должен появиться файл q.sed, являющийся искомым квайном на sed.

Промежуточные итоги

Описание основного эксперимента завершено (и я рекомендую немного поизучать код скриптов из репозитория). Но о квайнах рассказать можно ещё многое. А некоторые вопросы остаются вовсе малоизученными, фактически, открытыми.

Несмотря на приведенные доказательста теорем о неподвижных точках (Клини и Роджерса), кому-то, может быть, хотелось бы глубже понять структуру этих и подобных им доказательств. Поэтому ниже я приведу некоторые дополнительные сведения с примерами. К концу сообщения я попробуя немного задеть некоторые из философских аспектов квайнов и теории вычислимости. И, пожалуй, завершу изложение попыткой сформулировать интересующие меня, но пока не имеющие официального ответа открытые вопросы.

Надеюсь, это не последнее сообщение этой серии. Поэтому, темы, не затронутые здесь, будут, по возможности, обсуждаться позже в других частях.

Дополнительная теория

Проблема остановки

Проблемой останова(-ки) называют задачу определения завершаемости произвольной программы по её коду. Известна теорема об алгоритмической неразрешимости такой задачи, т.е. о невозможности построения алгоритма, устанавливающего для произвольной программы конечность времени её выполнения [8].

Доказательство 1.

В пользу этого утверждения можно привести такие доводы. Введем функцию $\text{[math]}$ , определённую для всех $\text{[math]}$ , которая в качестве своих аргументов принимает текст некоторой программы $\text{[math]}$ и входные данные $\text{[math]}$ этой программы, после чего возвращает 1 если эта программа завершается за конечное время, и 0 – если программа «зависает»:

$\text{[math]}$

Пусть $\text{[math]}$ – любая вычислимая (реализуемая в виде компьютерной программы) функция двух аргументов, способная обрабатывать тексты программ. Напишем программу $\text{[math]}$ так, чтобы выполнялось:

$\text{[math]}$

Т.е. $\text{[math]}$ передаёт свой аргумент функции $\text{[math]}$ и если та возвращает ноль, то ноль (или любое другое конечное значение) возвращает и $\text{[math]}$ , но в противном случае $\text{[math]}$ возвращает неопределенное значение, а именно зависает, входя в бесконечный цикл.

Так как $\text{[math]}$ тоже реализуема в виде программы (т.е. вычислима), то получение значения $\text{[math]}$ можно считать обычным вызовом подпрограммы. Все остальные действия (проверка на равенство нулю, возврат результата, условный переход, бесконечный цикл) тоже выполнимы на любом комппьютере.

Теперь мы можем передать программе $\text{[math]}$ её собственный текст; тогда, если $\text{[math]}$ , то и $\text{[math]}$ . Другими словами, в этом случае $\text{[math]}$ возвращает результат и завершается, т.е. $\text{[math]}$ . Если же $\text{[math]}$ , то $\text{[math]}$ зависает и таким образом $\text{[math]}$ .

В любом случае, из этого получается, что $\text{[math]}$ . Таким образом, функция $\text{[math]}$ не совпадает [хотя бы в одной точке] с вычислимой $\text{[math]}$ . А из произвольности выбора функции $\text{[math]}$ немедленно вытекает, что функция $\text{[math]}$ не совпадает вообще ни с одной вычислимой функцией, т.е. $\text{[math]}$ невычислима (в смысле несуществования программы, вычисляющей значение этой функции для всех программ). $\text{[math]}$

Доказательство 2.

Интересно, что можно воспользоваться теоремой Клини и попробовать доказать проблему останова методом «от противного».

Допустим, определённая выше функция останова $\text{[math]}$ – вычислимая. Определим вычислимую функцию

$\text{[math]}$
Вторая рекурсивная теорема говорит, что $\text{[math]}$ . Определение равенства вычислимых функций, определение $\text{[math]}$ и определение функции останова дают следующие цепочки логических эквавалентностей
$\text{[math]}$
Пришли к противоречию; значит, функция $\text{[math]}$ не является вычислимой. $\text{[math]}$

Диагонализация

Схема первого доказательства для проблемы останова фактически основана на процедуре диагонализации [6]. Второе доказательство, впрочем, тоже: ведь оно использует теорему Клини, доказательство которой также основано на диагонализации. Далее я попытаюсь пояснить суть этого процесса. Итак, если у нас есть некоторая бесконечная матрица $\text{[math]}$ (верхний индекс нумерует строки, нижний – столбцы), то мы можем построить вектор-строку $\text{[math]}$ , не совпадающий ни с одной из строк матрицы. Для этого достаточно лишь каким-то образом преобразовать элементы диагонали (отсюда название метода) матрицы $\text{[math]}$ так, чтобы для любого $\text{[math]}$ выполнялось $\text{[math]}$ (например, $\text{[math]}$ ).

Действительно, предположим, что $\text{[math]}$ равен одной из строк матрицы $\text{[math]}$ . Это означает, что существует такой индекс $\text{[math]}$ , что $\text{[math]}$ для всех $\text{[math]}$ . Однако, по-построению $\text{[math]}$ , при $\text{[math]}$ имеет место неравенство $\text{[math]}$ ; противоречие. Следовательно, мы действительно построили новый объект $\text{[math]}$ , не входящий в матрицу $\text{[math]}$ .

Примечание.

Название метода (диагонализация) несколько условно, т.к., по-видимому, достаточно чтобы в каждой строке был хотя-бы один преобразуемый элемент, совсем не обязательно лежащий на главной диагонали. [44] (Правда, нужно учитывать, что перестановкой строк можно вернуть преобразуемые элементы на диагональ матрицы; это замечание пока имеет интуитивный характер и детального анализа здесь не будет.)

Возможно, что пока применение этого трюка с конструированием патологической строки матрицы может показаться далёким от приведенных доказательств разбираемых здесь теорем (Клини, Роджерса и проблемы остановки); поэтому представляется нелишним небольшое продвижение ближе к историческим основам метода, и, я надеюсь, это сразу прояснит связь по крайней мере с проблемой останова. А вот теоремы о неподвижных точках потребуют большего внимания… Итак, сейчас копнём вглубь истории.

Теорема Кантора

Изначально, диагональный метод был разработан и применен Кантором [7] для доказательства существования множеств, больших любого счетного бесконечного множества, или, точнее говоря, для доказательства несуществования сюръекции $\text{[math]}$ , где $\text{[math]}$ – булеан множества $\text{[math]}$ . Можно выразить теорему Кантора так: $\text{[math]}$ . В более общем виде, теорема Кантора говорит о несуществовании сюръекции $\text{[math]}$ , где $\text{[math]}$ , $\text{[math]}$ – некоторые множества (причем $\text{[math]}$ должно быть невырожденным, например в смысле существования беспорядка $\text{[math]}$ , т.е., перестановки без неподвижных точек), а $\text{[math]}$ – множество всех функций $\text{[math]}$ (структурно, обозначение $\text{[math]}$ соответствует формуле $\text{[math]}$ для подсчета количества таких функций).

Рассмотрим более детально пример с $\text{[math]}$ .

Мы можем закодировать произвольное подмножество $\text{[math]}$ двоичной маской, т.е. последовательностью $\text{[math]}$ , такой, что $\text{[math]}$ если $\text{[math]}$ и $\text{[math]}$ если $\text{[math]}$ .

После этого мы сможем определить матрицу $\text{[math]}$ (бесконечных размеров), каждая строка $\text{[math]}$ которой будет содержать двоичную маску для каждого подмножества $\text{[math]}$ . Теперь мы применим к диагональным элементам $\text{[math]}$ матрицы операцию инвертирования $\text{[math]}$ (т.е. $\text{[math]}$ и $\text{[math]}$ ), в результате чего получим новый бесконечный вектор-строку $\text{[math]}$ , который не будет совпадать ни с одной из строк матрицы.

Т.е. мы получили совершенно новый объект, имеющий конкретное описание в виде двоичной последовательности, тоже могущей быть двоичной маской для некоторого подмножества $\text{[math]}$ , но не входящей в матрицу $\text{[math]}$ . Этот пример показывает, что раз строки матрицы пронумерованы числами $\text{[math]}$ , а мы получили «лишнюю» двоичную маску, определяющую некое «лишнее» подмножество $\text{[math]}$ , то множество всех подмножеств $\text{[math]}$ , содержащее это лишнее подмножество и обозначаемое $\text{[math]}$ , строго больше самого $\text{[math]}$ ; выражение «строго больше» означает, что в $\text{[math]}$ есть лишние, дополнительные элементы и нельзя определить какую-нибудь функцию из $\text{[math]}$ на $\text{[math]}$ , т.е. такую функцию, чтобы у каждого элемента $\text{[math]}$ был прообраз.

Применительно же к проблеме останова, в качестве бесконечной матрицы используются значения $\text{[math]}$ , т.е. строки соответствуют функциям. Причем диагональные значения оборачиваются в функцию $\text{[math]}$ так, чтобы функция останова $\text{[math]}$ [хотя бы на диагональных элементах матрицы] возвращала результат, отличный от результата применения $\text{[math]}$ к тем же аргументам.

Теорема Ловера

Уильям Ловер предложил [43] обобщенную теорему из которой следуют многие другие результаты диагонализации, включая и проблему останова и теорему Гёделя о неполноте и некоторые другие. См. [44] для изложения тех же результатов на языке теории множеств (работа [43] сформулирована с существенным привлечением теории категорий).

Связь диагонализации с теоремами о неподвижной точке

(Этот подраздел добавлен через месяцы после размещения в моем дневнике первой версии этого сообщения. Добавить новый подраздел, демонстрирующий роль диагонализации при поиске неподвижных точек, я решил после того как однажды прочитал своё же сообщение и не увидел чётких следов диагонального процесса в приведенных доказательствах теорем Клини и Роджерса, кроме характерного приема с самоприменением программ… Материал в основном написан по мотивам [56].)

В рассмотренных выше примерах применения диагонального процесса мы определяли множество всех объектов определённого типа, представляли их строками матрицы, а затем применяли некоторую операцию к диагональным элементам и т.о. конструировали новый объект, не могущий быть описанным ни одной строкой матрицы. Но при поиске неподвижной точки, как в теоремах Клини и Роджерса, требуется, наоборот, построить или найти объект с требуемыми свойствами в исходном наборе, а не доказать, что его там нет. Причем же тут диагонализация?

Все дело в том, что если нам удается построить новую последовательность $\text{[math]}$ (иногда называемую антидиагональю [ которую не следует путать с побочной диагональю матрицы]), путем применения некоего преобразования $\text{[math]}$ к диагональным элементам матрицы $\text{[math]}$ , то мы, как уже было сказано ранее, можем быть уверены, что среди строк матрицы $\text{[math]}$ объекта $\text{[math]}$ нет. Но если по какой-то причине «антидиагональный» объект $\text{[math]}$ построить не получается, то среди строк матрицы $\text{[math]}$ может оказаться её диагональ. Т.е. возможно существует индекс $\text{[math]}$ , такой, что $\text{[math]}$ .

Нас интересует случай замкнутости набора строк матрицы относительно действия $\text{[math]}$ : для любой строки $\text{[math]}$ существует строка $\text{[math]}$ равная образу $\text{[math]}$ , т.е., $\text{[math]}$ . Итак, если диагональ матрицы равна её строке $\text{[math]}$ , то в силу замкнутости строк относительно $\text{[math]}$ , существует строка $\text{[math]}$ , а так как $\text{[math]}$ , то и образ диагонали под действием $\text{[math]}$ тоже оказывается среди строк: $\text{[math]}$ .

Но если результат преобразования диагонали равен одной из строк, то это означает, что на пересечении этой строки с главной диагональю матрицы есть элемент, переходящий в себя под действием преобразования $\text{[math]}$ . Другими словами, $\text{[math]}$ , i.e., $\text{[math]}$ – неподвижная точка $\text{[math]}$ .

Возможно, в визуализации этой идеи поможет следующий рисунок (матрица $\text{[math]}$ схематично изображена в виде таблицы; вместо каких-либо конкретных значений её ячеек используется символ $\text{[math]}$ ):

$\text{[math]}$

Ну вот, связь диагонализации и неподвижных точек в общих чертах продемонстрирована. Осталось выяснить, что же может пойти не так при построении вектора $\text{[math]}$ . Напомню, что в случае с теоремой Кантора и проблемой останова диагонализация проходила успешно… Разгадка здесь всего-лишь в том, что в случае с неподвижными точками мы не строим функцию $\text{[math]}$ специально так, чтобы у неё не было неподвижных точек. И лишь предполагая, допуская их наличие, мы применяем диагональный процесс для конструирования такой неподвижной точки. Получив же конкретное решение, можно легко убедиться, что это действительно неподвижная точка; с тем же успехом, мы могли бы просто угадать вид решения, а потом убедиться в его правильности. Т.о., если отбросить вариант с угадыванием, то конструктивный характер диагональной схемы существенен для её логической основы: мы создаём объект с нужными свойствами и назад пути уже нет в силу непротиворечивости используемых формальных систем (ведь если выведено некоторое утверждение, вывести его отрицание в таких системах уже не получится). (Рекомендую также глянуть интересное обсуждение логической основы диагонализации в [57].)

Пример приведем для теоремы Роджерса, более удобной из-за одноместности фигурирующей в ней функции. Требуется решить уравнение $\text{[math]}$ относительно $\text{[math]}$ для любой всюду определённой вычислимой $\text{[math]}$ . В соответствии с вышеизложенной схемой доказательства диагонализацией, далее предстоит определить матрицу $\text{[math]}$ и преобразование $\text{[math]}$ так, чтобы неподвижная точка функции $\text{[math]}$ подходила бы в качестве решения к уравнению из теоремы Роджерса.

По техническим причинам, о которых ещё будет сказано позже, вместо функции $\text{[math]}$ мы введем отношение $\text{[math]}$ (его конкретный вид будет определён ниже). Вместо $\text{[math]}$ будем писать $\text{[math]}$ ; в частности, если некоторая функция $\text{[math]}$ – искомая неподвижная точка, то будет выполняться $\text{[math]}$ . К строкам матрицы и вообще к последовательностям это отношение применяется поэлементно.

Пусть элементы матрицы равны $\text{[math]}$ . Т.е. строка с индексом $\text{[math]}$ соответствует вычислимой функции с номером $\text{[math]}$ ; номера столбцов соответствуют значениям аргументов. (Заметьте, что элементы матрицы $\text{[math]}$ равны не самим значениям $\text{[math]}$ , а вычислимым функциям с номерами $\text{[math]}$ .) Если $\text{[math]}$ для некоторых $\text{[math]}$ и $\text{[math]}$ , то считается, что элемент $\text{[math]}$ содержит нигде не определённую функцию: $\text{[math]}$ . Диагональ $\text{[math]}$ обозначим $\text{[math]}$ и будем считать $\text{[math]}$ .

Если некоторый гипотетический объект $\text{[math]}$ , для которого справедливо $\text{[math]}$ не является «патологическим», т.е. гарантированно отсутствующим среди строк матрицы, то диагональ может оказаться равной одной из строк.

Мы можем определить функцию $\text{[math]}$ , конструирующую программу, которая принимая аргумент $\text{[math]}$ , применяет к нему диагональный элемент матрицы, находящийся на пересечении строки $\text{[math]}$ и столбца $\text{[math]}$ . А именно, выполняется

$\text{[math]}$
Важно, что для вычисления $\text{[math]}$ тоже можно написать программу $\text{[math]}$ , т.е. $\text{[math]}$ – вычислимая функция. Это означает, что в матрице $\text{[math]}$ существует строка $\text{[math]}$ равная $\text{[math]}$ ; действительно, из того, что $\text{[math]}$ является программой для $\text{[math]}$ , а также из определения элементов $\text{[math]}$ и из $\text{[math]}$ следует $\text{[math]}$ . Если набор строк замкнут относительно $\text{[math]}$ , то существует строка $\text{[math]}$ ; и именно её пересечение с $\text{[math]}$ дает неподвижную точку: $\text{[math]}$ .

Чтобы последнее уравнение выглядело как уравнение из теоремы Роджерса, определим отношение $\text{[math]}$ так, что для функций $\text{[math]}$ и $\text{[math]}$ выполняется $\text{[math]}$ . Попробуем показать, что $\text{[math]}$ . Пусть $\text{[math]}$ – такая последовательность, что $\text{[math]}$ . Из определений элементов матрицы $\text{[math]}$ и отношения $\text{[math]}$ следует $\text{[math]}$ и $\text{[math]}$ . В силу вычислимости $\text{[math]}$ , композиция $\text{[math]}$ тоже вычислима и имеет некоторый индекс $\text{[math]}$ , т.е., $\text{[math]}$ . В соответствии с определением элементов матрицы $\text{[math]}$ , это выражение означает, что $\text{[math]}$ равна строке с индексом $\text{[math]}$ . Т.о., мы только что показали, что набор строк замкнут относительно $\text{[math]}$ .

Выше было установлено, что $\text{[math]}$ . Левую часть перепишем с помощью $\text{[math]}$ , учитывая равенство $\text{[math]}$ , а правую – с помощью определения элементов матрицы $\text{[math]}$ . Это даёт $\text{[math]}$ . Из определения отношения $\text{[math]}$ следует, что $\text{[math]}$ . Это уравнение говорит, что $\text{[math]}$ – один из возможных текстов программ, вычисляющих композицию функций $\text{[math]}$ ; кроме того, то же самое уравнение вместе с $\text{[math]}$ в случае с $\text{[math]}$ немедленно даёт $\text{[math]}$ . Таким образом, $\text{[math]}$ , где $\text{[math]}$ является программой для вычисления композиции $\text{[math]}$ , – искомая неподвижная точка из теоремы Роджерса, т.е., $\text{[math]}$ .

Да, это построение выглядит более громоздким и запутанным чем изначально приведенное почти однострочное доказательство теоремы Роджерса, но оно, я надеюсь, позволяет более глубоко увидеть связь диагонального процесса с теоремами о неподвижных точках.

Примечание.

Ранее я говорил, что лучше использовать отношение $\text{[math]}$ вместо функции $\text{[math]}$ . Чтобы неподвижная точка $\text{[math]}$ функции $\text{[math]}$ удовлетворяла уравнению $\text{[math]}$ , можно было бы определить $\text{[math]}$ как $\text{[math]}$ . В принципе, та же схема доказательства работала бы и в этом случае: сначала мы бы выяснили, что строки замкнуты относительно $\text{[math]}$ , затем преобразовали бы строку $\text{[math]}$ , равную диагонали $\text{[math]}$ , и получили бы новую строку $\text{[math]}$ ; завершилось бы такое доказательство проверкой, что элемент $\text{[math]}$ , находящийся на пересечении $\text{[math]}$ и $\text{[math]}$ , удовлетворяет уравнению $\text{[math]}$ .

Пусть некоторый элемент в $\text{[math]}$ равен $\text{[math]}$ для некоторого $\text{[math]}$ . Тогда соответствующий элемент в $\text{[math]}$ равен $\text{[math]}$ и равенство последовательностей $\text{[math]}$ означает, что $\text{[math]}$ . В строке $\text{[math]}$ элементу $\text{[math]}$ из строки $\text{[math]}$ соответствует элемент $\text{[math]}$ . Проблема в том, что исходный элемент $\text{[math]}$ из $\text{[math]}$ , под действием преобразования $\text{[math]}$ должен перейти в $\text{[math]}$ и мы вынуждены потребовать, чтобы этот результат совпадал с $\text{[math]}$ , ведь иначе нельзя будет говорить о $\text{[math]}$ если $\text{[math]}$ будет желаемым элементом на пересечении $\text{[math]}$ и $\text{[math]}$ .

Другими словами, из равенства $\text{[math]}$ должно следовать $\text{[math]}$ , а для этого требуется экстенсиональность функции $\text{[math]}$ – должно выполняться $\text{[math]}$ , i.e., одинаково ведущие себя программы, должны преобразовываться функцией $\text{[math]}$ снова в одинаково себя ведущие, однако не всякая вычислимая функция обладает такой формой монотонности. Трюк с заменой преобразования $\text{[math]}$ (вместе с обычным сравнением функций) отношением $\text{[math]}$ , позволяет обойти это ограничение и расширить класс пригодных функций до всех вычислимых всюду определённых.

Версия «от противного».

Рассуждения по схеме «а вдруг», могут показаться не всегда удовлетворительными. Можно ли вместо попытки сконструировать желаемый объект — неподвижную точку — вопреки диагонализации (призванной доказать невозможность подобного мероприятия) попробовать облачить вышеизложенное в привычную схему доказательства от противного? Такое доказательство выглядело бы более привычно и ощущалось бы более весомым (ведь доказательство от противного основано на надёжном процессе поиска ошибки в цепочке умозаключений, приведших к абсурду; такой поиск призван, в итоге, локализовать ошибку, загнав её в единственный туманный уголок доказательства, а именно, в самое его начальное предположение, после чего способ исправления ошибки — отрицанием предположения — немедленно следует из закона исключённого третьего, и, таким образом любые претензии к качеству такого доказательства сводятся к вере в этот закон). Оказывается, что, да, доказательство, одновременно явно использующее диагонализацию и показывающее наличие неподвижной точки методом от противного, существует, и, в общем-то, общеизвестно.

Итак. Определим бинарное отношение $\text{[math]}$ так, что $\text{[math]}$ .

Теорема (переформулировка теоремы Роджерса).

Если $\text{[math]}$ – всюду определённая вычислимая функция, то $\text{[math]}$ .

Доказательство теоремы Роджерса методом от противного.

(N.B., Акцент в этой версии доказательства сделан на диагонализации, пусть и в ущерб конструктивности, — здесь я не буду выводить явный вид неподвижной точки, хотя при желании его можно извлечь и из такой урезанной версии.)

Основное предположение: $\text{[math]}$ .

Лемма 1 (без доказательства). Для любой вычислимой функции $\text{[math]}$ существует вычислимая всюду определённая $\text{[math]}$ (т.н., $\text{[math]}$ -продолжение функции $\text{[math]}$ ), такая, что $\text{[math]}$ .

Определим вычислимую всюду определённую функцию $\text{[math]}$ , такую, что $\text{[math]}$ .

Утверждение 1. Не существует вычислимой функции $\text{[math]}$ , такой, что $\text{[math]}$ (иначе это бы противоречило определению универсальной функции $\text{[math]}$ ).

(N.B., конкретный вид $\text{[math]}$ на самом деле не важен, — требуется лишь справедливость утверждения 1, — но здесь мы всё-таки зафиксируем такое «диагональное» выражение, и даже воспользуемся им в конце этого подраздела для лучшей визуализации процесса.)

По лемме 1, $\text{[math]}$ , т.е., $\text{[math]}$ . Определим функцию $\text{[math]}$ . Т.к. $\text{[math]}$ и $\text{[math]}$ и их композиция $\text{[math]}$ – вычислима. Допустим, $\text{[math]}$ . Это вместе с $\text{[math]}$ и с определением отношения $\text{[math]}$ ведет к $\text{[math]}$ , из чего следует $\text{[math]}$ . Но $\text{[math]}$ , откуда $\text{[math]}$ , однако по основному предположению, $\text{[math]}$ ( $\text{[math]}$ выглядит как неподвижная точка, но мы предполагаем, что их не существует). Противоречие, значит, $\text{[math]}$ отличается всюду от $\text{[math]}$ . Но это противоречит уже утверждению 1. Следовательно, основное предположение неверно и мы должны его исправить, заменив на $\text{[math]}$ . $\text{[math]}$

Обратите внимание, здесь мы имеем дело с матрицей $\text{[math]}$ в которой строки, как и прежде, соответствуют вычислимым функциям, а столбцы – их аргументам (изменились только сами элементы матрицы). Функция $\text{[math]}$ порождена диагональю $\text{[math]}$ . Лемма 1 говорит, что в матрице $\text{[math]}$ присутствует строка $\text{[math]}$ (отношение $\text{[math]}$ применено поэлементно). Мы используем эту строку для конструирования кандидата в антидиагональ, а именно мы действуем на $\text{[math]}$ данной вычислимой функцией $\text{[math]}$ , но т.к. строка $\text{[math]}$ соответствует функции $\text{[math]}$ , а композиция $\text{[math]}$ вычислима, то среди строк должна найтись строка $\text{[math]}$ (пересекающая диагональ в некоторой точке).

Откуда же тогда берутся подозрения в антидиагональности $\text{[math]}$ , т.е. в том, что $\text{[math]}$ ? Мы знаем, что $\text{[math]}$ (так мы строили строку $\text{[math]}$ ). Теперь если для какого-то $\text{[math]}$ верно $\text{[math]}$ , то в строке $\text{[math]}$ найдётся элемент $\text{[math]}$ , но по определению элементов матрицы $\text{[math]}$ , $\text{[math]}$ , откуда и вытекает выражение $\text{[math]}$ , противоречащее основному предположению [о несуществовании неподвижной точки $\text{[math]}$ ], а значит опровергающее, методом от противного, наше предположение о том, что $\text{[math]}$ совпадает с $\text{[math]}$ в точке $\text{[math]}$ .

На данный момент мы имеем уже два утверждения: одно говорит о том, что антидиагональ на самом деле равна строке $\text{[math]}$ и пересекается с диагональю в некоторой точке, а второе утверждение говорит, что антидиагональ действительно нигде не совпадает с диагональю. Эти утверждения противоречат друг другу, что абсурдно, и, опять методом от противного, приводит к утверждению, прямо противоположному основному предположению об отсутствии неподвижных точек у данной функции $\text{[math]}$ .

Я специально воспроизвел последнее доказательство от противного в уже знакомых терминах матриц, диагоналей, строк, антидиагоналей, и т.д., чтобы придать максимальную наглядность процессу и окончательно удалить мистический налёт с диагонального доказательства теоремы о рекурсии.

Немного о пределах познаваемости

Проблема останова разрешима для многих систем, например, для конечных автоматов, коими, кстати говоря, и являются реальные компьютеры. Правда, в силу огромного количества состояний таких автоматов, они, с практической точки зрения, хорошо моделируются машиной Тьюринга (или эквивалентными моделями, типа лямбда-исчисления). Поэтому, многие теоретические результаты, вытекающие из проблемы останова или доказываемые редукцией к ней, по прежнему применимы в обычном программировании.

Также проблема останова может быть вполне разрешимой для определенных частных случаев. Например, в теории, антивирусы невозможны (это доказывается редукцией к проблеме остановки), но они всё-таки ~~вертятся~~ существуют как программные продукты (в том числе, благодаря «маркетингу», наверное). В теории, невозможно написать программу-детектор, безошибочно определяющую, что другая программа печатает на экране, например, слово «привет» [28, 29]. Но ведь многие бы без труда написали такой детектор. Даже сами доказательства теорем, в силу соответствия Карри-Ховарда, вообще говоря, требуют решения проблемы остановки. Но ведь математики как-то доказывают теоремы! Иногда при помощи компьютера (и автоматизированно и даже автоматически).

Эти исключения не являются ошибками или фактами, опровергающими упомянутые контринтуитивные утверждения (содержащие квантор всеобщности). А положительные результаты имеют вполне конкретное применение. Компиляторы, интерпретаторы, квайны и многие другие интересные артефакты теории вычислимости существуют не только теоретически, но и имеют осязаемые реализации в виде реальных кусков кода и даже устройств (e.g. те же компьютеры). А теорема Гёделя о неполноте говорит, что некоторые теоремы просто не могут быть доказаны, – не стоит даже и пытаться.

Наконец, диагонализация внесла некоторый вклад и в более абстрактные области философии. Например, применением диагонального процесса к демону Лапласа — «древнему» суперкомпьютеру, имеющему неограниченный доступ к любой информации обо всех частицах вселенной — была установлена «монотеистическая» теорема о невозможности существования более чем одного демона Лапласа [27].

В следующих сообщениях этой серии я напишу о некоторых из этих [как классических, так и относительно новых] результатов подробнее.

Другие подходы и «слегка открытые» вопросы

В этом разделе обсуждаются достаточно простые, но до сих пор представляющие некоторый исследовательский интерес альтернативные подходы к конструированию квайнов. Некоторые из рассмотренных здесь вопросов могут быть тривиальными и, возможно, представляющими сложность лишь для меня; другие – могут оказаться объективно стоящими дальнейшей проработки.

Более подробно все эти воросы будет или не будут освещены в следующем(-их) сообщении(-ях) этой серии.

«Креацианизм» vs. «абиогенез»

Я условно назвал совокупность методов (как ручных, так и автоматических), применяемых для конструирования квайнов и основанных на существенном привнесении специально подготовленной внешней информации/знаний в этот процесс [квайнологическим] «креацианизмом». Традиционное написание квайна вручную, а также его конструирования на основе второй рекурсивной теоремы Клини – суть примеры креацианисткого подхода в квайнологии. В них требуется существенный контроль со стороны программиста.

В подразделах же, приведенных ниже, акцент сделан на автоматическом итеративном конструировании квайнов (если оно возможно). «Абиогенетическое», самостоятельное «зарождение» квайнов потенциально могло бы представлять некоторую ценность в ряде областей. Так, например, квайнологический абиогенез был бы интересен в таком разделе информационной безопасности как компьютерная вирусология; он был бы применим в автономных системах (e.g., самомодифицирующееся ПО каких-нибудь марсоходов) и, возможно, интересен экзобиологам (в том смысле, что квайны, будучи «дистиллированной» моделью жизни, подошли бы для изучения тварей с terra incognita, – будь-то океанские впадины, астероиды, космическая пыль/мусор, или любые другие субстраты).

Кимианские квайны и итеративное вычисление неподвижной точки

Хофштадтер в [26] не только ввел термин «квайн», но и описал там же ещё одну разновидность самореплицирующегося кода – кимианские квайны, названные в честь Скотта Кима (Scott Kim), подсказавшего эту идею Хофштадтеру.

Кимианский квайн представляет собой текст, который будучи поданым на вход компилятора/интерпретатора, не распознается как корректный исходный текст, а приводит к выводу сообщения об ошибке [31]. Причём такое сообщение побуквенно совпадает с самим кимианским квайном. Т.е. при попытке запуска или компиляции, подобный код всё-таки воспроизводит себя, как и положено квайну.

Если обозначить среду исполнения для кимианского квайна (e.g., компилятор, интерпретатор или командную оболочку) как функцию $\text{[math]}$ , принимающую и возвращающую текстовую строку, то некоторый кимианский квайн $\text{[math]}$ будет неподвижной точкой этой функции: $\text{[math]}$ .

Интересно, что в данном случае $\text{[math]}$ может быть вычислен итерированием функции $\text{[math]}$ начиная с подходящего (иногда пустого) начального приближения. Т.е. алгоритм конструирования кимианского квайна должен будет вычислить $\text{[math]}$ , где $\text{[math]}$ , $\text{[math]}$ для некоторого начального значения $\text{[math]}$ .

Следует заметить, что такая функция $\text{[math]}$ определена для всех $\text{[math]}$ (и к тому же всегда завершается, если речь идет о компиляторе без поддержки вычислительно-универсальных металингвистических средств, — например, подобных C++ шаблонам, — могущих приводить к «зависанию» компилятора).

В минирепозитории (gist) [33] можно найти простую реализацию подобного метода итеративного конструирования кимианского квайна, выполненную на языке командной оболочки bash. Скрипт принимает в качестве аргумента путь до исполняемого файла интерпретатора или компилятора, запускает его и передает ему имя файла, хранящего начальное приближение. Результат из потоков вывода сохраняется в этот же файл если этот результат отличается от содержимого файла, после чего процесс повторяется. И так до стабилизации процесса, т.е. пока данный интерпретатор не будет выдавать тот же текст, который он получил на вход.

Эксперименты показывают, что таким способом неподвижная точки находится не всегда. И это не удивительно. Теорема о неподвижной точке может быть переформулирована в форме утверждения о том, что алгоритм преобразования программного кода не может всегда возвращать программу, отличную от данной. И если неподвижная точка существует, то итерирование применения этого алгоритма может породить последовательность программ, сходящуюся к неподвижной точке. Но последовательность может сойтись и к какому-нибудь циклу. Т.е. даже если $\text{[math]}$ , то возможно существует последовательность $\text{[math]}$ такая, что $\text{[math]}$ и $\text{[math]}$ . Причем, возможно, что $\text{[math]}$ .

Обсуждаемый скрипт [33] имеют рудиментарную поддержку определения таких циклов, но для меня остается открытым вопрос о возможности автоматического «преобразования» такого цикла в настоящую неподвижную точку (формально, в цикл из одного элемента).

(Несмотря на наблюдаемую эмпирическую сходимость итераций к неподвижной точке или к циклу, мне неизвестны какие-либо особые свойства функции $\text{[math]}$ , гарантирующие стабилизацию процесса после конечного количества шагов.)

Другие конструктивные теоремы о неподвижной точке

Пожалуй, это самый спекулятивный и неформальный подраздел этого сообщения. Здесь перечисляются некоторые известные теоремы о неподвижных точках, которые, возможно, могли бы быть применены для конструирования квайнов. Сама эта возможность находится под вопросом, но эти теоремы всё-же заслуживают упоминания в таком контексте.

Первая рекурсивная теорема Клини

(Этот раздел написан по мотивам соответствующего материала из [50].)

Для функций $\text{[math]}$ и $\text{[math]}$ , таких, что $\text{[math]}$ , $\text{[math]}$ и $\text{[math]}$ введем обозначение $\text{[math]}$ , читающееся как « $\text{[math]}$ продолжает $\text{[math]}$ ». (Другими словами, выполняется импликация $\text{[math]}$ .)

Функция называется конечной если она имеет конечную область определения. Конечной частью функции $\text{[math]}$ назовём конечную функцию $\text{[math]}$ . Сопоставим функции $\text{[math]}$ натуральное число $\text{[math]}$ .

Подразумевается, что существует алгоритм, который по числам $\text{[math]}$ и $\text{[math]}$ вычисляет $\text{[math]}$ если существует $\text{[math]}$ , такая, что $\text{[math]}$ и $\text{[math]}$ определена в точке $\text{[math]}$ .

Оператор $\text{[math]}$ называется рекурсивным оператором если существует вычислимая функция $\text{[math]}$ , такая, что $\text{[math]}$ тогда и только тогда, когда существует конечная $\text{[math]}$ , такая, что $\text{[math]}$ .

Оператор $\text{[math]}$ непрерывен если $\text{[math]}$ тогда и только тогда, когда существует конечная $\text{[math]}$ , такая, что $\text{[math]}$ .

Оператор $\text{[math]}$ называют монотонным, если $\text{[math]}$ .

Утверждение (без доказательства).

Рекурсивные операторы непрерывны и монотонны.

Теорема (без доказательства).

Для любого рекурсивного оператора $\text{[math]}$ существует неподвижная точка $\text{[math]}$ , т.е. $\text{[math]}$ . Причём $\text{[math]}$ – наименьшая из неподвижных точек, в том смысле, что если для какой-нибудь другой функции $\text{[math]}$ выполняется $\text{[math]}$ , то $\text{[math]}$ . (Всюду определенная функция $\text{[math]}$ автоматически будет единственной неподвижной точкой.)

Для демонстрации связи с квайнами в [50] (и это практически единственная обнаруженная мной в литературе зацепка, связывающая первую рекурсивную теорему с квайнами) по-сути предлагается попробовать в качестве рекурсивного оператора взять оператор, аналогичный оператору $\text{[math]}$ , определенному в разделе о теореме Роджерса (см. выше). Оператор $\text{[math]}$ преобразует программу $\text{[math]}$ в программу, печатающую текст $\text{[math]}$ , а по только что изложенной первой рекурсивной теореме Клини, рекурсивный оператор (с семантикой оператора $\text{[math]}$ ) должен иметь неподвижную точку $\text{[math]}$ и если из этого следует, что и сам оператор $\text{[math]}$ имеет неподвижную точку $\text{[math]}$ , такую, что $\text{[math]}$ , то, коль скоро программа $\text{[math]}$ равна программе, печатающей себя, $\text{[math]}$ есть квайн.

Здесь уместно прокомментировать согласованность этого вывода с данным выше определением рекурсивного оператора, ведь $\text{[math]}$ действует не на множестве вычислимых функций, а на множестве исходных текстов программ. Идея состоит в том, что оператор $\text{[math]}$ , преобразуя некоторую программу $\text{[math]}$ в программу $\text{[math]}$ , порождает рекурсивный оператор $\text{[math]}$ , преобразующий функцию $\text{[math]}$ в функцию $\text{[math]}$ . Обозначим $\text{[math]}$ , тогда вышеописанную идею можно проиллюстрировать следующей диаграммой:

$\text{[math]}$

К оператору $\text{[math]}$ напрямую применима первая рекурсивная теорема, т.е. существует $\text{[math]}$ , такая, что $\text{[math]}$ . Из этого следует, что существуют программы $\text{[math]}$ и $\text{[math]}$ , причем

$\text{[math]}$
Т.к., $\text{[math]}$ и $\text{[math]}$ , то
$\text{[math]}$
Подставляя (4) в (5) и применяя определение оператора $\text{[math]}$ получаем $\text{[math]}$ , т.е. $\text{[math]}$ удовлетворяет «уравнению квайна» $\text{[math]}$ и, соответственно, является квайном.

(Для меня остается открытым вопрос о возможности применения первой рекурсивной теоремы для автоматического конструирования квайнов, как в случае со второй рекурсивной теоремой.)

Теорема Клини о неподвижной точке [из теории решёток]

Произвольное отображение $\text{[math]}$ , непрерывное по Скотту и определенное на полном частично упорядоченном множестве $\text{[math]}$ с отношением порядка $\text{[math]}$ имеет наименьшую неподвижную точку.

Непрерывность по Скотту означает существование $\text{[math]}$ и выполнение $\text{[math]}$ для всякого направленного подмножества $\text{[math]}$ .

Теорема Кнастера-Тарского

В [37] приведена теорема о существовании неподвижных точек монотонных отображений на полной решетке. Пусть $\text{[math]}$ – монотонное отображение на полной решетке $\text{[math]}$ с отношением частичного порядка $\text{[math]}$ . Т.е. $\text{[math]}$ . Теорема Тарского утверждает, что $\text{[math]}$ , i.e. множество неподвижных точек отображения $\text{[math]}$ , само является непустой полной решеткой.

В [38] доказана конструктивная версия этой теоремы. До этой работы, неподвижные точки монотонных отображений уже конструировали как $\text{[math]}$ , где $\text{[math]}$ , а $\text{[math]}$ . Но это требовало от $\text{[math]}$ непрерывности по Скотту. В [38] же доказывается теорема, которая не требует от $\text{[math]}$ этого свойства и утверждая, что $\text{[math]}$ является полной решеткой относительно $\text{[math]}$ , предлагает, среди прочего, рецепт вычисления неподвижной точки в виде $\text{[math]}$ .

Здесь $\text{[math]}$ определяется как предел стационарной последовательности $\text{[math]}$ при $\text{[math]}$ . Считается, что $\text{[math]}$ для предельного ординала $\text{[math]}$ . Под стационарностью понимается, что начиная с некоторго индекса, элементы последовательности имеют одно и то же значение. Для корректного погружения в использованные в [38] трансфинитные определения необходимо чтение оригинальной статьи.

(Эти результаты обобщаются на случай полных частично упорядоченных множеств, только направленные, а не произвольные подмножества которых обязаны иметь супремум.)

Комбинатор неподвижной точки в лямбда-исчислении

В $\text{[math]}$ -исчислении [34] для реализации рекурсии используются комбинаторы неподвижной точки, в основном $\text{[math]}$ -комбинатор. Этот комбинатор определяется уравнением $\text{[math]}$ и в соответствии с этим определением вычисляет неподвижную точку функции $\text{[math]}$ , т.е. такое выражение $\text{[math]}$ , что $\text{[math]}$ .

Если конкретная реализация $\text{[math]}$ -исчисления поддерживает рекурсивные определения именованных символов, то вышеприведенного определения достаточно для работы с $\text{[math]}$ -комбинатором (могут возразить, что в таком случае он не особо-то и нужен; однако, здесь $\text{[math]}$ -комбинатор может служить полезной обёрткой для некоторых функций, позволяющей, к примеру, добавить временное хранение промежуточных результатов с целью исключения их повторного вычисления, — т.е., кэширование, — и, соответственно, получить ускорение в духе динамического программирования).

В чистом же $\text{[math]}$ -исчислении требуется определить $\text{[math]}$ -комбинатор в явном виде, например как $\text{[math]}$ (известный как комбинатор Карри или парадоксальный комбинатор) или, в случае использования императивного языка, задействовать [энергичный] комбинатор Тьюринга $\text{[math]}$ , где $\text{[math]}$ .

Теорема о неподвижной точке.

Несмотря на неочевидность этого утверждения, в нетипизированном $\text{[math]}$ -исчислении любое выражение имеет неподвижную точку (хотя бы одну).

Доказательство.

Пусть $\text{[math]}$ . Комбинатор Тьюринга есть $\text{[math]}$ . Утверждается, что для любого $\text{[math]}$ -выражения $\text{[math]}$ , выражение $\text{[math]}$ есть его неподвижная точка. Чтобы увидеть это, запишем следующую цепочку уравнений:

$\text{[math]}$

где $\text{[math]}$ обозначает последовательность из нуля или нескольких шагов $\text{[math]}$ -редукции. $\text{[math]}$

Теперь $\text{[math]}$ -комбинатор может быть применен для вычисления значений функций, вызывающих сами себя, в среде, не имеющей возможности выполнять именованный рекурсивный вызов или вообще не поддерживающей именование объектов.

Например, если требуется вычислить функцию $\text{[math]}$ , вызывающую саму себя по имени $\text{[math]}$ , то можно определить новую функцию $\text{[math]}$ , принимающую $\text{[math]}$ как аргумент: $\text{[math]}$ (а при использовании индексов де Брёйна или бинарного лямбда-исчисления мы можем избавиться и от именованных переменных вовсе). После определения $\text{[math]}$ мы можем вычислить $\text{[math]}$ как $\text{[math]}$ , потому что $\text{[math]}$ есть неподвижная точка $\text{[math]}$ , т.е., $\text{[math]}$ , а $\text{[math]}$ , как было сказано выше, как раз и находит такую неподвижную точку. Желающие могут непосредственной подстановкой убедиться, что в этом случае действительно выполняется $\text{[math]}$ .

Учитывая универсальность $\text{[math]}$ -исчисления и вышеприведенную теорему о неподвижной точке [в $\text{[math]}$ -исчислении], естественно возникает идея об использовании комбинатора неподвижной точки для конструирования квайнов. (См. также [2, 47].)

(Утверждение о существовании комбинатора неподвижной точки практически эквивалентно вышеприведенный первой рекурсивной теореме Клини, но выглядит более конкретным.)

Логическое программирование в ограничениях

В [12, 49] приводится интересный метод генерации квайнов с использованием логического программирования. Авторы использовали язык логического программирования miniKanren [52], позволяющий написать на нём аналог «основного уравнения квайнов» $\text{[math]}$ и дать системе решить его относительно $\text{[math]}$

С использованием реализации miniKanren, выполненной на языке scheme, квайны можно генерировать примерно так (q.scm взят из [49]):

(load "q.scm")
(run 1 (q) (eval-expo q '() q)))

Квайны вычисляются быстро (за секунду) и имеют малые размеры.

(Существует множество реализаций miniKanren и на других языках, e.g., на ECMAScript/JavaScript, Python, Ruby, etc.)

Эволюционные алгоритмы

Крайне интересной представляется потенциальная возможность генерации квайнов с помощью генетических алгоритмов. Среди многих проблем, возникающих при генерации программ эволюционными методами, выделяется проблема сохранения допустимости или синтаксической «корректности» программ при действии генетических операторов (кроссовер, мутация).

В этом смысле, одним из наиболее пригодных представлений для инкрементной эволюционной генерации, являются искусственные нейронные сети (далее ИНС или нейросети). Будучи сетями однотипных нелинейных сумматоров, работа которых зависит от весов связей (синапсов) между ними, нейросети продолжают сохранять работоспособность даже при почти случайных изменениях/«повреждениях» в матрице их весовых коэффициентов. Это довольно сильно контрастирует с традиционными языками программирования, программы на которых с гораздо большей вероятностью подвержены выходу из строя при малейших необдуманных модификациях их исходного текста.

Квайны в виде нейросетей уже известны. В [41] описана ИНС, обучающаяся выводить значения своих же синаптических коэффициентов. Я же хотел бы здесь сосредоточится на другом способе генерации квайнов, а именно на конструировании программ посредством применения генетических алгоритмов к промежуточному представлению на основе нейросетей.

Есть интересный экспериментальный язык Anne, [40], придуманный специально для работы с нейросетями и транслятор neuralbf [16, 51] того же автора, преобразующий программу на bf в описание рекуррентной ИНС. Последняя работа (кому-то могущая показаться несерьёзной) фокусируется на применении генетических алгоритмов для совершенствования и исправления уже написанных вручную программ (вместо их генерации без начального приближения).

Цепные квайны

Назовём цепным квайном (или итеративным квайном) с периодом $\text{[math]}$ , последовательность $\text{[math]}$ программ $\text{[math]}$ , такую, что $\text{[math]}$ и $\text{[math]}$ .

Можно получить интересное обобщение — многоязыковой или «релейный» квайн — если заменить в только-что данном определении скобки $\text{[math]}$ на $\text{[math]}$ , где $\text{[math]}$ – возможно различные языки программирования (подразумевается $\text{[math]}$ ).

Теорема (без доказательства).

Цепные квайны существуют для любого периода $\text{[math]}$ .

Всякий, кто пытался писать квайны и цепные квайны, не мог не отметить некоторое отличие в сложности их написания – цепные квайны [при $\text{[math]}$ ] обычно проще истинных квайнов (i.e., тоже цепных квайнов, но с периодом $\text{[math]}$ ).

Соответственно, не может не возникнуть вопрос о реализуемости полностью автоматического преобразования данной последовательности $\text{[math]}$ в настоящий квайн $\text{[math]}$ .

Генератор квайнов, не зависимый от языка

В разделе о конструировании квайнов на основе второй рекурсивной теоремы Клини, приводился готовый рецепт, алгоритм генерации квайна для конкретного заранее выбранного языка программирования. (Похожий алгоритм возможен и в контексте доказательства теоремы Роджерса.) Возможно, что слово «алгоритм» здесь можно понимать более формально и буквально.

Представляется интересным вопрос о существовании программы $\text{[math]}$ , — «квайнтификатора», — генерирующей квайн на указанном языке $\text{[math]}$ с использованием некоторого количества образцов кода на этом языке. Причем и разумной спецификацией языка $\text{[math]}$ и одновременно образцом кода на нём может служить интерпретатор языка $\text{[math]}$ (существующий по теореме об универсальной функции).

Чуть более формально задача может быть поставлена так. Пусть дан интерпретатор $\text{[math]}$ языка $\text{[math]}$ , написанный на своем же входном языке, т.е. для любой программы $\text{[math]}$ на языка $\text{[math]}$ выполняется $\text{[math]}$ . Пусть также $\text{[math]}$ оттранслирован на референсный язык (семантические скобки без индекса) и существует на нём в виде программы $\text{[math]}$ . В этом случае справедливо $\text{[math]}$ .

Спрашивается, как может выглядеть программа $\text{[math]}$ , такая, что $\text{[math]}$ и $\text{[math]}$ ? Выше мы видели, что $\text{[math]}$ есть неподвижная точка (по Роджерсу) оператора $\text{[math]}$ . При попытке реализовать $\text{[math]}$ выясняется, что структура соответствующей программы сильно схожа со структурой интерпретатора. Возможно, это сходство можно использовать для написания $\text{[math]}$ … Но это требует дальнейшего обдумывания.

Вместо самоинтерпретаторов можно использовать обычно более простые программы, — специализаторы, — реализующие $\text{[math]}$ -функцию, ведь именно она является главным ингредиентом (после диагонализации, конечно) в доказательстве теоремы Клини о рекурсии. (В следующих сообщениях этот вопрос, возможно, будет исследован более подробно.)

Заключение

Целью этого сообщения была демонстрация возможности автоматического конструирования квайнов на языке редактора sed с использованием доказательства второй рекурсивной теоремы Клини в качестве основы. Результат проведенного эксперимента можно считать положительным, хотя автоматическим такой способ написания квайнов можно назвать только в смысле достаточности запуска единственного скрипта generate.sh и ликвидации наиболее сложной, и, если можно так выразиться, творческой составляющей в конструировании самореплицирующейся системы.

В целом, сообщение уже немного вышло за рамки очерченных целей. Но о квайнах можно сказать больше… В следующих сообщениях этой серии.

Ссылки

[1] http://www.madore.org/~david/computers/quine.html
[2] http://math.berkeley.edu/~kmill/blog/blog_2018_5_31_universality_quines.html
[3] http://en.wikipedia.org/wiki/Smn_theorem
[4] http://en.wikipedia.org/wiki/partial_evaluation
[5] http://fi.ftmr.info
[6] http://ru.wikipedia.org/wiki/диагональный_аргумент
[7] http://ru.wikipedia.org/wiki/теорема_Кантора
[8] http://ru.wikipedia.org/wiki/проблема_остановки
[9] http://ru.wikipedia.org/wiki/автомат_фон_Неймана
[10] http://ru.wikipedia.org/wiki/зонд_фон_Неймана
[11] Jiazhen Cai, Robert Paige, Program derivation by fixed point computation, 1989
[12] William E.Byrd, Eric Holk, Daniel P.Friedman, miniKanren, live and untagged: Quine generation via relational interpreters, 2012
[14] S.C.Kleene, Introduction to Meta-Mathematics, 1952
[15] http://en.wikipedia.org/wiki/Quine%27s_paradox
[16] http://www.domob.eu/projects/neuralbf.php
[17] https://github.com/MakeNowJust/quine/blob/master/quine.sed
[18] https://github.com/MakeNowJust/quine
[19] H.Rogers, Theory of Recursive Functions and Effective Computability
[20] T.A.Hansen, T.Nikolajsen, J.L.Traff, N.D.Jones, Experiments with Implementation of two Theoretical Constructions
[21] G.Bonfante, M.Kaczmarek, J-Y.Marion, Toward an Abstract Computer Virology
[22] G.Bonfante, M.Kaczmarek, J-Y.Marion, A Classification of Viruses through Recursion Theorems, 2007
[23] Julia L. Lawall, Olivier Danvy, Continuation-Based Partial Evaluation
[24] Anders Bondorf, Improving Binding Times Without Explicit CPS-Conversion
[25] D.A.Wheeler, Fully Countering Trusting Trust through Diverse Double-Compiling, 2009
[26] Douglas R.Hofstadter, Goedel, Escher, Bach: an Eternal Golden Braid, 1979
[27] P.-M. Binder, Theories of almost everything, 2008
[28] H.G.Rice, Classes of recursively enumerable sets and their decision problems, 1953
[29] https://en.wikipedia.org/wiki/Rice_theorem
[30] Gary P.Thompson II, The quine page (self-reproducing code), http://www.nyx.net/~gthompso/quine.htm
[31] http://www.nyx.net/~gthompso/self_kim.txt
[32] http://www.latrobe.edu.au/phimvt/joy
[33] https://gist.github.com/Circiter/7152686
[34] http://en.wikipedia.org/wiki/lambda_calculus
[35] Lawrence S.Moss, Recursion Theorems and Self-Replication Via Text Register Machine Programs
[36] Neil Jones, Computer implementation and application of Kleene’s s-m-n and recursion theorem.
[37] A.Tarski, A lattice theoretical fixpoint theorem and its applications, 1955
[38] P.Cousot, R.Cousot, Constructive versions of Tarski’s fixed point theorems, 1979
[39] J.Case, S.E.Moelius III, Program Self-Reference in Constructive Scott Subdomains, 2009
[40] http://compann.sourceforge.net
[41] O.Chang, H.Lipson, Neural Network Quine, 2018
[42] http://en.wikipedia.org/wiki/quine
[43] F.William Lawvere, Diagonal arguments and cartesian closed categories, 1969
[44] Noson S.Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, 2003
[45] Jean-Yves Marion, From Turing machines to computer viruses, 2012
[46] https://github.com/Circiter/quine-kleene-generator
[47] Kleene Second Recursion Theorem: A Functional Pearl // Proc. ACM Program. Lang., Vol 1, 2018
[48] Дж. фон Нейман, Теория самовоспроизводящихся автоматов, 1971
[49] https://github.com/webyrd/quines
[50] В.М.Зюзьков, Теория алгоритмов: Учебное пособие, 2005
[51] https://gitlab.com/domob/neuralbf
[52] https://github.com/miniKanren
[53] http://www.michaelwehar.com/quines
[54] http://www.keithschwarz.com/kleene
[55] http://www.nyx.net/~gthompso/quine-1.1.0.tar.gz
[56] J.C.Owings младший, Diagonalization and the Recursion Theorem, 1973
[57] E.Alonso, M.Manzano, Diagonalization and Church’s Thesis: Kleene’s Homework, 2005

М.И.Никитин
г.Алматы, июль, 2020
(последняя правка: ноябрь, 2020)

Зани­ма­тель­ное квай­но­вод­ство. Часть I.

Содер­жа­ние:

Вве­де­ние в квай­но­ло­гию

Искус­ство versus ремесло

Эффек­тив­ность и выбор назва­ния серии сооб­ще­ний.

Поста­новка задачи

Ввод­ные заме­ча­ния

Тео­рема об уни­вер­саль­ной функ­ции

S-m-n тео­рема Клини

Непо­движ­ные точки вычис­ли­мых функ­ций

Глав­ный экс­пе­ри­мент

Про­ме­жу­точ­ные итоги

Допол­ни­тель­ная тео­рия

Про­блема оста­новки

Диа­го­на­ли­за­ция

Тео­рема Кан­тора

Тео­рема Ловера

Связь диа­го­на­ли­за­ции с тео­ре­мами о непо­движ­ной точке

Вер­сия «от про­тив­но­го».

Немного о пре­де­лах позна­ва­е­мо­сти

Дру­гие под­ходы и «слегка откры­тые» вопросы

«Кре­а­ци­а­низм» vs. «абио­ге­нез»

Кими­ан­ские квайны и ите­ра­тив­ное вычис­ле­ние непо­движ­ной точки

Дру­гие кон­струк­тив­ные тео­ремы о непо­движ­ной точке

Пер­вая рекур­сив­ная тео­рема Клини

Тео­рема Клини о непо­движ­ной точке [из тео­рии решёток]

Тео­рема Кнастера-Тарского

Ком­би­на­тор непо­движ­ной точки в лямбда-исчислении

Логи­че­ское про­грам­ми­ро­ва­ние в огра­ни­че­ниях

Эво­лю­ци­он­ные алго­ритмы

Цеп­ные квайны

Гене­ра­тор квай­нов, не зави­си­мый от языка

Заклю­че­ние

Ссылки

Занимательное квайноводство. Часть I.

Содержание:

Введение в квайнологию

Искусство versus ремесло

Эффективность и выбор названия серии сообщений.

Постановка задачи

Вводные замечания

Теорема об универсальной функции

S-m-n теорема Клини

Неподвижные точки вычислимых функций

Главный эксперимент

Промежуточные итоги

Дополнительная теория

Проблема остановки

Диагонализация

Теорема Кантора

Теорема Ловера

Связь диагонализации с теоремами о неподвижной точке

Версия «от противного».

Немного о пределах познаваемости

Другие подходы и «слегка открытые» вопросы

«Креацианизм» vs. «абиогенез»

Кимианские квайны и итеративное вычисление неподвижной точки

Другие конструктивные теоремы о неподвижной точке

Первая рекурсивная теорема Клини

Теорема Клини о неподвижной точке [из теории решёток]

Теорема Кнастера-Тарского

Комбинатор неподвижной точки в лямбда-исчислении

Логическое программирование в ограничениях

Эволюционные алгоритмы

Цепные квайны

Генератор квайнов, не зависимый от языка

Заключение