Игошин Математическая логика и теория алгоритмов (1019110), страница 97
Текст из файла (страница 97)
Один из фундаментальных законов классической логики — закон исключенного третьего Р м — Р в неко торой свободной трактовке фактически означает, что мы знаем все. Этот постулат конечно же никак нельзя назвать реалистичес ким: мы знаем чрезвычайно мало, и чем больше узнаем, тем лучше это понимаем. Голландский математик Л.Э.Я. Брауэр определил логические корни «привидений» еще до открытия теоремы Геделя, в 1908 г., и начал построение так называемой интуиционистской математики, не принимающей закон Р и — Р как универсальный. В 1930 — 1932 гг.
другой голландец А. Гейтинг строго сформулировал логику, которой пользовались в интуиционистской математике, — интуиционистскую логику. Ее математическая интерпретация, данная советским математиком А, Н. Колмогоровым в то же время, сохранила свое значение до сих пор. А. Н. Колмогоров рассмотрел логику как исчисление задач. Каждая формула алгебры высказываний рассматривается не просто как формула, но как требование решить задачу, т.е. построить объект, удовлетворяющий некоторым условиям. Это так называемая конструктивная интерпретация логики высказываний. Логические связки понимаются как средства построения формулировок более сложных задач из более простых, аксиомы — как задачи, решения которых даны, правила вывода — как способы преобразования решений одних задач в решения других.
Отметим, что решение задачи — это не только сам искомый объект, но и доказательство того, что он удовлетворяет предъявляемым требованиям. Например, формула А л В понимается в колмогоровской интерпретации как задача, состоящая в том, чтобы построить и решение задачи А, и решение задачи В, правило вывода А, В/ А л В— как преобразование, строящее из объекта а, решающего задачу А, и объекта Ь, решающего задачу В, пару (а, Ь), решающую задачу А л В. Объект а, решающий задачу, сопоставленную формуле А, называется реализацией А.
Этот факт обозначается аАА. Центральным моментом конструктивного понимания логических формул является интерпретация импликации. Конструктивная импликация А =~ В понимается как требование построить эффективное преобразование~ применимое ко всем реализациям формулы А и переводящее их в реализации формулы В. Нечеткая колмогоровская формулировка логики как исчисления задач породила многочисленные различные конкретизации, дав целую систему точных математических определений. Эта формулировка нашла применение не только в интуиционистской логике, для которой она была создана, но и в других логических системах.
Строгие математические семантики, основанные на идее Колмогорова, обычно называют семантиками реализуемости (в отличие от других видов логических семантик, которые базируют- 390 ся на системах истинностных значений). Первую реализуемость построил американский логик С. К. Клини в 1940 г. для арифметики с интуиционистской логикой. В 1960 — 1980-х гг. появились десятки понятий реализуемости как для систем, базирующихся на интуиционистской логике, так и для других логик. Советский логик А.А. Воронков в 1985 г.
вывел условия, при которых классическая логика может рассматриваться как конструктивная. Из них, в частности, следует, что необходимым (но не достаточным) условием конструктивности классической теории является ее полнота, т. е. выводимость в ней для каждой замкнутой формулы Глибо самой Г„либо ее отрицания Е (Тем самым еще раз подтвердилось прозрение Брауэра относительно логических корней неконструктивности.) Заметим, что примерами классических теорий, имеющих конструктивное истолкование, служат элементарная геометрия и алгебраическая теория вещественных чисел.
Описание программирования с помощью логики основано на определенной аналогии между выводом формулы в некотором логическом исчислении и программой решения задачи, отвечающей этой формуле при конструктивной интерпретации логики. Логическая теория, соответствующая структурным схемам программ, появилась в середине 1980-х гг.
Структурные схемы соответствовали нарождающемуся новому типу логики — логики схем программ, которой пользуется программист для создания сложных, многовариантных, итеративных планов действий. Имеется корректная и полная система конструктивных правил вывода (логика й,), позволяющих при помощи некоторой структурной схемы построить доказательство возможности преобразовать А в В на базе заданных функций, преобразующих некоторые А; в В;: А~В,С~Р— правило условного оператора (ПУО); А гС=ьВ~~Р А — > В, В ~ С, С -ь Р— правило релаксации (ПР); А =ь Р А ~ С =ь В~С вЂ” правило зацикливания(ПЗ); А =ь В А~А — правило бесконечного цикла (ПБЦ); -А ~А — правило ошибки(ПО). А~А 391 Все перечисленные правила имеют конструктивное истолкование.
Для ПУО и ПЗ оно видно из их названий. В ПУО А и В— охраны создаваемого условного оператора, в ПЗ С вЂ” инвариант создаваемого цикла,  — условие его завершения. ПР не преобразует, оно лишь говорит о том, что то же г" можно использовать и в более частной ситуации, чем А =» В. ПБЦ утверждает, что застой не может быть вечен. ПО постулирует существование нигде не определенной функции «оишбка». Таким образом, конструктивное описание ситуации, где классические средства работают плохо, оказалось весьма компактным и эффективным. Логика й, — лишь одна из простейших л4згик схем программ, успешно используемых в автоматизированном планировании действий. Интуиционистская логика из конструктивных логик с точки зрения синтаксиса оказалась наиболее близкой к традиционнойлогике.
Она полностью сохранила язык исчисления предикатов и логические связки классической логики (вложив в них свой, конструктивный, смысл).:Она по возможности сохранила и правила классической логики постольку, поскольку они не влекут закона исключенного третьего Р ч —,Р (принципа всезнания в конструктивной интерпретации) или закона двойного отрицания Р ~ Р. Этот закон, как выяснил Брауэр, влечет принцип всезнания„а сам конструктивно может быть истолкован как существование Общего Решателя Задач (такой же нонсенс, как вечный двигатель).
Задача построения программы выражается в интуиционистской логике с помощью функциональной формулы: ('с'х)[А, л...лА„» (Зу)(В, л...л Вг)]. Здесь х — входные переменные создаваемой программы; у — ее результаты; В; задают связи вход-выход; А; амбивалентны: они могут представлять как условия на входы, так и входные значения сложных типов (структуры данных, функции-параметры). Например, формула (~ух)[х> О ~ (Зу)(у > О л у' = х)] интерпретируется как задача построения программы вычисления квадратного корня из х, а формула (Чх„у) [х < у л (Чг)(х < г л г < у =» (3 и)(М(г, и))) =» (Зо)( гг, и)(х < < г л г < у л М(г, и) ~ и < о)] может трактоваться как задача построения оператора, ставящего в соответствие функции, определенной на [х, у] и перерабатывающей г в и, ее верхнюю границу.
Из-за отсутствия принципа всезнания выразительные возможности интуиционистской логики существенно повышаются по сравне- 392 нию с классической. На ее языке можно постулировать не только знание, но порой и незнание. Например, то, что значение действительного числа не может быть задано точно, постулируется в форме — (1ух, у)(х > у ~ у > х ч х = у). Но повышение выразительной силы и «аккуратности» выводов в интуиционистской логике по сравнению с классической имеет и оборотную сторону: поиск вывода в ней существенно сложнее. В частности, метод резолюций (см.
5 39) в ней неприменим, потому что формулы не могут быть разложены на дизъюнкты. Интуиционистская логика хорошо подходит для описания задач, в которых требуется вычислить новые величины по заданным величинам и ни один из вычислительных ресурсов (время, память, надежность) не налагает ограничений. Для других ситуаций интуиционистскую логику приходится варьировать. Впервые на возможности логики в качестве инструмента анализа понятий программирования обратили внимание в середине 1970-х гг.
в связи с развитием теории верификации (проверки правильности) программ. Оказалось, что для многих конструкций программирования, совместное использование которых не приводит к алгоритмической невычислимости, невозможно построить полную формальную систему, описывающую их взаимодействие. Например, рассмотрение логики схем программ позволило установить, что операторы ОО ТО естественно получаются в том случае, если все рассматриваемые действия можно считать глобальными преобразованиями состояния системы. Циклы оказались хорошо совместимы с массивами и плохо — с рекурсивными структурами данных, а процедуры высших типов — наоборот.
Массивы и сложные структуры данных плохо совместимы с присваиваниями (в данном случае присваивание дается на целый ряд операторов, несущих различный логический смысл).' В общем, можно сделать вывод, что нет средств программирования хороших либо плохих самих по себе; хороши или плохи их комбинации. При этом любая логически разумная комбинация оказывается неуниверсальной, она приспособлена лишь для определенного класса задач. Верификация (доказательство правильности) программ с помощью математической логики.
Широчайшее использование компьютеров в самых разнообразных сферах человеческой деятельности выдвигает на одно из первых мест волрос о надежности программ- лого обеспечения компьютеров. Как известно, правильность созданной программы обычно проверяется на ряде так называемых тестовых примеров, на начальных данных, для которых результат известен или его можно предсказать. Нетрудно понять, что такая проверка способна лишь выявить наличие ошибок в программе, но не доказать их отсутствие, что, разумеется, не одно и то же. 393 Поэтому исключительно важна задача строгого доказательства правильности программ, и именно для этой цели и начали разрабатываться программные и динамические логики. С интуиционистской точки зрения программа будет правильной, если в результате ее выполнения будет достигнуг тот результат, с целью получения которого и была написана программа, (Обратите внимание, что мы не рассматриваем программы, содержащие синтаксические ошибки, т.е.
предполагаем, что с точки зрения языка программирования программа написана безупречно.) Доказательство правильности программы состоит в предъявлении такой цепочки аргументов, которые убедительно свидетельствуют о том, что это действительно так, т.е. что программа на самом деле решает поставленную задачу. Сформулируем теперь точное определение понятия правильности программы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
