Игошин Математическая логика и теория алгоритмов (1019110), страница 96
Текст из файла (страница 96)
Теория алгоритмов и математическая логика — фундаментальная основа программирования. В 30-е гг. Х1Х в. английский математик Чарлз Бэббедж высказал впервые идею вычислительной машины. И только сто лет спустя логики разработали четыре математически эквивалентные модели понятия алгоритма (мы достаточно подробно рассмотрели в предыдущей главе три из них). Именно в теории алгоритмов были предугаданы основные концепции, которые легли в основу принципов построения и функционирования вычислительной машины с программным управлением и принципов создания языков программирования.
Идею такой вычислительной машины впервые смогли реализовать болгарский ученый С.Атанасов в 1940 г. и немецкий ученый К. Цузе в !942 г. Четыре главные модели алгоритма породили разные направления в программировании. Первая модель — это абстрактная вычислительная машина (А.Тьюринг, Р.Пост). Она явилась абстрактным прообразом реальных вычислительных машин. До сих пор все вычислительные 386 машины в некотором смысле базируются на идее Тьюринга: их память физически состоит из битов, каждый из которых содержит либо О, либо 1.
Программное управление унаследовало от этих абстрактных машин и программу, помещенную в «постоянную память» (идея поместить программу ЭВМ в основную память, чтобы иметь возможность изменять ее в ходе вычислений, принадлежит Джону фон Нейману), а структура команды современной ЭВМ в значительной степени напоминает структуру команды машины Тьюринга. В рамках теории машин Тьюринга откристаллизовались важнейшие для компьютерных приложений логики понятия: вычислимая функция, разрешимая задача, неразрешимая (алгоритмически) задача.
В [9.151 собрано большое количество определений абстрактных вычислительных машин и показано, как каждое из них можно свести к другому подходящей кодировкой входов и выходов. Другая модель — это рекурсивные функции, идея которых восходит к гильбертовскому аксиоматическому подходу. От них унаследовало свои основные конструкции современное структурное программирование.
Третий способ описания алгоритмов — нормальные алгоритмы А.А. Маркова. Они послужили основой языка Рефал и многих других языков обработки символьной информации. Четвертое направление в теории алгоритмов — так называемое ):исчисление — базируется на идеях советского логика Р.Шейнфинкеля и американского логика Х. Б. Карри. Оказалось, что для определения всех вычислимых функций достаточно операций так называемой Х-абстракции и суперпозиции. Идеи Х-исчисления активно развиваются в языке Лисп, функциональном программировании и во многих других перспективных направлениях современного программирования.
Математическая логика стала бурно развиваться в начале ХХ в. на почве казалось бы исключительно далекой от приложений проблемы обоснования математики. Но именно эти исследования положили начало строгому определению алгоритмических языков, показали их колоссальные возможности и принципиальные ограничения, развили технику формализации. Поэтому, когда в программировании было осознано, что всякая программа есть формализация, то возникшие здесь математические проблемы упали на почву, тщательно подготовленную математической логикой. Описание компьютерных программ с помощью математической логики. Первые попытки применить в программировании развитые логические исчисления и методы формализации предпринял амеРиканский логик Х.Б. Карри. В 1952 г.
он сделал доклад «Логика пРограммных композиций», идеи которого опередили свое время по крайней мере на четверть века. Карри рассмотрел задачу про"Раммирования как задачу составления более крупных программ из 387 готовых кусков. Были введены две базисные системы конструкций; первая — последовательное исполнение, разветвление и цикл, вторая — последовательное исполнение и условный переход. Он охарактеризовал логические средства, какие можно использовать лля композиции программ из подпрограмм в каждом из этих случаев Как известно, компьютер является своего рода «идеальным бюрократом»: он не воспримет программу, написанную на не до конца формализованном языке, и приступит к работе лишь после того, как все выражено в полном соответствии с детальными инструкциями.
Поэтому в 1960-е гг. на первый план вышли задачи точного определения формальных языков достаточно сложной структуры. Математическая логика, подпитываемая идеями программирования, успешно с ними справилась, разработав описание синтаксиса сложных и богатых по выразительным средствам формальных языков. В середине 1960-х гг. практически одновременно появился ряд пионерских работ в области описания условий, которым удовлетворяет программа. Советский математик В. М. Глушков в 1965 г.
ввел понятие алгоритмической алгебры, послужившее прообразом алгоритмических логик. Ф.Энгелер в 1967 г. предложил использовать языки с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при разных исполнениях программы.
Но наибольшую популярность приобрели языки алгоритмических логик. Эти языки были изобретены практически одновременно американскими логиками Р.У. Флойдом (1967), С.А. Р. Хоаром (1969) и учеными польской логической школы, например А. Сальвицким и др. (1970). Алгоритмическая логика (или динамическая логика, или программная логика, или логика Хоара) — раздел теоретического программирования, в рамках которого исследуются аксиоматические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации (проверки правильности работы). Языки алгоритмических логик основываются на логике предикатов 1-го порядка и включают в себя высказывания вида (А)В(В), читающиеся следующим образом: «Если до исполнения оператора убыло выполнено А, то после него будет выполнено В».
Здесь А называется предусловием,  — постусловием, либо обещанием В. На этом языке даются логические описания операторов присвоения и условного перехода, ветвления, цикла. Наряду с динамической логикой 1-го порядка рассматривается пропозициональная динамическая логика и ее обобщение — так называемая логика процессов, в которой выразимы некоторые свойства программы, зависящие от процесса ее выполнения.
Различные динамические логики получаются при варьировании средств языков программирования, используемых в программах. Эти сред- 388 ства содержат массивы и другие структуры данных, рекурсивные процедуры, циклические конструкции, а также средства задания иедетерминированных программ. Динамическая логика является одним из типов логических систем, используемых для логического синтеза компьютерных программ. Логический синтез — один из способов перехода от спецификации программы к реализующему алгоритму, имеющий форму точного рассуждения в некоторой логической системе. В динамической логике спецификация задачи задается в виде двух формул исчисления предикатов — предусловия и постусловия, а аксиомами логической системы являются схемы предусловий и постусловнй, связываемых теми или иными конструкциями языка программирования.
Синтезируемая программа получается в форме выводимого в динамической логике утверждения, гласящего, что если аргументы задачи удовлетворяют заданному предусловию, то результат выполнения синтезированной программы удовлетворяет заданному постусловию. В теоретических работах по динамическим логикам исследуются вопросы непротиворечивости и полноты аксиоматических систем, алгоритмические сложностные свойства множеств истинных формул, сравнения выразительной мощности языков динамической логики.
Принципиально иной способ определения семантики программ, пригодный скорее для описания всего алгоритмического языка, а не конкретных программ, предложил в 1970 г. американский ло- гик Д.Скотт. Он построил математическую модель А-исчисления и показал, как переводить функциональное описание языка структурного программирования в Х-исчисление и как определить математическую модель алгоритмического языка через модель Х-исчисления. Эта так называемая денотационная семантика алгоритмических языков, работы по которой насчитываются уже тысячами, стала практическим инструментом построения надежных трансляторов со сложных алгоритмических языков.
Так еще одна абстрактная область математической логики нашла прямые практические приложения. Описание программирования и анализ его концепций с помощью математической логики. Програияирование — это процесс составления программы, плана действий. Было замечено, что классическая логика плохо подходит для описания этого процесса хотя бы потому, что она плохо подходит вообще для описания всякого процесса а математике.
Еше в начале ХХ в. стало ясно, что в математике давно разошлись понятия «существовать» и «быть построенным», с античных времен трактовавшиеся как синонимы. Были выявлены так называемые математические объекты-«привидения» (множества, Функции, числа), существование которых доказано, но построить которые нельзя. Причиной их появления явился эффект соче- 389 тания классической логики с теоремой Геделя о неполноте фор мальной арифметики.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
