Теорема о неполноте компиляторов

lex_kravetski — 12.07.2022 Компилятор достаточно полного языка программирования мы всегда можем вызвать программно. Ну, поскольку такой язык должен позволять вызовы чего-то там в ОС — по меньшей мере, запуск других программ.

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

Если в стандартной библиотеке такого класса ещё нет, создадим специальный класс Try. Который создаёт блок перехвата ошибок, аналогичный try-catch, и запускает внутри него переданную ему функцию. Если ошибка не возникла, то Try возвращает Success(result) (где result — то, что вернула функция), а если возникла, то Failure(error).

Вообще говоря, это всё нужно только для краткости записи — с любой системой обработки ошибок можно было бы сделать то же самое, только строк понадобилось бы больше.

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

Теперь рассмотрим вот такую программу.

val badString = “Try(compile(badString)).getClass == Failure.class”
compile(badString)

Если компилятор из второй строки успешно скомпилирует содержимое badString, то класс результата компиляции не может быть Failure. А значит в badString написано ошибочное утверждение. Однако компилятор ведь его скомпилировал без ошибки.

Если же компилятор выдаст ошибку компиляции, то утверждение в badString было верным. Это значит, что компилятор не смог скомпилировать корректное выражение.

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

Ну или хотя бы надо завязывать с компиляторами.

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

Но чистым математикам — норм. Даже когда они так рассуждают о том, что, по сути, является программированием, а не «чистой математикой». Ну, как в теореме Гёделя.

«Не-не, пацаны», — скажет вам чистый математик, — «быть может, у вас там это всё и похоже на бред сумасшедшего, но в нашей вселенной, когда вот так — всё зашибись. Даже когда речь заходит о чём-то из вашей вселенной. Поэтому мы из нашей вселенной рекомендуем в вашу прекратить это бесполезное занятие — написание компиляторов и вообще софта. Ну, как Гёдель в своё время порекомедовал завязывать с системами автоматического поиска доказательств».

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

В badString лежит строка. Эта строка ссылается сама на себя, поэтому при попытке скомпилировать это всё в лоб — подстановкой строки в эту же строку — получится бесконечная рекурсия, что в перспективе даёт ошибку переполнения стэка. Она, конечно, в общем случае не означает некорректности программы, но в этом-то точно означает: тут последовательность преобразований точно никогда не закончится, что можно отследить по тому, что на следующей итерации результат преобразования внутри себя содержит фрагмент, полностью идентичный результату предыдущей итерации, а условия выхода не написано. По этой причине переполнение стэка на шаге больше первого действительно свидетельствует о том, что мы имеем дело с бесконечной рекурсией, а не об ошибке в компиляторе.

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

В обоих этих случаях результатом будет Failure.

Если же язык трактует такого рода конструкции, как «ленивые» — то есть на этапе компиляции на место «badString» не будет подставляться её текущее содержимое, а так останется само имя переменой «badString», то результатом второй строки будет Success. И compile в первой строке тоже даст его же.

Но как же, Success.getClass ведь не равен Failure.class?!

Ну так и что с того? Да, в badString, лежит выражение, дающее результат false, если его скомпилировать и вычислить. Однако сие ничего не говорит о «ложности компилятора». И о неправильности компилятора оно тоже ничего не говорит. Оно говорит только о том, что, если вы считаете «badString» каким-то там «мощным предсказанием», которое истинно или ложно по результатам работы второй строки, то с ним явно что-то не так.

Компилятор в порядке — это вашему «предсказанию» трындец.

Что, вообще говоря, не редкость при использовании логики высших порядков — то есть, такой логики, которая «рефлексирует» над логикой же.

Компилятор в качестве результата выдаёт Success и Failure, с чего вы вообще взяли, что true и false для какого-то выражения, зависящего от результата компиляции, обязан быть в трактовках полностью идентичным Success и Failure? Или что он таковым вообще может быть?

Хотя, постойте, мы ж — математики. Поэтому давайте переименуем «Success» и «Failure» в «true» и «false». Ведь если оно одинаково называется, то оно — идентично. Шах и мат, программисты!



doc-файл

Оставить комментарий

Популярные посты:

• Ранее
• Архив