Применение логики в информатике

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

Методы математической логики являются инструментом познания во всех разделах информатики.

Описание компьютерных программ в логике

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

B. М. Глушков в 1965 г. определил алгоритмическую алгебру, послужившую прообразом алгоритмических логик.

Ф. Энгелер в 1967 г. предложил использовать языки с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при разных исполнениях программы. Популярность приобрели языки алгоритмических логик. Языки были предложены практически одновременно американскими логиками Р. У. Флойдом (1967),.

C. А. Р. Хоаром (1969) и учеными польской логической школы А. Сальвицким и др. (1970)^[1].

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

В логике предикатов записываются утверждения {А}5{В}, где исполнению оператора S предшествует определение предусловия — исходного состояния программы А, а В — состояние-постусловие. Предусловия А являются аксиомами логической системы и определяются конструкциями языка программирования. Синтезируемая программа получается в форме выводимого в динамической логике утверждения, где результат выполнения программы удовлетворяет заданному постусловию, если аргументы задачи удовлетворяют заданному предусловию.

Один из фундаментальных законов классической логики — закон исключенного третьего, формулирующийся как закон дополнения (Р viР) =.

= Т или, и эквивалентной формулировке, как закон двойного отрицания —?(—IР) = Р с общим смыслом — истинны могут быть только высказывание Р либо инверсное высказываниеiР. Законы отрицают существование третьего или другого истинного решения и ограничивают возможности языка для определения процесса конструирования алгоритма. Э. Я. Брауэр предлагает интуиционистскую логику, не принимающую закон исключенного третьего как универсальный.

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

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

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

Например, формула А & В понимается как задача, состоящая в том, чтобы сформулировать решение задачи, А и найти решение задачи В. Правило вывода {А, В} —" Л & В интерпретируется как преобразование, строящее из объекта а, решающего задачу А, и объекта Ь, решающего задачу В, пару (а, Ь), решающую задачу, А & В. Конструктивная импликация, А —" В понимается как требование построить эффективное преобразование /, применимое ко всем реализациям формулы, А и переводящее их в реализации формулы В.

А. А. Воронков в 1985 г. определил условия, при которых классическая логика может рассматриваться как конструктивная. В частности, необходимым условием является ее полнота, т. е. выводимость в логике либо самой формулы F, либо ее отрицания —iF. Примерами классических теорий, имеющих конструктивное истолкование, служат элементарная геометрия и алгебраическая теория вещественных чисел.

Полная система конструктивных правил вывода (логика Q,) позволяет построить доказательство преобразования, А в В на базе заданных функций:

А —> В, С —" D.

—правило условного оператора (ПУО);

AvC —>Bv F)

A^B, B^C, C^D

—правило релаксации (IIP):

А-> D

AvC-«BvC.

—правило зацикливания (ИЗ);

А—> В

А—> А

• —правило бесконечного цикла (ПБЦ);
• —iА
• ———правило ошибки (ПО).

А —^ А В ПУО предикаты Л и В подтверждают (охраняют) правильное исполнение условного оператора, в ПЗ С — инвариант создаваемого цикла, В — условие его завершения. ПБЦ утверждает, что цикл не может быть бесконечным.

Интуиционистская логика сохранила язык исчисления предикатов и логические связки классической логики.

• [1] Игошин В. И. Математическая логика и теория алгоритмов: учеб, пособие для студентов вузов. 2-е изд., стер. М.: Академия, 2008.