Проблема машинного доказательства математических теорем
Перейдем к следующей актуальной проблеме философии информатики, а именно проблеме машинного доказательства математических теорем.
Для информатики эта проблема имеет практический характер: можно ли запрограммировать машину таким образом, чтобы та самостоятельно создавала для себя другие программы. Например, в комнате стоят стопки кубиков, помеченных буквами А, Б, В. Причем кубик А стоит на кубике В. Есть робот, который умеет брать кубики в манипулятор и ставить их на пол или на другие кубики. Наша задача – получить башенку вида "А на Б на В". Конечно, можно составить программу вида: "Снять кубик А, поставить Б на В, поставить А на Б". Но задача не в этом. Задача в том, чтобы создать для робота программу, для которой в качестве входных данных давался бы только конечный результат – башенка определенного вида, но не непосредственная последовательность действий, и эта программа самостоятельно создала бы подпрограмму "как достичь цели, исходя из текущего положения кубиков". В более широком смысле эта задача рассматривается в русле оценки возможности построения "искусственного интеллекта", которая в философии наиболее остро обсуждается во второй половине XX в.
Для решения этой задачи необходимо заложить в работу робота какие-то принципы математической логики. Наиболее подходящее средство предоставляет ее конструктивное направление[1], поскольку ОГЛАВЛЕНИЕ теорем конструктивизм рассматривает не относительно того, что существует, а относительно того, что может быть сделано[2]. С точки зрения прикладной компьютерной науки, смыслом обладает то, что можно эксплицитно определить или запрограммировать.
Представление чисел, функций (операций), множеств в виде конструктивных объектов требует определения отношений между ними на уровне спецификации языка программирования. Традиционно это определение осуществляется благодаря типизации используемых объектов. Понятия "тип", "класс" и "объект" являются настолько привлекательными для моделирования, что их применяют в информатике повсеместно. Однако дискуссии о том, насколько корректно и насколько "естественно" описание реальности посредством типов, актуальны и на сегодняшний день.
Перейдем теперь к философской проблематике, обусловленной развитием упомянутых конструктивных форм.
В рамках проблемы машинного доказательства математических теорем особую важность представляет верификация проводимых вычислений. Например, возможно создать программу, которая будет искать доказательство утверждения исходя из заданных аксиом. И это доказательство будет верным, если сама программа написана корректно. Проблема в том, что корректность программы – сама по себе требует доказательства. Корректность этого доказательства тоже можно пробовать доказать программой... и так далее до бесконечности.
Возникает резонный вопрос: можно ли считать доказанным утверждение, доказательство которого существенно опирается на машинные вычисления? Ответ на этот вопрос зависит от определения онтологического статуса компьютерной программы или созданного конструкта. Например, признавая или не признавая компьютерную программу материальным объектом, мы можем принимать или отрицать "машинные" доказательства математических теорем[3].
В связи с вопросами моделирования также возникает вопрос о корректности применения математического моделирования в тех доказательствах, в которых доказательство корректности модели также было бы невычислимым. Некоторое подобие ответа можно сформулировать следующим образом. Модель не должна быть с необходимостью верной в неформальной интерпретации. Например, если мы моделируем поведение биологического объекта, то оказывается совершенно не важно, что модель (робот) совершенно не изоморфна самому объекту. То есть, если нам важен только один аспект поведения моделируемого объекта, например то, как пчела находит свой улей, то моделировать всю пчелу и не нужно.
Остановившись на проблемах и успехах в конструктивистской части информатики, перейдем к проблемам другой ее части – аналитической.