Роль логического программирования, и стоит ли планировать его изучение на 2021-й
Логи́ческое программи́рование — парадигма программирования, основанная на автоматическом доказательстве теорем, а также раздел дискретной математики, изучающий принципы логического вывода информации на основе заданных фактов и правил вывода. Логическое программирование основано на теории и аппарате математической логики с использованием математических принципов резолюций.
Итак, пришло время второй ссылки. Что это будет? Статья на Хабре? Может быть статья на ином ресурсе? Прочитав пару первых абзацев на разных сайтах, вы, скорее всего, мало что поймете, так как, во-первых, материал обычно ориентирован на знающего читателя, во-вторых, хорошей и понятной информации по теме не так много в русскоязычном интернете, в-третьих, там почему-то постоянно речь идёт о некоем «прологе» (речь о языке программирования Prolog, разумеется), но сам язык, кажется, использует мало кто (почётное 35 место в рейтинге TIOBE). Однако наш герой не теряет мотивации и, спустя некоторое время, натыкается на эту самую статью, желая, все-таки понять:
Что такое логическое программирование
Какова история его создания и фундаментальные основы (серьезно, какому новичку это может быть интересно?)
Зачем и где его применяют
Стоит ли лично вам его изучать
Что ж, постараюсь ответить просто и понятно, обходя страшные термины и не вспоминая исторических личностей.
Что такое логическое программирование
В школе на уроках информатики многие, если не все, слышали про Pascal (а кто-то даже писал на нем). Многие также могли слышать про Python, C/C++/C#, Java. Обычно программирование начинают изучать именно с языков из этого набора, поэтому все привыкли, что программа выглядит как-то так:
Этот яркий, но малоинформативный пример призван показать, что обычно команды выполняются одна за другой, причем мы ожидаем, что следующие инструкции (команды) могут использовать результат работы предыдущих. Также мы можем описывать собственные команды, код которых будет написан подобным образом. Остановимся на том, что как завещал Фон Нейман, так компьютер и работает. Машина глупа, она делает то, что скажет программист, по четкому алгоритму, последовательно выполняя инструкции. Не может же, в конце концов, компьютер, подобно мыслящему живому существу, делать выводы, строить ассоциативные ряды… Или может?
Давайте устроимся поудобнее рядом со своим компьютером и порассуждаем о жизни и смерти вместе с Аристотелем:
Следовательно, Сократ смертен.
Звучит логично. Но есть ли способ научить компьютер делать выводы как Аристотель? Конечно! И вот тут мы вспомним о Prolog-e, который так часто мелькает при поиске информации о логическом программировании. Как несложно догадаться, Prolog (Пролог) является самым популярным чисто логическим языком программирования. Давайте рассуждения об этом языке оставим на следующие разделы статьи, а пока что продемонстрируем «фишки» логических языков, используя Пролог.
Напишем небольшую программу, где перечислим, кто является людьми (ограничимся тремя) и добавим правило «всякий человек смертен»:
Что ж, давайте спросим у компьютера, смертен ли Сократ:
Компьютер выдал нам сухое «true», но мы, конечно, вне себя от счастья, так как вот-вот получим премию за успешное прохождение нашим умным устройством теста Тьюринга.
Предикат a от трех аргументов вернет истину, если удастся доказать истинность предикатов b, c и d. Читаются правила справа налево следующим образом: «Если b от X истинно И c от Y, Z истинно И d истинно, то a от X, Y, Z истинно».
Уже на таком небольшом примере видно, что мы не описываем четко последовательность действий, приводящую к нужному результату. Мы описываем необходимые условия, при выполнении которых результат будет достигнут. Тут будет к слову упомянуть, что раз компьютер сам для нас выводит способ достижения результата на основе известных правил, то и использовать один и тот же код можно по-разному:
Теперь начнём делать запросы к программе (всё те же предикаты):
Как видите, очень удобно. Стало быть, первым и очевидным применением логического программирования (об эффективности поговорим ниже) является работа с базами данных. Мы можем достаточно естественным образом описывать запросы, комбинируя предикаты, причем научить писать такие запросы можно даже человека, совершенно не знакомого с логическим программированием.
Какие задачи и как можно решать с помощью логического программирования
Давайте рассмотрим ряд учебных примеров (без подробного описания, все же статья обзорная) и подумаем, как те или иные подходы можно применять в реальной жизни. Начну с примера, призванного продемонстрировать, почему логическое программирование удобно, и за что же его любят математики. А именно, опишем правила вычисления производной:
Пусть производная получилась довольно громоздкой, но мы и не ставили цель её упростить. Главное, из примера видно, что правила вывода производной на Prolog-е описываются очень близким образом к их математическому представлению. Чтобы сделать подобное на привычных языках программирования, пришлось бы вводить понятие дерева выражений, описывать каждое правило в виде функции и т. д. Тут же мы обошлись 8-ю строками. Но здесь важно остановиться и задуматься: компьютер не начал работать как-то иначе, он все ещё обрабатывает последовательности команд. Стало быть, те самые деревья, которые где-то все-таки должны быть зашиты, чтобы программа работала, действительно присутствуют, но в неявном виде. Деревья эти именуют «деревьями вывода», именно они позволяют подбирать нужные значения переменных, перебирая все возможные варианты их значений (существует механизм отсечения, который является надстройкой над логической основой языка, но не будем об этом).
Давайте на простом примере рассмотрим, что из себя представляет перебор, а затем то, чем он может быть опасен.
Ага…то есть Петя, Петя и ложь… Что-то не так, подумает программист и попробует разобраться. На самом деле, перебирая все варианты значений X, Пролог пройдёт по такому дереву:
Представим, что перед нами в ячейках расположены три чёрных и три белых шара (как на картинке выше), которые требуется поменять местами. За один ход шар может или передвинуться в соседнюю пустую клетку, или в пустую клетку за соседним шаром («перепрыгнуть» его). Решать будем поиском в ширину в пространстве состояний (состоянием будем считать расположение шаров в ячейках). Суть этого метода заключается в том, что мы ищем все пути длины 1, затем все их продления, затем продления продлений и т. д., пока не найдем целевую вершину (состояние). Почему поиск в ширину? Он первым делом выведет самый оптимальный путь, то есть самый короткий. Как может выглядеть код решения:
Со стороны улучшения алгоритма можно предложить использовать поиск в глубину. Но как же, он ведь не даст оптимального результата? Сделаем просто: ограничим глубину поиска. Так мы точно не забьём стек и, возможно, получим ответ. Поступим так: проверим, есть ли пути длины 1, затем длины 2, затем длины 4 и т. д. Получим так называемый поиск с итерационным заглублением:
Во-первых, здесь стоит обратить внимание, что мы не используем очереди, а также внешних предикатов (кроме reverse, но он для красоты). Это потому, что поиск в глубину естественен для Пролога (ищите картинку с деревом выше). Во-вторых, пусть мы и делаем вроде как «лишние» действия, то есть для каждого нового значения глубины проходим по всем путям заново, мы практически не теряем в скорости относительно поиска в ширину (может в несколько раз, но не на порядок), при этом значительно экономим память. В-третьих, мы наконец-то получаем ответ, и это самое главное. Приводить его не буду, так как он займет много места, но для интриги оставлю вам его длину: 16.
С другой стороны, задачу можно было бы решить, не меняя код поиска, а лишь изменив правила перемещения шаров. Обратим внимание, что нам заранее известны входные и выходные данные. Приглядевшись становится понятно, что нет никакого смысла в движении фишек «назад». Действительно, если чёрным нужно встать в правые позиции, то какой смысл делать ходы влево? Перепишем предикаты движения:
Хм, код стал даже проще. Запустив мы убедимся, что поиск (оба варианта), во-первых, работает, во-вторых, работает быстро, в-третьих, работает быстро и выводит результат. Это успех. Мало того, что мы решили задачку, только что был создан самый настоящий искусственный интеллект. Программа получает входные данные и желаемый результат, а затем сама ищет, как его достигнуть. Да, это однозначно успех.
Зачем и где применяют логическое программирование
Давайте вернемся к рассмотренным примерам и попробуем представить, как это можно использовать на практике.
И тут крайне важно отметить, что решения на логических языках оказываются столь же неэффективны, сколько удобны (если речь не идёт о нишевых, специализированных решениях). Программа на императивном языке всегда обгонит аналогичную программу на логическом, но затраты на написание кода в ряде случаев (в том числе описанных выше) падают в разы. На практике вы вряд ли столкнетесь именно с Prolog-ом. Он, конечно, выразителен (можно описывать сложные вещи просто), хорошо расширяется, на нем легко писать надежный код и решать определенные задачи (в т. ч. просто логические задачки), но есть и ряд недостатков: пролог сильно уступает по скорости императивным языкам, а также не особенно поддерживается и не развивается, что делает его применение на практике практически невозможным.
Стоит ли планировать его изучение на 2021-й
Тут оставлю своё субъективное мнение, разделённое на две части:
И здесь остаётся лишь пожелать продуктивного 2021-го года!
Хочется выразить особую благодарность Дмитрию Сошникову за знакомство с этой удивительной парадигмой.
Математика для программистов
В статье пойдет речь о роли математики в жизни разработчика ПО. Мы не будем углубляться в частные области вроде машинного обучения, моделирования или же компьютерной графики, а сделаем упор на базовых математических вещах.
Этот материал предназначен в первую очередь для тех, кто уже сделал свои первые шаги в IT-индустрии, но в своем образовании уделял больше времени языкам программирования и конкретным технологиям, нежели фундаментальным вещам.
Как изучать математику
Многим людям математика кажется очень сложной для понимания наукой. Чаще всего, такое мнение складывается из-за неправильного подхода к ее изучению. На самом деле можно сильно упростить себе жизнь, следуя рекомендациям ниже.
В освоении математики есть два уровня понимания. Первый уровень — идейный. Это осознание того, для чего нужны определенные объекты, какая задача решается и где это используется. Второй уровень понимания — детальный; это подробное изучение подробностей решения задачи. Иногда нужно разобраться в задаче на детальном уровня понимания, но в большинстве случаев — достаточно идейного.
Математика не любит баззвордов. Если вы читаете книгу и видите слова, смысл которых вам непонятен, пропускать их опасно, потому как вы можете поймать себя на том, что с какого-то момента не понимаете вообще ничего. Очень важно сразу останавливать себя, когда вам что-то непонятно.
Дискретная математика
Область математики, которая занимается дискретными структурами (например: графами, автоматами, утверждениями в логике). Основное ее отличие от обычной математики, которую вы изучали в школе, — ее объекты не могут изменяться так же гладко, как и вещественные числа.
В каком-то смысле все задачи, которые решаются в программировании, так или иначе относятся к дискретной математике, поэтому ее знание очень вам пригодится.
Логика
Это наука о формальных системах и доказательствах. Она лежит в основе компьютерных наук, ведь любой язык программирования — формальная система. Но не нужно заглядывать глубоко в теорию, чтобы найти применение этой науке в написании программ, да и вообще в решении задач.
Хорошо, если вы умеете писать решение задачи. Но так же важно понимать, каким образом вы можете доказать, что ваш код работает правильно. Большинство программ решает какую-либо математическую задачу, и вам нужно уметь доказывать, что ваша задача решена правильно. Тогда на помощь приходят методы логики и в частности исчисление высказываний.
Изучение логики целесообразно начинать с простых вещей: например с того, что такое высказывание, какие есть операции между ними, что такое правила вывода. Далее можно перейти к более прикладным областям: старайтесь решать логические задачи, пробуйте оптимизировать разные проверки, которые вам приходится писать в коде. Далее, стоит обратить внимание на логику первого порядка: она может пригодиться в тестировании программ.
При этом решение, которое первым пришло вам в голову, не всегда самое правильное и красивое. Часто формальными преобразованиями можно сократить объем кода и сделать его более читаемым. А кроме того, некоторые логические трюки позволяют сделать само решение короче, быстрее и эффективнее.
Ресурсы:
Комбинаторика
Комбинаторика изучает разные дискретные множества и отношения их элементов. Наиболее часто встречаемая программистами комбинаторная задача — вывести количество элементов, которые необходимо перебрать, чтобы получить решение в зависимости от некоторых параметров. Таким образом вы можете вывести асимптотическую сложность алгоритма.
Комбинаторные задачи формулируются в виде задачи подсчета количества элементов некоторого (в математике используют термин мощность) множества. Чтобы решать такие задачи, полезно иметь базовые знания в теории множеств из разряда свойств операций над множествами. Тогда задача сводится к выражению искомого множества через множества, мощности которых вычисляются по известным правилам. Для подсчета количества элементов применяются правила умножения или сложения, числа сочетаний или размещений. Хотя есть и более сложные задачи, лучше начинать с простого.
Ресурсы:
Теория вероятностей
Иногда на собеседовании интервьюер, дабы проверить насколько крут кандидат, задает такую задачу: «Вот у нас есть отрезок, который начинается с числа А и заканчивается числом Б. Мы кидаем на него две точки случайным образом. Какая будет средняя длина наибольшего отрезка?» или же «Пусть у нас есть треугольник, на вершине которого сидит муха. Пусть она перелетает с вершины на вершину за 3 секунды и отдыхает на каждой вершине по секунде, каждый раз случайно выбирая себе путь. Через какое время она в среднем вернется в начальную точку?».
Это задачи по теории вероятностей. В программировании часто приходится применять вероятностный подход, для того чтобы оценить среднюю скорость работы алгоритма или же подогнать параметры вашего решения задачи под те запросы, которые чаще всего встречаются на практике.
Теория вероятности делится на две части: дискретную и непрерывную. Хотя в теории дискретная — это подкласс непрерывной, методы решения задач несколько различаются. Опять же лучше начинать с простого — дискретная теория вероятности часто сводится к комбинаторным задачам. И теоретическая часть у дискретной формулируется проще.
Непрерывная теория вероятности для полного понимания требует знания элементарных основ мат. анализа, в частности понятия интеграла, хотя многие задачи требуют лишь умения считать площади простых фигур. Именно непрерывная теория вероятности является фундаментом для математической статистики и машинного обучения. Поэтому, если хотите работать в этой области, стоит начать с изучения книги Ричарда Хэнсена Probability Theory and Statistics или Probability Theory with Simulations.
Ресурсы:
Теория графов
Слышали ли вы задачу о мостах Кенигсберга?
«Можно ли пройти по всем семи мостам города Кенигсберга, не проходя по каждому из них дважды?». Нам известно, что ответ на эту задачу — нет. Решить подобные задачи помогает теория графов.
Графы — это очень удобные формализованные представления нелинейных структур, которые довольно часто встречается в прикладных задачах. В отличие от простых линейных структур, таких как массивы или списки, работа с графами более сложна.
Изучите классические результаты и алгоритмы из теории графов, потому как некоторые задачи на графах являются NP-полными, и для них доказано существование более эффективного решения.
Ресурсы:
Теория чисел и криптография
Задумывались ли вы, почему к простым числам такой большой интерес? Почему работает шифрование RSA? Чем отличается http от https и что такое сертификат безопасности?
Все эти вопросы изучает криптография. Сразу скажем, что эта наука достаточно сложная и не интуитивная — бывает непонтяно, как реализовать тот или иной алгоритм совершенно безошибочно. Тем не менее алгоритмы в криптографии не могут быть «чуть-чуть нерабочими». Малейшая ошибка может привести к компрометации всей криптографической системы.
Дискретная оптимизация
Чтобы найти экстремум (максимум либо минимум) функции, надо взять ее производную и приравнять к нулю. Решение уравнения дает локальный экстремум. Но если вам нужно искать максимум не на каком-то промежутке, а только по целым числам, то вам уже нужно будет задумываться о том, какое из соседних целых чисел нужно выбрать. Когда задача многомерная, вариантов с целыми числами становится все больше, и выбирать приходится из все увеличивающегося количества. Но бывают случаи еще хуже — когда вовсе нет никакой непрерывной функции, от которой можно было бы взять производную. Или же когда количество вариантов очень велико (в том случае, когда сами варианты нужно вычислять).
Бывает, что в таких задачах нельзя найти точное решение за приемлемое время — его можно получить только полным перебором. Такова, например, задача Коммивояжера, или задача линейного программирования. Иногда можно отказаться от точного решения, и использовать некоторые приближения. Обо всем этом можно узнать в курсе Discrete Optimization на Coursera.
Источники
Небезызвестная серия курсов Introduction to Discrete Mathematics for Computer Science на Coursera по дискретной математике. Она довольно обширна и дает общее представление о всех нужных областях дискретной математики — логике, комбинаторике, теории вероятностей, теории графов, теории чисел и криптографии. Последний курс затрагивает проблему дискретной оптимизации.
Кроме того, для тех, кому не очень нравится формат курсов, будет полезной книга Discrete Mathematics. An Open Introduction. Книга довольно большая и подробная, поэтому можно сделать упор на основных понятиях и определениях.
Напоследок для тех, кого заинтересовала дискретная математика, приведем одну из наиболее подробных практико-ориентированных книг по дискретной математике. Довольно известная книга Кнута, Грехема и Паташника «Конкретная математика». Она написана в неформальном стиле, изложение разбавлено комментариями на полях. Книга очень полезна для развития умения решать разные задачи. Однако в ней много частных вещей, которые могут пригодится только в олимпиадном программировании.
Что дальше?
В целом, для того чтобы иметь достаточный математический фундамент для изучения большинства областей, достаточно первых двух курсов, изучаемых на математических специальностях. К дискретной математике добавляются некоторые разделы непрерывной: линейная алгебра, общая алгебра, математический анализ, аналитическая геометрия, обыкновенные дифференциальные уравнения, методы оптимизации. В зависимости от специфики решаемых задач, к ним могут добавиться и дифференциальная геометрия, если вы собираетесь заниматься компьютерной графикой, или же теоретическая механика и мат. физика, если вы собираетесь заниматься физическими движками.
Математическая логика и языки программирования
Образно выражаясь, можно сказать, что компьютер состоит из материальной части и математического (программного) обеспечения, или, используя профессиональную лексику, из «железа» и «обуви». И к тому, и к другому имеет самое непосредственное отношение математическая логика, ни первое, ни второе без математической логики обойтись не могут. Ранее здесь и здесь было рассмотрено применение математической логики к релейно-контактным (переключательным) схемам, являющимся неотъемлемой составной частью современного компьютера. Часть настоящей главы также посвящена вопросам взаимодействия математической логики и компьютеров. Так, в этой статье рассказывается о применении математической логики к языкам программирования и к самому процессу программирования и получающимся в результате этого программам. В статье дается характеристика обратного процесса — применению компьютеров для поиска доказательств теорем математической логики и других математических дисциплин. Значительное внимание уделено методу резолюций для доказательства теорем в исчислениях высказываний и предикатов. В статье кратко описывается язык ПРОЛОГ — принципиально новый язык программирования, выросший непосредственно из математической логики (логики- предикатов) и призванный стать языком компьютеров пятого поколения.
В свою очередь, информатика как наука начала оформляться вместе с созданием и бурным развитием вычислительной техники. Ее формирование и определение ее предмета продолжаются по настоящее время. Информатика — наука о хранении, обработке и передаче информации с помощью компьютеров. Она включает в себя крупные разделы, изучающие алгоритмические, программные и технические средства хранения, обработки и передачи информации. Математическая логика оказалась единственной математической наукой, методы которой стали мощнейшими инструментами познания во всех разделах информатики. Поэтому сколько-нибудь серьезное изучение информатики немыслимо без освоения основ математической логики.
Вторая часть настоящего раздела посвящена тем вопросам математической логики, которые находят наиболее яркое применение в информатике, а также краткому показу того, как математическая логика работает в некоторых разделах информатики. Здесь будет рассказано о применении математической логики при исследованиях, посвященных базам данных, базам знаний и системам искусственного интеллекта.
Чтобы компьютер работал, он должен быть оснащен программным обеспечением, т.е. комплексом программ, ориентирующих компьютер на решение задач того или иного класса. (Слово «программа» имеет греческое происхождение и означает «объявление», «распоряжение».) Уже само понятие компьютерной программы, предусматривающее четкое алгоритмическое предписание компьютеру о порядке и характере действий, предусматривает проникновение в программу, а также в процесс ее составления (в программирование) теории алгоритмов. Но при более пристальном рассмотрении процесс проникновения логики в программы и программирование оказывается значительно более глубоким и органичным. Не только один ее раздел — теория алгоритмов — работает здесь, но исключительно действенным оказывается само существо математической логики — ее язык, ее аксиоматические теории, выводы и теоремы в них, свойства этих теорий.
В данном параграфе дается краткий обзор основных направлений, по которым математическая логика внедряется в программирование, из которых программирование возникло и без которых существовать не может.
Теория алгоритмов и математическая логика — фундаментальная основа программирования. В 30-е гг. XIX в. английский математик Чарлз Бэббедж высказал впервые идею вычислительной машины. И только сто лет спустя логики разработали четыре математически эквивалентные модели понятия алгоритма (мы достаточно подробно рассмотрели в предыдущей главе три из них). Именно в теории алгоритмов были предугаданы основные концепции, которые легли в основу принципов построения и функционирования вычислительной машины с программным управлением и принципов создания языков программирования. Идею такой вычислительной машины впервые смогли реализовать болгарский ученый С. Атанасов в 1940 г. и немецкий ученый К. Цузе в 1942 г. Четыре главные модели алгоритма породили разные направления в программировании.
Первая модель — это абстрактная вычислительная машина (А. Тьюринг, Р. Пост). Она явилась абстрактным прообразом реальных вычислительных машин. До сих пор все вычислительные машины в некотором смысле базируются на идее Тьюринга: их память физически состоит из битов, каждый из которых содержит либо 0, либо 1. Программное управление унаследовало от этих абстрактных машин и программу, помещенную в «постоянную память» (идея поместить программу ЭВМ в основную память, чтобы иметь возможность изменять ее в ходе вычислений, принадлежит Джону фон Нейману), а структура команды современной ЭВМ в значительной степени напоминает структуру команды машины Тьюринга. В рамках теории машин Тьюринга откристаллизовались важнейшие для компьютерных приложений логики понятия: вычислимая функция, разрешимая задача, неразрешимая (алгоритмически) задача. Собрано большое количество определений абстрактных вычислительных машин и показано, как каждое из них можно свести к другому подходящей кодировкой входов и выходов.
Другая модель — это рекурсивные функции, идея которых восходит к гильбертовскому аксиоматическому подходу. От них унаследовало свои основные конструкции современное структурное программирование.
Третий способ описания алгоритмов — нормальные алгоритмы А. А. Маркова. Они послужили основой языка Рефал и многих других языков обработки символьной информации.
Четвертое направление в теории алгоритмов — так называемое λ-исчисление — базируется на идеях советского логика Р.Шейнфинкеля и американского логика X. Б. Карри. Оказалось, что для определения всех вычислимых функций достаточно операций так называемой λ-абстракции и суперпозиции. Идеи λ-исчисления активно развиваются в языке Лисп, функциональном программировании и во многих других перспективных направлениях современного программирования.
Математическая логика стала бурно развиваться в начале XX в. на почве казалось бы исключительно далекой от приложений проблемы обоснования математики. Но именно эти исследования положили начало строгому определению алгоритмических языков, показали их колоссальные возможности и принципиальные ограничения, развили технику формализации. Поэтому, когда в программировании было осознано, что всякая программа есть формализация, то возникшие здесь математические проблемы упали на почву, тщательно подготовленную математической логикой.
Описание компьютерных программ с помощью математической логики
Первые попытки применить в программировании развитые логические исчисления и методы формализации предпринял американский логик X. Б. Карри. В 1952 г. он сделал доклад «Логика программных композиций», идеи которого опередили свое время по крайней мере на четверть века. Карри рассмотрел задачу программирования как задачу составления более крупных программ из готовых кусков. Были введены две базисные системы конструкций: первая — последовательное исполнение, разветвление и цикл, вторая — последовательное исполнение и условный переход. Он охарактеризовал логические средства, какие можно использовать для композиции программ из подпрограмм в каждом из этих случаев.
Как известно, компьютер является своего рода «идеальным бюрократом»: он не воспримет программу, написанную на не до конца формализованном языке, и приступит к работе лишь после того, как все выражено в полном соответствии с детальными инструкциями. Поэтому в 1960-е гг. на первый план вышли задачи точного определения формальных языков достаточно сложной структуры. Математическая логика, подпитываемая идеями программирования, успешно с ними справилась, разработав описание синтаксиса сложных и богатых по выразительным средствам формальных языков.
В середине 1960-х гг. практически одновременно появился ряд пионерских работ в области описания условий, которым удовлетворяет программа. Советский математик В. М. Глушков в 1965 г. ввел понятие алгоритмической алгебры, послужившее прообразом алгоритмических логик. Ф. Энгелер в 1967 г. предложил использовать языки с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при разных исполнениях программы. Но наибольшую популярность приобрели языки алгоритмических логик. Эти языки были изобретены практически одновременно американскими логиками Р.У.Флойдом (1967), С.А.Р.Хоаром (1969) и учеными польской логической школы, например А. Сальвицким и др. (1970).
Наряду с динамической логикой 1-го порядка рассматривается пропозициональная динамическая логика и ее обобщение — так называемая логика процессов, в которой выразимы некоторые свойства программы, зависящие от процесса ее выполнения. Различные динамические логики получаются при варьировании средств языков программирования, используемых в программах. Эти средства содержат массивы и другие структуры данных, рекурсивные процедуры, циклические конструкции, а также средства задания недетерминированных программ.
Динамическая логика является одним из типов логических систем, используемых для логического синтеза компьютерных программ. Логический синтез — один из способов перехода от спецификации программы к реализующему алгоритму, имеющий форму точного рассуждения в некоторой логической системе. В динамической логике спецификация задачи задается в виде двух формул исчисления предикатов — предусловия и постусловия, а аксиомами логической системы являются схемы предусловий и постусловий, связываемых теми или иными конструкциями языка программирования. Синтезируемая программа получается в форме выводимого в динамической логике утверждения, гласящего, что если аргументы задачи удовлетворяют заданному предусловию, то результат выполнения синтезированной программы удовлетворяет заданному постусловию.
В теоретических работах по динамическим логикам исследуются вопросы непротиворечивости и полноты аксиоматических систем, алгоритмические сложностные свойства множеств истинных формул, сравнения выразительной мощности языков динамической логики.
Принципиально иной способ определения семантики программ, пригодный, скорее для описания всего алгоритмического языка, а не конкретных программ, предложил в 1970 г. американский логик Д. Скотт. Он построил математическую модель λ-исчисления и показал, как переводить функциональное описание языка структурного программирования в λ-исчисление и как определить математическую модель алгоритмического языка через модель λ-исчисления. Эта так называемая денотационная семантика алгоритмических языков, работы по которой насчитываются уже тысячами, стала практическим инструментом построения надежных трансляторов со сложных алгоритмических языков. Так еще одна абстрактная область математической логики нашла прямые практические приложения.
Описание программирования и анализ его концепций с помощью математической логики
Программирование — это процесс составления программы, плана действий. Было замечено, что классическая логика плохо подходит для описания этого процесса хотя бы потому, что она плохо подходит вообще для описания всякого процесса в математике. Еще в начале XX в. стало ясно, что в математике Давно разошлись понятия «существовать» и «быть построенным», с античных времен трактовавшиеся как синонимы. Были выявлены так называемые математические объекты-«привидения» (множества, Функции, числа), существование которых доказано, но построить которые нельзя. Причиной их появления явился эффект сочетания классической логики с теоремой Гёделя о неполноте формальной арифметики. Один из фундаментальных законов классической логики — закон исключенного третьего в некоторой свободной трактовке фактически означает, что мы знаем все. Этот постулат конечно же никак нельзя назвать реалистическим: мы знаем чрезвычайно мало, и чем больше узнаем, тем лучше это понимаем. Голландский математик Л. Э. Я. Брауэр определил логические корни «привидений» еще до открытия теоремы Гёделя, в 1908 г., и начал построение так называемой интуиционистской математики, не принимающей закон как универсальный. В 1930–1932 гг. другой голландец А. Гейтинг строго сформулировал логику, которой пользовались в интуиционистской математике, — интуиционистскую логику. Ее математическая интерпретация, данная советским математиком А. Н. Колмогоровым в то же время, сохранила свое значение до сих пор.
Описание программирования с помощью логики основано на определенной аналогии между выводом формулы в некотором логическом исчислении и программой решения задачи, отвечающей этой формуле при конструктивной интерпретации логики. Логическая теория, соответствующая структурным схемам программ, появилась в середине 1980-х гг. Структурные схемы соответствовали нарождающемуся новому типу логики — логики схем программ, которой пользуется программист для создания сложных, многовариантных, итеративных планов действий.
Имеется корректная и полная система конструктивных правил вывода (логика ), позволяющих при помощи некоторой структурной схемы построить доказательство возможности преобразовать в на базе заданных функций, преобразующих некоторые в
правило условного оператора (ПУО);
правило релаксации (ПР);
правило зацикливания (ПЗ);
правило бесконечного цикла (ПБЦ);
Таким образом, конструктивное описание ситуации, где классические средства работают плохо, оказалось весьма компактным и эффективным.
Логика — лишь одна из простейших логик схем программ, успешно используемых в автоматизированном планировании действий.
Задача построения программы выражается в интуиционистской логике с помощью функциональной формулы:
Здесь — входные переменные создаваемой программы; — ее результаты; задают связи вход-выход; амбивалентны: они могут представлять как условия на входы, так и входные значения сложных типов (структуры данных, функции-параметры). Например, формула
Из-за отсутствия принципа всезнания выразительные возможности интуиционистской логики существенно повышаются по сравнению с классической. На ее языке можно постулировать не только знание, но порой и незнание. Например, то, что значение действительного числа не может быть задано точно, постулируется в форме
Но повышение выразительной силы и «аккуратности» выводов в интуиционистской логике по сравнению с классической имеет и оборотную сторону: поиск вывода в ней существенно сложнее. В частности, метод резолюций в ней неприменим, потому что формулы не могут быть разложены на дизъюнкты.
Интуиционистская логика хорошо подходит для описания задач, в которых требуется вычислить новые величины по заданным величинам и ни один из вычислительных ресурсов (время, память, надежность) не налагает ограничений. Для других ситуаций интуиционистскую логику приходится варьировать.
Впервые на возможности логики в качестве инструмента анализа понятий программирования обратили внимание в середине 1970-х гг. в связи с развитием теории верификации (проверки правильности) программ. Оказалось, что для многих конструкций программирования, совместное использование которых не приводит к алгоритмической невычислимости, невозможно построить полную формальную систему, описывающую их взаимодействие. Например, рассмотрение логики схем программ позволило установить, что операторы GOTO естественно получаются в том случае, если все рассматриваемые действия можно считать глобальными преобразованиями состояния системы. Циклы оказались хорошо совместимы с массивами и плохо — с рекурсивными структурами данных, а процедуры высших типов — наоборот. Массивы и сложные структуры данных плохо совместимы с присваиваниями (в данном случае присваивание дается на целый ряд операторов, несущих различный логический смысл).
В общем, можно сделать вывод, что нет средств программирования хороших либо плохих самих по себе; хороши или плохи их комбинации. При этом любая логически разумная комбинация оказывается неуниверсальной, она приспособлена лишь для определенного класса задач.
Верификация (доказательство правильности) программ с помощью математической логики
Широчайшее использование компьютеров в самых разнообразных сферах человеческой деятельности выдвигает на одно из первых мест вопрос о надежности программного обеспечения компьютеров. Как известно, правильность созданной программы обычно проверяется на ряде так называемых тестовых примеров, на начальных данных, для которых результат известен или его можно предсказать. Нетрудно понять, что такая проверка способна лишь выявить наличие ошибок в программе, но не доказать их отсутствие, что, разумеется, не одно и то же.
Поэтому исключительно важна задача строгого доказательства правильности программ, и именно для этой цели и начали разрабатываться программные и динамические логики.
С интуиционистской точки зрения программа будет правильной, если в результате ее выполнения будет достигнут тот результат, с целью получения которого и была написана программа. (Обратите внимание, что мы не рассматриваем программы, содержащие синтаксические ошибки, т. е. предполагаем, что с точки зрения языка программирования программа написана безупречно.) Доказательство правильности программы состоит в предъявлении такой цепочки аргументов, которые убедительно свидетельствуют о том, что это действительно так, т.е. что программа на самом деле решает поставленную задачу.
Говорить о правильности программы самой по себе бессмысленно. Программа пишется с целью решения той или иной конкретной задачи. Каждая правильно поставленная задача содержит в себе условие (то, что дано) и вопрос, на который нужно дать ответ. При составлении программы условие задачи превращается в предусловие, а вопрос преобразуется в постусловие, имеющее уже форму не вопроса, а утверждения, которое должно быть истинно всякий раз, когда ответ на вопрос задачи правилен.
Из определений следует, что всякая тотально правильная программа является частично правильной при тех же пред- и постусловиях. Обратное конечно же неверно. Ясно, что тотальная правильность «лучше» частичной, хотя доказать тотальную правильность программы, по-видимому, сложнее, чем частичную.
Для доказательства частичной правильности операторных программ обычно используются различные модификации метода Флойда, который состоит в следующем. На схеме программы выбираются контрольные точки так, чтобы любой циклический путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется специальное условие (индуктивное утверждение или инвариант цикла), которое истинно при каждом переходе через эту точку. С входом и выходом схемы также ассоциируются пред- и постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется так называемое условие правильности. Выполнимость всех условий правильности гарантирует частичную правильность программы.
Один из способов доказательства завершения работы программы состоит во введении в программу дополнительных счетчиков для каждого цикла и в доказательстве их ограниченности в процессе доказательства частичной правильности программы.
Одна из модификаций метода Флойда заключается в построении конечной аксиоматической системы (так называемой «логики Хоара»), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ, в частности на языке программирования Паскаль. Такая система используется и для задания аксиоматической семантики языка Паскаль. Аксиоматические системы, родственные логике Хоара, разработаны и для других алгоритмических языков программирования.
Для доказательства правильности рекурсивных программ используется метод математической индукции, связанный с определением наименьшей неподвижной точки, а для программ со сложными структурами данных (например, графами, деревьями) — индукция по структуре данных. При этом в теоретических исследованиях по логике Хоара рассматриваются обычные свойства аксиоматизаций в логике — их непротиворечивость и полнота.
б) после завершения цикла;
в) в ходе выполнения цикла.
В заключение отметим, что исследования по логическому описанию программ и программирования убедительно показали, что логический анализ позволяет анализировать концепции языков программирования и находить многие скрытые недоработки в этих концепциях. Пожалуй, до сих пор это применение строгих математических методов в качестве инструмента критики концепций (зачастую совершенно не продуманных, вставляемых ради «усиления» языков программирования) является важнейшим применением математической логики в области программирования.