Теорема о неполноте компиляторов
Компилятор достаточно полного языка программирования мы всегда можем вызвать программно. Ну, поскольку такой язык должен позволять вызовы чего-то там в ОС - по меньшей мере, запуск других программ.
Кроме того, хороший и правильный компилятор не должен компилировать ошибочный код, а должен вместо этого выдавать ошибку компиляции. Тогда как правильный код он, напротив, всегда должен компилировать.
Если в стандартной библиотеке такого класса ещё нет, создадим специальный класс 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-файл
Кроме того, хороший и правильный компилятор не должен компилировать ошибочный код, а должен вместо этого выдавать ошибку компиляции. Тогда как правильный код он, напротив, всегда должен компилировать.
Если в стандартной библиотеке такого класса ещё нет, создадим специальный класс 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-файл