Введение к работе
Актуальность темы. В диссертационной работе исследуются функциональные и логические языки программирования, являющиеся инструментом создания современных интеллектуальных систем. А если точнее, то функциональный и логический взгляды на языки программирования, согласно которым семантика не связывается с процессом выполнения программы, а является ее функциональной, соответственно логической сущностью.
Начнем с функциональных языков программирования. Функциональная программа представляет собой систему рекурсивных уравнений. Семантика — главная функция ее наименьшего решения. Пионерами в области формализации функциональной (денатационной) семантики алгоритмических языков являются Д. Скотт и К.Стрейчи. Для этой цели они использовали бестиповое Д-исчисление, полные множества и непрерывные (в топологии Скотта) отображения. Наш подход основан на типовом Я-исчислении, полных множествах и монотонных отображениях. Что является характерным для нашего подхода? Типовые Л-термы являются на наш взгляд более удобной конструкцией при определении реального алгоритмического языка. Любой типовой Л-терм имеет нормальную форму, и типовое Л-исчисление является сильно нормализуемой теорией, то есть любая /^-редукция типового Я-терма заканчивается. Однако существенной сложностью на нашем пути является отсутствие теоремы о неподвижной точке в случае типового Я-исчисления и, естественно, ни о каком операторе неподвижной точки не может быть и речи. Это та трудность, которую необходимо преодолеть в конкретных моделях Л-исчисле-ния. Не требуя непрерывности рассматриваемых отображений, мы с одной стороны усложняем нашу задачу, с другой — расширяем границы рассматриваемых языков, так как мы теперь можем рассматривать языки, использующие монотонные, но не непрерывные константы. К монотонным, но не непрерывным константам относятся и функционалы, которые соответствуют таким важным свойствам программ, как: тотальность, бесконечность области определения и т. д.
Перейдем к логическим языкам программирования. Логическая программа представляет собой выполнимую формулу некоторой логики. Семантика логической программы определяется множеством пар [запрос, ответ), где запрос является формулой из
некоторого (допустимого) множества запросов, а ответ зависит от запроса и является положительным, если запрос логически следует из программы и отрицательным — в противном случае. Очевидно, что не для всякого логического языка программирования существует такой интерпретатор, который бы отвечал на все запросы из допустимого множества запросов (следствие теоремы АЧерча). Однако всякий интерпретатор логического языка программирования обязан быть логически корректным, то есть, если он останавливается с положительным ответом, то запрос логически следует из программы, если же — с отрицательным ответом, то — нет. Логическая (пропозициональная) семантика языков программирования исследовалась в работах Р.Флойда, З.Манны, С.Хоара, которые использовали формализацию логической семантики процедурных программ для доказательства их правильности. Суть логических языков программирования состоит в том, что для них исходной является логическая семантика. Конкретная реализация логического языка программирования задает его некоторую процедурную семантику, которая обязана быть согласована с логической. Чрезвычайно важной задачей является проверка процедурной семантики логического языка программирования (семантики его реализации) на логическую непротиворечивость, иными словами, проверка интерпретатора логического языка программирования на логическую корректность. Другой важной задачей является расширение области определения интерпретатора, т.е. расширение того множества запросов, на которые интерпретатор даст определенный ответ.
Цель диссертационной работы. Целью диссертационной работы является создание соответствующего формализма и на его основе теории, позволяющей определять и исследовать широкий класс языков, используемых для создания современных интеллектуальных систем. Функциональная и логическая направленность теории должны обеспечить возможность дать точные математические определения функционального и соответственно логического языков программирования. Теория должна позволять, не осуществляя никаких сложных трансляций, определять язык программирования и его семантику с функциональной, соответственно с логической точек зрения. При этом текст программы рассматриваемогс языка программирования, представленный в виде системы рекурсивных уравнений, соответственно в виде логической формулы, был бы легко узнаваем и восстановить его не представляло бы никакого труда. На основании созданной теории должны бьіті
поставлены и решены задачи, касающиеся интерпретации языков реальных систем программирования.
Научная новизна. Впервые построена математическая теория языков программирования, отвечающая поставленной в предыдущем пункте цели. Создана функциональная концепция языков программирования, основанная на типовом Л-исчислении, полных множествах и монотонных отображениях. Используя единый математический аппарат, определена логическая концепция языков программирования, включающая функциональный подход. Поставлена задача об интерпретации и преобразованиях логических программ. В рамках этой концепции исследован язык ПРОЛОГ, использующий любые встроенные предикаты. Разработаны основания хорновского программирования со встроенными предикатами и метод резолюций для логики предикатов первого порядка со встроенными предикатами.
Практическая ценность. Исследования, проводимые в диссертационной работе, носят теоретический характер и имеют явно выраженную практическую ориентацию. Результаты диссертации могут быть использованы при создании новых интеллектуальных систем, а также для обоснования логической корректности и расширения "интеллектуальных способностей" уже существующих.
Методика исследований. Методика исследований включает в себя методы алгебры, математической логики, теории алгоритмов, а также методы, разработанные в самой диссертационной работе, такие, как: методы интерпретации функциональных программ с константами и переменными монотонных типов, представляющие собой способы вычисления главной функции наименьшего решения соответствующих систем рекурсивных уравнений; методы интерпретации логических программ со встроенными предикатами, основанные на предложенных для этой цели правилах вывода; методы расширения области определения интерпретаторов посредством преобразований логических программ.
Апробация работы и публикации. Основные результаты работы докладывались на научных конференциях и семинарах, в частности на научных конференциях Ереванского госуниверситета (1987-1996), на научных конференциях Армянского математического общества (июль 1996, декабрь 1996), на конференции "Sixth Conference of Program Designers" (Будапешт, 1990), на международной конференции "Conference on Computer Science and Information Technologies (CSIT-97)" (Ереван, 1997), на семинаре по теоретическому программированию Ереванского госуниверситета,
6 на общем семинаре Института проблем информатики и автоматизации НАН Армении, на семинаре департамента Computer Science Будапештского университета, на семинаре по теории автоматов и автоматизации программирования Института кибернетики АН Украины, на семинаре в ИПМ РАН, на семинаре по теоретическим вопросам программирования кафедры Математической кибернетики МГУ, на объединенном научно-исследовательском семинаре кафедр Автоматизации систем вычислительных комплексов, Алгоритмических языков и Системного программирования МГУ.
Основные результаты работы отражены в 13 публикациях.
Структура и объем работы. Диссертация состоит из введения, шести глав, заключения и списка цитируемой литературы (83 наименования). Объем работы — 161 стр.
