Для чего нужна математическая логика программисту

Математика для программиста

Вступление

Приветствую. Я занимаюсь программированием и 3D-дизайнером, а также относительно недавно приступил к изучению основ кибербезопасности. Сейчас в процессе учебы столкнулся с интересной ситуацией, когда необходимо применять сложные математические алгоритмы для решения разных задач. Кроме того, подумал, о том, что раньше я по-другому смотрел на математику и не любил её. Следовательно, моё мнение об этом предмете изменилось, и я решил, что это может пригодиться другим, кто решил идти в программирование. Статья будет больше теоретической, но если будет интересно, пример подтверждения на практике сделаю в будущих статьях.

Основная мысль

Один из самых частых вопросов, который задают новички, люди, далёкие от программирования, и один из самых больших стереотипов современности: нужна ли математика программисту? И ведь точно на этот вопрос никто не даст полного ответа. Это связанно с тем, что направлений в программировании очень много.

Современные языки программирования, которые и очень популярны одновременно, сейчас, способны решать многие задачи очень быстро, а их инструментарий специально сделан таким образом, чтобы не вызывать дискомфорта у разработчиков в процессе разработки.

Конечно, большинство современных разработчиков предпочитают уходить больше в Frontend, Backend и не создавать себе проблем с изучением языков никого уровня.

Программисты, которые работают в этих сферах и пишут на JavaScript, Python, PHP и т. д. зарабатывают хорошие деньги, работают в высокоуровневом программировании, знают несколько технологий и не выполняют сложных математических вычислений. В большинстве случаев. Всё это хорошо, особенно, когда люди знают, что хотят. И когда им задают вопрос, «Нужна ли математика» говорят, что нужна лишь базовая для такого рода работ, а вот для более сложных проектов и технологий стоит дополнительно изучать что-то и посложнее школьной программы.

И другое дело, когда такие же разработчики, которые работают только с высоким уровнем и программируют сайты, отвечаю на такой же вопрос. Говорят, что математика вообще не нужна. Максимум-это сложение, вычитание, деление и умножение. И что дальше сочетательного закона идти не стоит.

Вполне логично. Однако стоит подумать про одну важную деталь, которую почти никто никогда не озвучивает. Дело в том, что ведь все компьютеры и ЭВМ работают с помощью математики. И что у истоков всего программирования стоит математика.

Вся программная арифметика связана с числами. В компьютерах используется бинарный код (1 и 0). Именно на этом коде и работают системы, начиная от операционных и заканчивая нейронными сетями. Всё, что связанно с вычислениями, всегда взаимодействует и цифрами.

Вспомним, что все люди, которые создавали подобные вещи в вычислительных науках, всегда имели хорошие знания во всеми нелюбимом школьном предмете. А ведь современные компьютерные технологии никуда эту науку не убрали.

Все сложные низкоуровневые языки программирования базируются на математике, да и современные высокоуровневые тоже, ведь в них заложена основа из никого уровня. А ведь, чем выше уровень языка, тем тяжелее создать что-то сложное и большое.

Поэтому зачастую все стараются избежать изучения С/С++, Java и других подобных языков, а предпочитают уходить в веб-разработку, где процесс понимания направления и технологий более легкий, и платят не хуже.

Вывод

Задумайтесь, все сложные вещи пишутся на низких языках и включают математические знания. Конечно, нет необходимости учить весь курс вышмата, но если вы серьёзно захотите создать, например, свою ОС, написать крутой фреймворк, или уникальный искусственный интеллект, то без хороших математических знаний и соответствующих навыков в ЯП это будет сделать почти невозможно.

Отвечая на вопрос, «Нужна ли математика программисту? », я могу смело дать ответ: «Да». Каким бы ни был программист и что бы он ни делал, чем больше знаний в точных областях он будет знать, тем лучше для него, как специалиста.

Нельзя пренебрегать этой наукой, и уж точно нельзя говорить, что достаточно будет знать только сложения, вычитания, умножения и деления. А как вы считаете?

Источник

Насколько важна математическая подготовка в перспективных направлениях разработки ПО

Профессия программиста становится все более массовой и востребованной. Сейчас порог вхождения в ИТ-сферу в принципе снизился, но продолжает расти интерес к ИТ-технологиям в целом, и к программированию в частности.

Среди ИТ-компаний и программистов, тем не менее, растет конкуренция. Однако стоит отметить, что, по крайней мере, на рынке труда она достаточно честная. Например, принимая на работу программиста работодатель в первую очередь будет оценивать уровень реальных знаний и навыков, а не цвет диплома. Впрочем, эта ситуация способствует распространению «программистов-самоучек», которые ограничены узкой специализацией. Для них нередко оказывается справедливо выражение «шаг вправо, шаг влево – расстрел». Так что, сейчас недостаточно сказать: этот человек – «ИТшник», или даже программист. Программист программисту рознь.

Специализации программистов множатся и развиваются, программист, специализирующийся в одной области приложений, не всегда может понять своего коллегу, работающего в другой области. Хотя вроде бы и языки программирования, и технологии одни и те же. Области приложений могут кардинально отличаться друг от друга, и для того, чтобы писать специализированные программы, мало знать языки и технологии программирования, нужно хорошо разбираться в той области, для которой разрабатывается программный продукт. В последнее время все чаще при изучении предметной области возникает необходимость в математической формализации.

Я учился в ВУЗе, в котором раньше, лет 30-40 назад, не существовало специальности «Инженер-программист». Однако люди, занимающиеся программированием, там были – их называли «ПМщики». Дело в том, что учились они на кафедре Прикладной математики. Но справедливо было бы все-таки называть их математиками, нежели программистами.

Шли годы, и со временем кафедра стала курировать новую специальность – «Программное обеспечение вычислительной техники и автоматизированных систем». Математики в учебной программе стало гораздо меньше, а преподаватели начали сетовать, что у выпускников школ большие проблемы с математикой. То есть, зачисляясь на первый курс, многие студенты уже имеют достаточно слабую математическую базу, а так как времени на этот предмет теперь меньше в учебном плане, то надежды на улучшение ситуации мало.

Конечно, можно еще вспомнить, что раньше была и трава зеленее, и небо голубее… Но где же программистам прокачивать матчасть в сегодняшних условиях? Означает ли это, что теперь на «серьезные» позиции разработчиков будут охотнее брать математиков, а не программистов?

Новые реалии

Уже на последних курсах университета студенты часто узнают, что появились новые технологии, которые в ВУЗе не изучались: их просто не успели включить в учебную программу. Однако благодаря фундаментальному образованию, заложенным основам будущие специалисты могут легко изучить эти технологии самостоятельно. Но тут и встает вопрос о качестве этого образования. Всего ли там достаточно для сегодняшних требований рынка труда?

В последнее время новые технологии стали более наукоемкими – точнее, математикоемкими. Во многих областях человеческой деятельности стало активнее применяться математическое моделирование различных процессов, пишут в своем послании абитуриентам представители Новосибирского государственного технического университета.

Физическая реализация экспериментов, экспериментальная проверка выдвинутых гипотез являются очень дорогостоящими, как правило, требуют значительных человеческих и материальных ресурсов. А имитация экспериментов на математических моделях, выявление закономерностей в ходе многократного моделирования оказывается на порядки дешевле.

На основе математических моделей разрабатывается соответствующее программное обеспечение, реализующее математическую модель объекта и математические методы, позволяющие найти оптимальное решение. И если мы заменяем физический эксперимент математическим, то должны быть уверены, что их результаты совпадают. «И как тут специалисту по IT-технологиям обойтись без глубоких математических знаний и вычислительных методов?», задают вопрос они.

До начала 90-х годов, неспешно развивалась так называемая прикладная статистика. Но развивалась она больше в теоретическом плане, чем в практическом.

А «в один прекрасный» день настала необходимость адаптировать ее к практике. В связи с совершенствованием технологий записи и хранения данных на людей обрушились колоссальные потоки информации в самых различных областях. Деятельность любого предприятия (коммерческого, производственного, медицинского, научного и тд) теперь сопровождается регистрацией и записью всех подробностей его деятельности.

Стало ясно, что без продуктивной переработки потоки данных образуют никому не нужную свалку. Выявление в накопленной информации скрытых закономерностей является задачей интеллектуального анализа данных (Data Mining) – составной части процесса принятия решений. Если смотреть глубже, то в основе интеллектуального анализа данных лежит широкий спектр методов теории вероятностей и математической статистики.

Знания математики нужны большинству программистов, вот только какие именно разделы нужны для разработки того или иного вида ПО? Что нужно знать для того чтобы, программировать игры, искусственный интеллект, big data, научный софт и так далее?

Иван Хватов, разработчик ПО, «Яндекс»:

Насколько нужна программисту математика? Опишите, пожалуйста, свою историю отношений с матчастью.

В целом, нужна. В каких-то областях — больше, в каких-то — меньше. После университета в теорию погружался только если была необходимость по задачам.

В каких направлениях разработки необходима матчасть? Почему? Какие разделы математики там нужны?

Направлений много. Всего не перечислишь. Если, например, говорить про текущий хайп, то необходимо хорошо знать статистику. Базовый уровень, который надо знать везде: университетский курс математической логики, теории вероятности, статистики и дискретной математики.

Можете посоветовать, как подтянуть математический аппарат программистам, давно закончившим ВУЗ? Могут ли здесь быть какие-то сложности?

Проходить онлайн-курсы. Сейчас с этим нет проблем.

Чем отличается математическое мышление от программистского (алгоритмического)?

Не знаю, я бы это не разделял.

Какие специалисты лучше подходят для математикоемкой разработки: математики с азами программирования или программисты с азами математики?

Антон Каракулов, веб-разработчик, ТМ

Насколько нужна программисту математика? Опишите, пожалуйста, свою историю отношений с матчастью.

Всё зависит от того какие задачи предстоит решать программисту. Чем больше прикладных — тем реже нужна матчасть. Чем более системных — тем чаще оказывается востребованной.

К сожалению мои какие-либо внятные отношения с ней закончились на 2 курсе института. В тот момент ещё верилось, что она будет мне полезна и нужна, но в силу обстоятельств отвлёкся на другие знания, и потом уже было очень сложно вернуться к абстрактному изучению.

В каких направлениях разработки необходима матчасть? Почему? Какие разделы математики там нужны?

Как сказал уже выше, чем больше системных задач решается программистом, чем больше нужно знание матчасти. В названии мат. дисциплин всегда путался что к чему, поэтому тут что-то сказать уверено не могу.

Можете посоветовать, как подтянуть математический аппарат программистам, давно закончившим ВУЗ? Могут ли здесь быть какие-то сложности?

От тру-программиста слышал мнение что на coursera хорошие курсы на любой вкус. Можно начать с базовых, а дальше уже выбирать по интересам и необходимостям.

Чем отличается математическое мышление от программистского (алгоритмического)?

Математик определяет понятия (отвечает на вопрос «Что»), а программист транслирует их в машинный язык (отвечает на вопрос «Как»).

Какие специалисты лучше подходят для математикоемкой разработки: математики с азами программирования или программисты с азами математики?

В общем среднем по больнице — конечно, программисты с азами математики.

Артем Кухаренко, основатель NTechLab:

Насколько нужна программисту математика?

Если здесь имеется ввиду знание математики, то, на мой взгляд, оно обязательно далеко не во всех областях программирования, но лишним оно, конечно, тоже не будет. Я бы сказал, что в разных областях оно даст свой прирост к квалификации: в каких-то – 10%, в каких-то – 1000%.

Если имеется ввиду знание теории и основ области в которой человек работает, то, на мой взгляд, это must have для любого эксперта в своей области.

Опишите, пожалуйста, свою историю отношений с матчастью.

Учился в математическом классе одной из лучших матшкол Москвы — Гимназия №1543, потом учился на ВМК МГУ, где тоже была математика, не такая серьезная, конечно, как на МЕХМАТе МГУ например, но на достаточном уровне, чтобы можно было разбираться и понимать, например, современные алгоритмы машинного обучения. Плюс участвовал в школьных олимпиадах по программированию, где нужно было изучать теорию алгоритмов, что в дальнейшем мне очень сильно помогло.

В каких направлениях разработки необходима матчасть? Почему? Какие разделы математики там нужны?

Точно могу сказать, что математическая и алгоритмическая подготовка нужна в областях, связанных с машинным обучением, нейронными сетями, искусственным интеллектом. Мы активно пользуемся знаниями из следующих разделов: математический анализ, линейная алгебра, теория вероятности, линейное программирование и решение оптимизационных задач, алгоритмы, высокопроизводительные вычисления.

Можете посоветовать, как подтянуть математический аппарат программистам, давно закончившим ВУЗ? Какие курсы лучше посещать?

Сейчас появилось много открытых курсов, таких как Coursera, но в них обычно материал дается очень поверхностно, чтобы охватить как можно более широкую аудиторию. Есть, конечно, и исключения, но их мало. Есть несколько ресурсов, где материал дается на очень хорошем уровне, например, Stanford engineering everywhere: там просто записи лекций, которые читаются в Стэнфорде. На мой взгляд, их очень полезно смотреть если есть базовая подготовка.

Но нужно понимать, что получение хороших знаний в любой области – это достаточно долгий процесс и с нуля быстро (за несколько месяцев) получить хорошую математическую (как и любую другую) подготовку не получится. Если все-таки есть цель заняться этим серьезно, то, на мой взгляд, для этого лучше подойдет либо магистратура, либо второе высшее образование в математическом вузе.

Какие специалисты лучше подходят для математикоемкой разработки: математики с азами программирования или программисты с азами математики?

У нас в компании разработка и исследования разделены. Для разработки больше подходят программисты с азами математики, для исследований — математики с азами программирования. Но в обоих командах очень часто встречаются люди, у которых одновременно очень высокий уровень знаний и математики и программирования.

Пользователь Mrrl, рассуждая о разделах математики, необходимых программистам, писал следующее:

1) Математический анализ — без него просто никуда, основа всех численных моделей.

2) Алгебра (высшая) — применяется довольно редко. Либо в виде теории групп — когда нужно что-нибудь сделать с группами вращений или движений пространства, либо в виде конечных групп/полей, где она смыкается с теорией чисел. Но если уж пришлось туда забрести, то приходится использовать активно. Если и не в коде, то в разработке алгоритмов.

3) Аналитическая геометрия — думаю, она нужна любому, кто связан с компьютерной графикой, компьютерной геометрией, моделированием в 3D…

4) Линейная алгебра и геометрия — аналогично аналитической геометрии. Плюс матрицы вылезают во многих задачах обработки информации.

5) Дискретная математика — графы сюда входят? А булева алгебра? А конечные автоматы? Для разработки алгоритмов будет использоваться часто, пусть и в фоновом режиме.

6) Математическая логика — разве что на уровне понимания логических операций и кванторов. Чтобы доказать правильность программ, и реже — чтобы их спроектировать исходя из «дано» и «получить». Может помочь, когда условия задачи слишком формальны и упорно не хотят восприниматься мозгом.

7) Дифференциальные уравнения — если они не являются частью предметной области, то встречаются редко. Чаще в качестве такого же вспомогательного инструмента, как производящие функции. Или для анализа данных, оптимизационных алгоритмов…

8) Дифференциальная геометрия. — Бывает. Когда приходится работать с многопараметрической моделью, полезно представлять себе свойства пространства параметров. Чаще всего это ограничивается метрикой — даже геодезические считать не приходится. Ну, и есть один специфический случай — программы, в которых дело идёт в пространстве Лобачевского.

9) Топология — кроме трассировки плат не могу представить, где она нужна. Возможно, в компьютерной геометрии, например, при построении поверхности по одному или нескольким облакам точек, при расчётах взаимодействия тел, для поиска пути в пространстве допустимых параметров какого-нибудь робота… Но я этим пока не занимался, и насколько нужна именно топология, не знаю. Для разработки алгоритмов, думаю, нужна.

10) Функциональный анализ — не помню, что туда входит. Но если базисы семейств функций (ряды Фурье и более сложные системы) изучаются там, то это полезно. Бесконечномерные пространства, скорее всего, не потребуются.

11) Интегральные уравнения — не сталкивался. Возможно, потому, что в качестве отдельного предмета я их не знаю.

12) Теория функций комплексного переменного — линейные и рациональные функции очень полезны для работы с движениями плоскости и сферы, с комплексными числами работать проще, чем с ортогональными матрицами. Ещё в комплексном поле удобно решать системы полиномиальных уравнений (они редко, но встречаются). И то же пространство Лобачевского в комплексных координатах выглядит приятнее.

13) Уравнения в частных производных — если не часть предметной области… могут пригодиться для каких-нибудь вариантов гладкой интерполяции данных (когда работы с базисными функциями почему-то не хватает). Насколько УрЧП нужны для моделирования, скажем, морской поверхности в компьютерной графике, не знаю — не занимался. Подозреваю, что нужны.

14) Теория вероятностей, математическая статистика, теория случайных процессов — в разной степени в любом анализе данных.

15) Вариационное исчисление и методы оптимизации — ИИ в играх и роботехника.

16) Методы вычислений и численные методы — сколько угодно. Если работа связана хоть с какими-нибудь вещественными числами.

17) Теория чисел — аналогично теории конечных групп. В целом, встречается нечасто. Если, конечно, не считать современной криптографии…

Источник

Математическая логика и языки программирования

Образно выражаясь, можно сказать, что компьютер состоит из материальной части и математического (программного) обеспечения, или, используя профессиональную лексику, из «железа» и «обуви». И к тому, и к другому имеет самое непосредственное отношение математическая логика, ни первое, ни второе без математической логики обойтись не могут. Ранее здесь и здесь было рассмотрено применение математической логики к релейно-контактным (переключательным) схемам, являющимся неотъемлемой составной частью современного компьютера. Часть настоящей главы также посвящена вопросам взаимодействия математической логики и компьютеров. Так, в этой статье рассказывается о применении математической логики к языкам программирования и к самому процессу программирования и получающимся в результате этого программам. В статье дается характеристика обратного процесса — применению компьютеров для поиска доказательств теорем математической логики и других математических дисциплин. Значительное внимание уделено методу резолюций для доказательства теорем в исчислениях высказываний и предикатов. В статье кратко описывается язык ПРОЛОГ — принципиально новый язык программирования, выросший непосредственно из математической логики (логики- предикатов) и призванный стать языком компьютеров пятого поколения.

В свою очередь, информатика как наука начала оформляться вместе с созданием и бурным развитием вычислительной техники. Ее формирование и определение ее предмета продолжаются по настоящее время. Информатика — наука о хранении, обработке и передаче информации с помощью компьютеров. Она включает в себя крупные разделы, изучающие алгоритмические, программные и технические средства хранения, обработки и передачи информации. Математическая логика оказалась единственной математической наукой, методы которой стали мощнейшими инструментами познания во всех разделах информатики. Поэтому сколько-нибудь серьезное изучение информатики немыслимо без освоения основ математической логики.

Вторая часть настоящего раздела посвящена тем вопросам математической логики, которые находят наиболее яркое применение в информатике, а также краткому показу того, как математическая логика работает в некоторых разделах информатики. Здесь будет рассказано о применении математической логики при исследованиях, посвященных базам данных, базам знаний и системам искусственного интеллекта.

Чтобы компьютер работал, он должен быть оснащен программным обеспечением, т.е. комплексом программ, ориентирующих компьютер на решение задач того или иного класса. (Слово «программа» имеет греческое происхождение и означает «объявление», «распоряжение».) Уже само понятие компьютерной программы, предусматривающее четкое алгоритмическое предписание компьютеру о порядке и характере действий, предусматривает проникновение в программу, а также в процесс ее составления (в программирование) теории алгоритмов. Но при более пристальном рассмотрении процесс проникновения логики в программы и программирование оказывается значительно более глубоким и органичным. Не только один ее раздел — теория алгоритмов — работает здесь, но исключительно действенным оказывается само существо математической логики — ее язык, ее аксиоматические теории, выводы и теоремы в них, свойства этих теорий.

В данном параграфе дается краткий обзор основных направлений, по которым математическая логика внедряется в программирование, из которых программирование возникло и без которых существовать не может.

Теория алгоритмов и математическая логика — фундаментальная основа программирования. В 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 естественно получаются в том случае, если все рассматриваемые действия можно считать глобальными преобразованиями состояния системы. Циклы оказались хорошо совместимы с массивами и плохо — с рекурсивными структурами данных, а процедуры высших типов — наоборот. Массивы и сложные структуры данных плохо совместимы с присваиваниями (в данном случае присваивание дается на целый ряд операторов, несущих различный логический смысл).

В общем, можно сделать вывод, что нет средств программирования хороших либо плохих самих по себе; хороши или плохи их комбинации. При этом любая логически разумная комбинация оказывается неуниверсальной, она приспособлена лишь для определенного класса задач.

Верификация (доказательство правильности) программ с помощью математической логики

Широчайшее использование компьютеров в самых разнообразных сферах человеческой деятельности выдвигает на одно из первых мест вопрос о надежности программного обеспечения компьютеров. Как известно, правильность созданной программы обычно проверяется на ряде так называемых тестовых примеров, на начальных данных, для которых результат известен или его можно предсказать. Нетрудно понять, что такая проверка способна лишь выявить наличие ошибок в программе, но не доказать их отсутствие, что, разумеется, не одно и то же.

Поэтому исключительно важна задача строгого доказательства правильности программ, и именно для этой цели и начали разрабатываться программные и динамические логики.

С интуиционистской точки зрения программа будет правильной, если в результате ее выполнения будет достигнут тот результат, с целью получения которого и была написана программа. (Обратите внимание, что мы не рассматриваем программы, содержащие синтаксические ошибки, т. е. предполагаем, что с точки зрения языка программирования программа написана безупречно.) Доказательство правильности программы состоит в предъявлении такой цепочки аргументов, которые убедительно свидетельствуют о том, что это действительно так, т.е. что программа на самом деле решает поставленную задачу.

Говорить о правильности программы самой по себе бессмысленно. Программа пишется с целью решения той или иной конкретной задачи. Каждая правильно поставленная задача содержит в себе условие (то, что дано) и вопрос, на который нужно дать ответ. При составлении программы условие задачи превращается в предусловие, а вопрос преобразуется в постусловие, имеющее уже форму не вопроса, а утверждения, которое должно быть истинно всякий раз, когда ответ на вопрос задачи правилен.

Из определений следует, что всякая тотально правильная программа является частично правильной при тех же пред- и постусловиях. Обратное конечно же неверно. Ясно, что тотальная правильность «лучше» частичной, хотя доказать тотальную правильность программы, по-видимому, сложнее, чем частичную.

Для доказательства частичной правильности операторных программ обычно используются различные модификации метода Флойда, который состоит в следующем. На схеме программы выбираются контрольные точки так, чтобы любой циклический путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется специальное условие (индуктивное утверждение или инвариант цикла), которое истинно при каждом переходе через эту точку. С входом и выходом схемы также ассоциируются пред- и постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется так называемое условие правильности. Выполнимость всех условий правильности гарантирует частичную правильность программы.

Один из способов доказательства завершения работы программы состоит во введении в программу дополнительных счетчиков для каждого цикла и в доказательстве их ограниченности в процессе доказательства частичной правильности программы.

Одна из модификаций метода Флойда заключается в построении конечной аксиоматической системы (так называемой «логики Хоара»), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ, в частности на языке программирования Паскаль. Такая система используется и для задания аксиоматической семантики языка Паскаль. Аксиоматические системы, родственные логике Хоара, разработаны и для других алгоритмических языков программирования.

Для доказательства правильности рекурсивных программ используется метод математической индукции, связанный с определением наименьшей неподвижной точки, а для программ со сложными структурами данных (например, графами, деревьями) — индукция по структуре данных. При этом в теоретических исследованиях по логике Хоара рассматриваются обычные свойства аксиоматизаций в логике — их непротиворечивость и полнота.

б) после завершения цикла;

в) в ходе выполнения цикла.

В заключение отметим, что исследования по логическому описанию программ и программирования убедительно показали, что логический анализ позволяет анализировать концепции языков программирования и находить многие скрытые недоработки в этих концепциях. Пожалуй, до сих пор это применение строгих математических методов в качестве инструмента критики концепций (зачастую совершенно не продуманных, вставляемых ради «усиления» языков программирования) является важнейшим применением математической логики в области программирования.

Источник