Системный трюк: ещё одно доказательство

 

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

 

10 LIST

 

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

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

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

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

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

 

GetProgramText (var s: string)

 

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

 

ExecuteProgram(s: string)

 

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

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

 

function Compute_h (x: string): string; begin

end;

 

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

 

program fixed_point; var s: string;

function Compute_h (x:string): string; begin

end; begin

GetProgramText (s);

s:= Compute_h (s);

ExecuteProgram (s); end.

 

Выполнение этой программы сразу же сводится к выполнению программы, получающейся применением к ней функции А, так что она будет неподвижной точкой по построению.

Мы только что объяснили, как с помощью языка с дополнительной процедурой «получить текст программы» можно доказать теорему о неподвижной точке. Но можно рассуждать и в обратном направлении и объяснить, почему применение теоремы о неподвижной точке заменяет такую дополнительную процедуру.

В самом деле, пусть мы имеем программу р, в которой есть строка GetProgramText (s). Заменим эту строку на оператор присваивания s: = t, где t — некоторая строковая константа. Получится новая программа, зависящая от t. Назовём её p(t). Согласно теореме о неподвижной точке, существует такое значение t, при котором программы t и p{t) эквивалентны. При этом t выполнение программы t эквивалентно выполнению её текста, в котором в момент вызова процедуры GetProgramText(s) в строку s помещается текст программы t — чего мы и хотели.

Теперь становится понятнее, почему теорема о неподвижной точке называется ещё теоремой о рекурсии. В самом деле, рекурсия состоит в том, что мы вызываем программу изнутри её самой. Здесь происходит даже больше: мы не только имеем право вызвать программу, но и можем получить доступ к её тексту! Обычный вызов действительно является частным случаем доступа к тексту, так как мы можем вызвать процедуру интерпретации на этом тексте. (Конечно, при этом нам понадобится включить в состав программы текст интерпретатора нашего языка программирования, записанный на этом языке.)

 

Несколько замечаний