Сборник работ зарубежных специалистов, отражающий новые результаты в теоретическом и практическом программировании на основе применения идей и методов математической логики. В него включены статьи по функциональному программированию, лямбда-исчислению, автоматическому поиску логического вывода, методам работы с равенствами. Среди авторов статей — известные специалисты: Дж. Бэкус, Д. Оппен, Д. Скотт (США), Дж. Р. Хиндли, С. Л. Пейтон Джоунз (Англия).

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

Чтобы представить себе, хотя бы в самых общих чертах, те направления, в которых развивается современная вычислительная наука, полезно взглянуть на названия сборников широко известной серии Lecture Notes in Computer Science, выпускаемой западногерманским издательством Springer-Verlag и содержащей материалы многих международных конференций по информатике. И тогда перед нами предстанет довольно любопытная картина: наряду с такими близкими программисту названиями, как «Параллельные алгоритмы и архитектуры» или «Программы как объекты данных», чуть ли не на каждой пятой обложке можно увидеть термины «логический вывод», «логическое программирование», «компьютерная логика», «логики программ» и т. д. Математическая логика, возникшая почти 100 лет назад в связи с внутренними потребностями математики, нашла применение в теоретическом (и практическом) программировании, и, судя по всему, взаимодействие этих двух наук в недалёком будущем сможет принести новые плоды.

Причины, по которым программисты обратились к математической логике, а логики заинтересовались программированием, имеют довольно глубокие корни. Следует, наверное, вспомнить, что математическая логика занимается построением формальных языков, предназначенных для представления таких фундаментальных понятий, как функция, отношение, аксиома, доказательство, и изучением основанных на этих языках логических и логико-математических исчислений. Именно в недрах математической логики были найдены математически точные понятия алгоритма и вычислимой функции, развита семантика формальных языков и теорий, построены системы логического вывода — и всё это, заметим, было сделано в 30—40-х годах, т. е. ещё в «докомпьютерную эру».

Программирование также имеет дело с формальными языками — языками программирования, являющимися средствами общения человека и компьютера. В своём стремлении сделать эти средства удобными и естественными для человека вычислительная наука не могла пройти мимо тех языков описания вычислимых функций и отношений, которые были созданы в рамках математической логики с учётом многовекового математического опыта. В результате появились принципиально новые языки функционального и логического программирования: Лисп, Рефал, ML, Миранда, Пролог и другие — особенно активно разрабатываемые в последнее десятилетие. С другой стороны, языки высокого уровня нуждаются в детально проработанной семантике, которая выходит на первый план при написании трансляторов. И здесь идеи и аппарат математической логики, уже занимавшейся проблемами семантики, оказались весьма кстати. Поначалу для формализации смысла программ использовалось известное логикам ещё с 30-х годов бестиповое лямбда-исчисление А. Чёрча, а затем абстрактным базисом денотационной семантики стала мощная и элегантная теория областей, развитая Д. Скоттом. Важное значение приобретает теория логического вывода, причём не только в задачах искусственного интеллекта, но и как средство рассуждения о программах и доказательства их свойств (скажем, правильности относительно спецификации) или, наоборот, как метод построения правильных программ (например, путём их извлечения из конструктивных дoкaзaтeльcтв).

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

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

Функциональное программирование, точнее, два его различных течения представлены статьями Дж. Бэкуса и С. Л. Пейтона Джоунза. Краткое введение в круг основных идей и понятий лямбда-исчисления и комбинаторной логики, написанное Дж. Р. Хиндли, поможет читателю глубже понять эти и другие статьи сборника. Работа Дж. Бэкуса является продолжением и развитием знаменитой лекции «Можно ли избавить программирование от фон-неймановского стиля? Функциональный стиль и его алгебра программ», прочитанной Бэкусом в 1977 году при вручении ему Тьюринговской премии. Хотя русский перевод этой лекции войдёт в книгу «Лекции лауреатов премии Тьюринга» (М.: Мир, план.), переводчик для удобства читателей написал к статье Бэкуса небольшое дополнение, в котором коротко изложил наиболее важные идеи упомянутой лекции. Логическое программирование представлено в сборнике статьёй Д. Миллера и статьёй Дж. А. Гогена и Ж. Мезегера. Методам обращения с отношением равенства, играющим важную роль как в функциональном и логическом программировании, так и в более общем контексте автоматического доказательства теорем, посвящён обзор Ж. Юэ и Д. Оппена. В статье К. А. Гоуда обсуждается проблема извлечения программ из доказательств. Читателя, конечно же, заинтересует и прекрасно написанная статья Д. Скотта, в которой впервые в столь доступной форме излагается созданная им теория областей. Завершает сборник обзорная статья советских авторов, посвящённая тем приложениям математической логики, которые уже нашли практическое воплощение в языках программирования и методах разработки программного обеспечения…

ПРЕДИСЛОВИЕ РЕДАКТОРОВ ПЕРЕВОДА
М. В. Захарьящев,
Ю. И. Янов

Книги на ту же тему

1. Заметки по логике, Линдон Р., 1968
2. Введение в математическую логику, Колмогоров А. Н., Драгалин А. Г., 1982
3. Логический подход к искусственному интеллекту: от классической логики к логическому программированию, Тей А., Грибомон П., Луи Ж., Снийерс Д., Водон П., Гоше П., Грегуар Э., Санчес Э., Дельсарт Ф., 1990
4. Математическая логика, Клини С. К., 1973
5. Логические основы цифровой вычислительной техники. Учебное пособие для вузов. — 3-е изд., перераб. и доп., Папернов А. А., 1972
6. Логическая семантика и модальная логика, Таванец П. В., ред., 1967
7. Задачи по теории множеств, математической логике и теории алгоритмов, Лавров И. А., Максимова Л. Л., 1975
8. Моделирование семантики в базах данных, Цаленко М. Ш., 1989
9. Теория алгоритмов: основные открытия и приложения, Успенский В. А., Семёнов А. Л., 1987
10. Введение в теорию моделей и метаматематику алгебры, Робинсон А., 1967
11. Методы распознавания: Учебное пособие для вузов. — 3-е изд., перераб. и доп., Горелик А. Л., Скрипкин В. А., 1989
12. Теоретико-множественные модели языков, Маркус С., 1970
13. Математическая лингвистика, Шаумян С. К., ред., 1973
14. Языки программирования. Концепции и принципы, Кауфман B. Ш., 1993
15. Универсальные языки программирования. Семантический подход, Калинин А. Г., Мацкевич И. В., 1991
16. Сравнительное изучение языков программирования, Хигман Б., 1974
17. Программирование и алгоритмические языки, Криницкий Н. А., Миронов Г. А., Фролов Г. Д., 1975
18. Элементы программирования, Гнеденко Б. В., Королюк В. С., Ющенко Е. Л., 1961
19. Языки программирования. Практический сравнительный анализ, Бен-Ари М., 2000
20. Язык Ассемблера для IBM PC и программирования, Абель П., 1992
21. Объектно-ориентированное программирование в C++. — 4-е изд., Лафоре Р., 2003
22. Программирование на C++ в Linux, Секунов Н. Ю., 2003
23. Разработка приложений на C++ и С#. Библиотека программиста, Секунов Н. Ю., 2003
24. Язык программирования Си для персонального компьютера, Бочков C. O., Субботин Д. М., 1990
25. Мультипарадигменное проектирование для C++, Коплиен Д., 2005
26. C++ Boost Graph Library, Сик Д., Ли Л., Ламсдэйн Э., 2006
27. Профессиональное PHP программирование, 2-е издание, 2003
28. PHP. Справочник, Хадсон П., 2006
29. PHP. Сборник рецептов, Скляр Д., Трахтенберг А., 2005
30. Perl: изучаем глубже. — 2-е изд., Шварц Р. Л., Фой Б., Феникс Т., 2007
31. Perl для системного администрирования, Бланк-Эдельман Д. Н., 2001
32. Perl & XML. Библиотека программиста, Макинтош Д., Рэй Э. Т., 2003
33. CGI/Perl: Создание программ для Web, Пэтчетт К., Райт М., 1999
34. Perl 6 и Parrot: справочник. — 2-е изд., Рэндал Э., Сугальски Д., Тёч Л., 2005
35. Perl-отладчик. Карманный справочник, Фоули Р., 2005
36. Программирование на современных алгоритмических языках: Учебное пособие для втузов.— 3-е изд., перераб. и доп., Пярнпуу А. А., 1990
37. Язык программирования Эль-76. Принципы построения языка и руководство к пользованию. — 2-е изд. испр. и доп., Пентковский В. М., 1989