Логика в компьютерных науках

Логика в информатике — это направления исследований и отрасли знания, где логика применяется в информатике и искусственном интеллекте. Логика оказалась гораздо более эффективной в информатике, чем это было в математике^[1].

Включаются следующие основные применения:

• исследования в логике, вызванные развитием компьютерных наук. Например, аппликативные вычислительные системы, теория вычислений и модели вычислений;

• формальные методы и логика рассуждения о понятиях. Например, семантическая сеть^[2], семантическая Web;

• булева логика и алгебра для разработки аппаратного обеспечения компьютеров;

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

• доказательное программирование - технология разработки алгоритмов и программ с доказательствами правильности алгоритмов;

• фундаментальные понятия и представления для компьютерных наук, которые являются естественной областью для формальной логики. Например, семантика языков программирования^[3];

• логика знания и предположения. Например, искусственный интеллект;

• Язык Пролог и логическое программирование для создания баз знаний и экспертных систем и исследований в сфере искусственного интеллекта;

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

• логика для описания пространственного положения и перемещения;

• логика в информационных технологиях. Например, реляционная модель данных. реляционные СУБД, реляционная алгебра, реляционное исчисление^[4];

• логика вычислений с объектами. Например, комбинаторная логика, суперкомбинаторы^[5];

• логика для компилирования программного кода и его оптимизации. Например, категориальная абстрактная машина;

• логика для эквивалентного преобразования объектов. Например, λ-исчисление;

• переизложение логики и математики в терминах, понятных специалистам в компьютинге и компьютерных науках^[6].

Этот список продолжает пополняться.

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

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

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

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

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

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

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

Практика применения и изучения доказательных методов программирования показала, что эта технология вполне доступна студентам математических факультетов, которым вполне по силам написание доказательств правильности алгоритмов, после проверки и тестирования программ на ЭВМ.

Наибольший эффект в освоении технологий доказательного программирования наблюдается в олимпиадах по информатике и программированию, где победителями и призерами становятся те студенты, которые освоили технику тестирования программ на ЭВМ и составления алгоритмов и программ без ошибок.

См. также

• Комбинаторная логика
• программирование
• парадигма програмирования
• структурное программирование
• логическое программирование
• информатика
• решение задач
• тестирование программ
• доказательное программирование

Примечания

1. ↑ Halpern J.Y., Harper R., Immerman N., Kolaitis Ph.G., Vardi M.Y., and Vianu V. On the unususal effectiveness of logic in computer science. — January, 2001.
2. ↑ Roussopoulos N.D. A semantic network model of data bases. — TR No 104, Department of Computer Science, University of Toronto, 1976.
3. ↑ Scott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp.~311-372.
4. ↑ Codd E. F. Relational Completeness of Data Base Sublanguages. In: R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972.
5. ↑ Peyton Jones S., Eber J.-M., Seward J. Composing contracts: an adventure in financial engineering. — ICFP 2000
6. ↑ Asperti A, and Longo G. Categories, Types and Structures. Category Theory for the working computer scientist. — M.I.T. Press, 1991 (pp. 1-300)

Литература

• Вольфенгаген В. Э. Логика. Конспект лекций: техника рассуждений. 2-е изд., дополн. и перераб. — М: АО «Центр ЮрИнфоР», 2004. — 229 с ISBN 5-89158-135-3.