автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Функциональные и логические языки программирования

..»Л,"'*

ЖУКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ им. М.В.ЛОМОНОСОВА Л Факультет вычислительной математики и кибернетики

На правах рукописи

НИГИЯН Семен Александрович

ФУНКЦИОНАЛЬНЫЕ И ЛОГИЧЕСКИЕ ЯЗЫКИ ПРОГРАММИРОВАНИЯ (ФОРМАЛИЗАЦИЯ, АНАЛИЗ, ИНТЕРПРЕТАЦИЯ) .

Специальность 05.13.11 -математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора физико-математических наук

Москва - 1997

Работа выполнена на кафедре Алгоритмических языков Ереванского государственного университета

Официальные оппоненты:

член-корреспондент УАН, доктор физико-математических наук, профессор ЛЕТИЧЕВСКИЙ Александр Адольфович

доктор физико-математических наук, профессор ЛЮБИМСКИЙ Эдуард Зиновьевич

доктор физико-математических наук, профессор ТУЗОВ Виталий Алексеевич

Ведущая организация: Институт систем информатики СО РАН им. А.П. Ершова

Защита диссертации состоится ок?А(УрА 1997 года в 11 часов на заседании Диссертационного совета Д 053705.38 при Московском государственном университете им. М.В.Ломоносова по адресу: 119899, ГСП, Воробьевы горы, МГУ, факультет ВМиК, аудитория 685.

С диссертацией можно ознакомиться в библиотеке факультета Вычислительной математики и кибернетики МГУ.

Автореферат разослан сен1997 года

Ученый секретарь Диссертационного совета,

профессор

Н.П.ТРИФОНОВ

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Начнем с функциональных языков программирования. Функциональная программа представляет собой систему рекурсивных уравнений. Семантика — главная функция ее наименьшего решения. Пионерами в области формализации функциональной (денатационной) семантики алгоритмических языков являются Д.Скотг и К.Стрейчи. Для этой цели они использовали бестиповое ^-исчисление, полные множества и непрерывные (в топологии Скотта) отображения. Наш подход основан на типовом Я-исчислении, полных множествах и монотонных отображениях. Что является характерным для нашего подхода? Типовые Л-термы являются на наш взгляд более удобной конструкцией при определении реального алгоритмического языка. Любой типовой Л-терм имеет нормальную форму, и типовое Л-исчисление является сильно нормализуемой теорией, то есть любая /^-редукция типового Я-терма заканчивается. Однако существенной сложностью на нашем пути является отсутствие теоремы о неподвижной точке в случае типового Я-исчисления и, естественно, ни о каком операторе неподвижной точки не может быть и речи. Это та трудность, которую необходимо преодолеть в конкретных моделях Я-исчисле-ния. Не требуя непрерывности рассматриваемых отображений, мы с одной стороны усложняем нашу задачу, с другой — расширяем границы рассматриваемых языков, так как мы теперь можем рассматривать языки, использующие монотонные, но не непрерывные константы. К монотонным, но не непрерывным константам относятся и функционалы, которые соответствуют таким важным свойствам программ, как: тотальность, бесконечность области определения и т. д.

Перейдем к логическим языкам программирования. Логическая программа представляет собой выполнимую формулу некоторой логики. Семантика логической программы определяется множеством пар (запрос, ответ), где запрос является формулой из

некоторого (допустимого) множества запросов, а ответ зависит от запроса и является положительным, если запрос логически следует из программы и отрицательным — в противном случае. Очевидно, что не для всякого логического языка программирования существует такой интерпретатор, который бы отвечал на все запросы из допустимого множества запросов (следствие теоремы А.Черча). Однако всякий интерпретатор логического языка программирования обязан быть логически корректным, то есть, если он останавливается с положительным ответом, то запрос логически следует из программы, если же — с отрицательным ответом, то — нет. Логическая (пропозициональная) семантика языков программирования исследовалась в работах Р.Флойда, З.Манны, С.Хоара, которые использовали формализацию логической семантики процедурных программ для доказательства их правильности. Суть логических языков программирования состоит в том, что для них исходной является логическая семантика. Конкретная реализация логического языка программирования задает его некоторую процедурную семантику, которая обязана быть согласована с логической. Чрезвычайно важной задачей является проверка процедурной семантики логического языка программирования (семантики его реализации) на логическую непротиворечивость, иными словами, проверка интерпретатора логического языка программирования на логическую корректность. Другой важной задачей является расширение области определения интерпретатора, т.е. расширение того множества запросов, на которые интерпретатор даст определенный ответ.

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

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

Научная новизна. Впервые построена математическая теория языков программирования, отвечающая поставленной в предыдущем пункте цели. Создана функциональная концепция языков программирования, основанная на типовом ¿-исчислении, полных множествах и монотонных отображениях. Используя единый математический аппарат, определена логическая концепция языков программирования, включающая функциональный подход. Поставлена задача об интерпретации и преобразованиях логических программ. В рамках этой концепции исследован язык ПРОЛОГ, использующий любые встроенные предикаты. Разработаны основания хорновского программирования со встроенными предикатами и метод резолюций для логики предикатов первого порядка со встроенными предикатами.

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

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

Апробация работы и публикации. Основные результаты работы докладывались на научных конференциях и семинарах, в частности на научных конференциях Ереванского госуниверситета (1987-1996), на научных конференциях Армянского математического общества (июль 1996, декабрь 1996), на конференции "Sixth Conference of Program Designers" (Будапешт, 1990), на международной конференции "Conference on Computer Science and Information Technologies (CSIT-97)" (Ереван, 1997), на семинаре по теоретическому программированию Ереванского госуниверситета,

на общем семинаре Института проблем информатики и автоматизации HAH Армении, на семинаре департамента Computer Science Будапештского университета, на семинаре по теории автоматов и автоматизации программирования Института кибернетики АН Украины, на семинаре в ИПМ РАН, на семинаре по теоретическим вопросам программирования кафедры Математической кибернетики МГУ, на объединенном научно-исследовательском семинаре кафедр Автоматизации систем вычислительных комплексов, Алгоритмических языков и Системного программирования МГУ.

Основные результаты работы отражены в 13 публикациях.

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

СОДЕРЖАНИЕ РАБОТЫ

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

Функциональной концепции языков программирования посвящены первые две главы диссертации.

В ГЛАВЕ 1 приводятся начальные понятия и утверждения, определяется необходимый формализм, доказывается семантическая Теорема 1.2.1. Основываясь на этой теореме, дается определение функционального языка программирования. Приведенная концепция иллюстрируется на конкретных алгоритмических языках. Глава 1 состоит из трех разделов 1.1-1.3.

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

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

Отображение /:А-т>В назовем монотонным, если для любых х,уеА имеем: если х<у, то f(x)-<f(y) (■< — символ частичного порядка). Если f:A—>A и f(a)=a, где аеА, то элемент а назовем неподвижной точкой отображения f.

Пусть А — полное множество, i:A->A — монотонное отображение и 0А — множество ординалов, отвечающих мощностям, не превосходящим мощность множества А. Определим отображение

y¡:0A->A следующим образом: yf(0)=l, где 1 — наименьший элемент множества А; если и <%=т]+1 для некоторого r¡eOA, то

yi(^)=f(r¡(T})); если £,£<9^ 4>0 и не существует такого TjeO^ что

4=r¡+l, то y,(Z)=sup{ri(k) /к<£}.

Лемма 1.1.1 (о неподвижной точке монотонного отображения). Пусть А — полное множество и I: А—>А ■— монотонное отображение. Тогда существует наименьшая неподвижная точка а отображения /, причем a=sup{y,(k) ¡keOA }.

Справедливость леммы следует из работы Я.Московакиса1. В разделе 1.2 вводятся понятия типа, монотонного типа, терма. Доказывается Теорема 1.2.1 о существовании наименьшего решения монотонной системы уравнений. Дается определение функционального языка программирования.

Зафиксируем непустое ч.у.м. М. Введем понятие типа.

1. Множество М есть тип.

2. Любое непустое подмножество типа есть тип.

3. Если P,a¡,...,av (к>0)— типы, то множество всех отображений из а,х...хак в ¡5 (обозначим {а,х...хак->/3}) есть тип.

4. Других типов, кроме определенных согласно 1-3, нет. Каждому типу а сопоставим натуральное число ord(a),

называемое его порядком. Если асМ, го ord(a)=0, если же ac{a¡x...xak->/3}, где р,а,,...,ак (к>0) — типы, то ord(a)=max(ord(a,),...,ord(ak),ord(P))+l. Если х — переменная типа а, cea и ord(a)=n>0, то х — переменная порядка п (ord(x)=n), ас — константа порядка п (ord(c)-nj.

Пусть С — множество констант некоторых ' типов, X — множество переменных некоторых типов. Определим множество термов Т(С,Х). Каждому терму t сопоставим:

• множество переменных, от которых t зависит — Var(t);

• тип терма t — Type(t);

• если Var(tjcrfy¡,...,yj, n>0, y0=<y°,..., y°n >, где y° ea„ a¡

— тип переменной y„ то терму t сопоставим константу Val?o (t),

i=l,...,n.

Определение терма:

1. Если сеС, то сеТ(С,Х), Var(c¡=0, Val- (с)=с, Туре(с)={с}.

1 Moschovakis Y.N. On the basic notions in the theory of induction.// Logic, Foundations of Mathematics, and Computability Theory. Butts and Hintikka (eds.), Reidel, 1977, p.207-236.

2. Если хеХ, то хеТ(С,Х), Vai(x)={x}, Val^ (х)=у°, если х=у,

(1<1<п), Туре(х)—а, где а—тип переменной х.

3. Пусть f,t„...,tkeT(C,X), к>0, Да„...,ак — типы, такие, что Type(zjc{a,x...хак->р}, Type (t,j era,, i=l,...,k, тогда T(t„...,tk)eT(C,X) и, если t=r(ti,...,tj, то

Var( t j— Var( r) uVar( t,)u... UVar(tk), Val?o (t)=VaIJo (r)(Val?o (t,),..., Valft (tk)j,

Type(tMVal<y„ л> (t)/у- eType(Yi), i=l,...,n}.

4. Пусть теТ(С,Х), xxkeX, k>0 и, если то x^j (l<i,j<k), тогда lx,,...,xk[z]eT(C,X) и, если t~Ax, ,...рск[т], то

Var(t)=Vai( t)\{xi,...^J,

Val-o (t) e{Type(x,jx... хТуре(хк)->Туре(т)}

и, если Vai(t)~{yfj,..., yim}, 0<m.<n, y'0 =<y",...,y? >, то для всяких x°j eType(Xj), Val-Jt)(x0)=Val-4-y.(T), где х0=<х° ,...,xl>,

Type(t) определяется так же, как в п.З;

5. Никаких других термов, кроме определенных согласно 1-4,

нет.

Рассмотрим систему уравнений

F, = г,

• ••• (1)

Л = ?п>

где F] еХ и, если Щ, то Ft*Fp Vj£T(C,Xj, Typef iJczTypefFJ, Var(T,)c{Fh...,FJ, i,j=l,...,n, n>l.

Отображение <p:TYpe(Fl)x...xType(Fn)—>Type(F,)x...xType(F„j такое, что (p(g)=<Val-(Tl),...,Val-(zn)>, где g eType(F,)x... xTypefFJ, назовем отображением, соответствующим системе уравнений (1): через (д), условимся обозначать i'-ую компоненту вектора д i~l,...,n. Будем говорить, что f&Type(F,)x...xType(FJ есть решение системы (1), если q>(f)=f.

Пусть М — ч.у.м., содержащее наименьший элемент 1 v. каждый элемент из М сравним только с 1 и с самим собой Введем понятие монотонного типа.

1. Множество М есть монотонный тип.

2. Если Р,а,,...,ак (к>0) — монотонные типы, то множество всех монотонных отображений из а,х...хак в ¡3 (обозначим [а,х...хак-*Д']) есть монотонный тип.

3. Других монотонных типов, кроме определенных согласно 1-2, нет.

Лемма 1.2.1. Всякий монотонный тип является полным множеством.

Константы и переменные монотонных типов условимся называть монотонными; термы, использующие только монотонные константы и переменные, — монотонными термами; системы уравнений (1), использующие только монотонные константы и переменные, — монотонными системами уравнений.

Теорема 1.2.1 (о наименьшем решении монотонной системы уравнений). Всякая монотонная система уравнений (1) имеет наименьшее решение /:

1 =зир{у^(к)/кеа/1}, где <р — отображение соответствующее системе уравнений (1), с/£= Тур е(Р!)х... хТур е(Рл).

Функциональный язык Ь определяется заданием четверки множеств М, С, X, Т, где М — ч.у.м., содержащее неопределенный элемент Д, который является наименьшим элементом множества М, и каждый элемент из М сравним только с _/. и с самим собой; С — некоторое множество монотонных констант; X — некоторое множество монотонных переменных; ТсТ(С,Х). Обозначим через Р(Ь) множество систем уравнений вида (1) таких, что цеТ, Туре(Р,)—[Мк—>М], к>1, 1=1,...,п. Будем говорить, что функция (е[Мк->М] (к>!) представима в языке Ь, если существует такая система уравнений РеР(Ь), что если I — ее наименьшее решение, то (I)/=/. Функцию (I), обозначим через /Р и назовем главной функцией наименьшего решения системы уравнений Р. Уравнение Рг=т1 назовем главным уравнением данного представления функции {.

Функциональный язык I назовем функциональным языком программирования, если существует такой алгоритм и, что для любых РеР(Ь) и Ш еМк, где к —местность функции имеем: если то и(Р,Ш)=т, если же [Р(т)=1, то либо и(Р,т)—±, либо и на Р и Ш функционирует бесконечно. В этом случае 'Р(Ц назовем множеством программ, функцию 1Р — семантикой программы РеР(Ь), а и интерпретатором языка Ь.

Раздел 1.3 посвящен иллюстрации, описанной в разделе 1.2 концепции, на таких языках как: язык рекурсивных функций Геделя-Эрбрана, функциональный язык Бэкуса, ЛИСП, РЕФАЛ, язык нормальных алгорифмов Маркова, язык машин Тьюринга, процедурные языки. Для всех рассматриваемых языков интерпретаторы существуют, поэтому иллюстрация заключается только в описании четверки множеств М, С, X, Г для каждого из них.

ГЛАВА 2 посвящена вопросам, связанным с интерпретацией функциональных языков программирования и состоит из трех разделов 2.1-2.3.

В разделе 2.1 на всяком полном множестве определяется топология и рассматриваются непрерывные отображения, отображающие одно топологическое пространство в другое. Понятия и утверждения раздела 2.1 используются в последующих разделах. Пусть А — полное множество. На множестве А определим топологию следующим образом. Множество БсА является открытым, если:

• аеБ и а<Ъ ЬеБ,

• БсА, X» —л.у.м. и эирБ еБ =>

Далее будем считать, что на всяком полном множестве определена такая топология. Пусть А,В — полные множества и Можно показать, что / — непрерывное отображение тогда и только тогда, когда Ц8ирО)=5\1рЦО) для любого непустого линейно упорядоченного ИсА. Легко показать, что всякое непрерывное отображение монотонно.

В разделе 2.2 рассматривается класс функциональных языков £, использующих переменные и константы монотонных типов любых порядков, причем константы порядка 1 являются вычислимыми функциями, а константы порядков >2 эффективно представи-мы. К классу £ принадлежат все широко распространенные алгоритмические языки, в частности и те, которые были рассмотрены в разделе 1.3.

Будем говорить, что монотонная константа у/ порядка >2 эффективно представима, если существует такая монотонная система уравнений (1), что всякая константа порядка 1, используемая системой, является вычислимой функцией, система не использует констант, порядок которых >1, и если / — ее наименьшее решение, то \у=(1),. Систему (1) назовем эффективным представлением константы уг, а уравнение Р,=т, — главным уравнением данного представления.

Теорема 2.2.1. Всякий язык Ье£ является функциональным языком программирования.

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

Пусть М — ч.у.м., содержащее наименьший элемент ± , и каждый элемент из М сравним только с ± и с самим собой. Введем понятие непрерывного типа:

1. Множество М есть непрерывный тип.

2. Если Да,,...,ак(к>0) — непрерывные типы, то множество всех непрерывных отображений из а,х...хак в р (обозначим (а,х...хак—>Р)) есть непрерывный тип.

3. Других непрерывных типов, кроме определенных согласно 1-2, нет.

Определение корректно, так как всякий непрерывный тип является полным множеством. Константы и переменные непрерывных типов условимся называть непрерывными; термы, использующие только непрерывные константы и переменные, — непрерывными термами; системы уравнений (1), использующие только непрерывные константы и переменные, — непрерывными системами уравнений.

Лемма 2.2.1. Непрерывная система уравнений (1) имеет наименьшее решение /:

I = вир{ (^[Щ ¡к<со}, где (р— отображение, соответствующее системе (1), О— наименьший элемент множества Туре(Р])х... хТуре(Рл), </?(П)=П, £2)=(р(<^(П)), к<оо, со — ординал, соответствующий натуральному ряду.

Каждому монотонному типу а сопоставим непрерывный тип а, называемый проекцией типа а. Если а=М, то а~М, если же <х=[а,х...хак-^/3], то а=(а,х.. хак-*р), где /?,а,- — непрерывные типы, являющиеся проекциями монотонных типов Д аг„ соответственно, 1=1,...,п. Пусть х — монотонная переменная типа а и а — проекция а, тогда непрерывную переменную х типа а назовем проекцией переменной х.

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

а, называемая проекцией константы ст. Если а=<а„...,стп> (п>0) вектор проецируемых констант, то вектор их проекций §=<сгг/.<хп > назовем проекцией вектора сг. Если сге[а,х...хак—>/3], где /3,а,,...,ак (к>0) —монотонные типы, то через Агд(а) будем обозначать а,х...хак.

Определение проецируемой константы:

1. Всякая монотонная константа порядка 0 или 1 и всякая монотонная константа порядка 2, которая непрерывна, являются проецируемыми константами, проекциями этих констант будут они сами.

2. Пусть ёеа, где а — монотонный тип, огс1(а)=п>3, тогда ё будет проецируемой константой, если существует такая непрерывная константа ё еа, где а — проекция а, что для любых векторов ап_1,...,сгп__к [1<к<п-2), состоящих из проецируемых констант, и векторов их проекций ап_,,...,а:Г1_к таких, что

огй(8( (ё„_к))<3,

имеем

8(ап_,}...(ап_к) = 6 (ста.,)...(сга.к),

константу <3 назовем проекцией константы 8.

3. Других проецируемых констант, кроме определенных согласно 1-2, нет.

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

Пусть Р — проецируемая система уравнений вида (1), тогда

проекцией системы Р назовем непрерывную систему уравнений Р, имеющую вид

где ^ и х{ являются проекциями Pi и г„ соответственно,

Лемма 2.2.2. Пусть Р — проецируемая система уравнений

вида (1) и Р — ее проекция. Тогда, если </,...../„> — наименьшее

решение системы Р, a <f,.....1„> — наименьшее решение системы

Р, то для каждого i=I,...,n i, — проецируемая константа, /) — проекция константы f, и для тех г'=/,...,п, для которых ord(f,)<2 имеем:

f-sup{(^(n))Jk<a}, Где ^ — отображение, соответствующее системе уравнений Р, О — наименьший элемент множества Type(Fl)x...xType(Fn), <ff (Q)~Q, к<со, со — ординал, соответствующий

натуральному ряду.

Лемма 2.2.3. Всякая эффективно представимая константа является проецируемой.

Универсальный интерпретатор для класса языков £ основан на следующем. Пусть Lefj , P^P(L), т еМк, где к — местность функции /,.. Тогда, используя Лемму 2.2.2 и Лемму 2.2.3, получим: {,,(т )=svLp{(<^(Q)),(m) /к<о> }, где <р — отображение, а О — наименьший элемент, соответствующие системе Р.

Раздел 2.3 посвящен языкам, использующим монотонные, но не непрерывные функционалы (константы порядка 2). В нем вводятся понятия монотонного и непрерывного свойств монотонных функций, которым соответствуют монотонные соответственно непрерывные функционалы. Описывается класс языков, использующих функционалы, соответствующие монотонным, но не непрерывным свойствам монотонных функций и на примере эдного языка иллюстрируется методика построения интерпретато-эов для таких языков программирования.

Обозначим через Ф множество всех монотонных функций констант порядка 1) некоторой фиксированной местности. Всякое тодмножество Ф'сгФ назовем свойством монотонных функций. Свойство Ф' назовем монотонным, если из того, что 1еФ\ деФ и <д следует, что деФ'. Монотонное свойство Ф' назовем непрерыв-шм, если для всякого непустого линейно упорядоченного Ф"сФ\Ф' шеем зирФ"еФ\Ф'. Каждому свойству Ф' сопоставим функционал '.ф- такой, что если [еФ, то

[true если / е Ф',

ХфМ = , ,

(±, если / g Ф ,

десь true —некоторый фиксированный элемент из М\{1).

Утверждение 2.3.1. Пусть Ф' — свойство монотонных функций, тогда

а) Ф'—монотонно о %ф--монотонный функционал,

б) Ф'— непрерывно о хф'— непрерывный функционал.

Утверждение 2.3.2. Пусть Ф' — свойство монотонных функций, тогда Ф'монотонно и Ф\Ф'монотонно Ф—0или Ф—Ф.

Свойство монотонных функций Ф'назовем эффектвно предс-тавимым, если Хф' — эффективно представимый функционал. Заметим, что из эффективной представимости свойства Ф' следует его непрерывность, а из непрерывности — монотонность. Можно показать, что свойство пустоты области определения монотонных функций не является монотонным, однако его дополнение эффективно представимо; свойства тотальности и бесконечности области определения будут монотонными, но не непрерывными, а следовательно, и не эффективно представимыми свойствами, а дополнения этих свойств не будут монотонными.

Рассмотрим функциональные языки, которые используют функционалы, соответствующие монотонным, но не непрерывным свойствам монотонных функций. В обсуждаемых языках такие функционалы должны применяться к функциям, которые представляются системами уравнений, принадлежащими к таким классам программ, для которых рассматриваемые свойства частично разрешимы. Такие функционалы, вообще говоря, нельзя заменить на некоторые эффективно представимые функционалы, которые бы на рассматриваемом классе программ имели бы те же самые значения, что и исходные функционалы. Однако для каждого исходного монотонного, но не непрерывного функционала в должен, существовать такой ¿-^/-местный (к>0) эффективно представимый функционал щ , что для каждой интересующей нас функции /, представимой в рассматриваемом языке, можно было бы эффективно определить такие элементы т,,...,ткеМ\{±}, что у/^^т,,.. .,тк). Тогда каждое применение в вида 0(Р,), которое использовано в конкретной программе рассматриваемого языка, можно заменить на у^т'^... ,т'к), где т\,...,т[ будут определяться по подсистеме уравнений, главным уравнением которой будет Р,=г,. Таким образом, интерпретатор, получив на вход программу и начальное значение, должен расширить программу эффективными представлениями функционалов у/в для каждого в и, если главным уравнением эффективного представления функци-

онала у/д является Fg= тв , то интерпретатор для каждого конкретного применения в вида 9(F() должен находить свои элементы т\,...,т'к и заменять 6(FJ на Г0(Рьт\,...,т'к). Далее может функционировать интерпретатор, описанный в доказательстве Теоремы 2.2.1. Проиллюстрируем данный подход на конкретном языке программирования L0.

Язык L& Опишем множества М, С, X, Т.

M=Zu{±}, где Z — множество целых чисел.

С = {+, - >, <, if_then_else, в„ О^иМ. Определим только функционалы 0,, 02, так как остальные элементы множества С определяются традиционным образом. Отметим, что 0 и 1 будут соответствовать значениям true и false соответственно. Функционалы 0,,02 е[[М->М1—>М} и, если fe[M-*M], то 0¡(f) равно 0, если VzeZ f(z)?±, и равно 1 в противном случае; в2({) равно 0, если множество {z / zeZ и i(z)^dL} - бесконечно, и равно 1 в противном случае. Легко видеть, что 0t и 02 являются функционалами, соответствующими свойствам тотальности и бесконечности области определения одноместных монотонных функций, соответственно.

X={x,y}u{F;[J,F{2' !i>l], где Туре(х)=Туре(у)=М, Type(Ff'J)= [М-^М], Type(Ff2J)=[М2->М], i>l.

Т состоит из термов вида Ax[if е(х,с) then t, else t2] и Axy[if л then т, else т2], где £е{>,<}, ceZ; t,, t2 имеют вид m, х, F/'y(x), где msM, г>1; л имеет вид tyF/1'), sfF/'^x), у), s(F/1J(x),c), е(х,у), е(х,с), с(у,с), где ее{>, <}, ceZ, i>l, j=J,2; т„ т2 имеют вид a, Ftn/(а), Р/2у (а,Ь), где Туре(а)сМ, Туре(Ъ)сМ, а, Ь используют элементы множеств Ми{+,-}, {х,у} и не используют Я.

Приведем эффективные представления функционалов у/^ и ц/.

F0i =AFuv[if eq(u,v) then f0(F(v)) else Fffj (F,u,v-l)+fB(F(v))], (3)

Po2 = AFuv[f0(F(u)) *f0(F(v))J, (4)

где Type(F0i)=Type(Fg2 )=ЦМ-^М]хМхМ->М], Type(F)=[M->M],

Type(u)= Type(v) =M, f0(d)=l, fg(m)=0, если ша±, * — функция умножения, причем J_*0=0*.b=0, eq — функция равенства такая, что eq(l,m)=eq(m,±)—±, eq(mi,m2)=0, если m2^JL и m,=m2,

eq(m,,m2)—l, если m^l, m2*-L и mt?m2.

Интерпретатор языка Lg, получив на вход любую программу PdP(L0) и ш еМА, где к. — местность функции fP, добавляет к системе Р уравнения (3) и (4). Затем все вхождения термов вида OjF(lJh i>l, 1=1,2 заменяются на Fe, (F/'^c^-l^+l), где

cmin>cmax и являются минимальным и максимальным из чисел, используемых в подсистеме, главным уравнением которой является уравнение с левой частью Далее функционирует

интерпретатор из доказательства Теоремы 2.2.1.

В ГЛАВЕ 3 определяется логическая концепция языков программирования, включающая функциональный подход. С позиции общего определения логического языка программирования исследуется язык ПРОЛОГ. Глава 3 состоит из трех разделов 3.1-3.3.

В разделе 3.1 вводится соответствующая формализация и дается определение логического языка программирования. Зафиксируем множество М, содержащее по крайней мере два элемента true и false. Пусть С - множество констант, принадлежащих некоторым типам, X - множество переменных некоторых типов, Т(С,Х) - множество термов, построенных с использованием С и X (определение терма дано в разделе 1.2). Элементарной формулой, построенной с использованием С и X, назовём терм из Т(С,Х), тип которого входит в множество {true,false}. Определим множество формул Ф(С,Х): 1) любая элементарная формулы из Т(С,Х) является формулой, принадлежащей Ф(С,Х); 2) если А,В - формулы из Ф(С,Х) и хеХ, то -п(А), (А)&(В), (A)v(B), (А)=>(В), (А)~(В), Vx(A), Зх(А) есть формулы, принадлежащие Ф(С,Х); 3) других формул, принадлежащих Ф(С,Х), кроме определённых согласно 1-2, нет.

Интерпретация формулы А определяется заданием значений всем её свободным переменным. Значение формулы А на интрпретации определяется естественным образом. Если А,В — формулы и формула (A)zj(B) тождественно истинна, то будем говорить, что формула В является логическим следствием формулы А и обозначать А/=В.

Определение логического языка программирования. Логический язык программирования определяется заданием шестерки М. С, X, Prog, A, U, где:

М - непустое множество, содержащее по крайней мере два элемента true и false;

С - множество констант, принадлежащих некоторым типам;

X - множество переменных некоторых типов;

Prog - множество программ, представляющее собой некоторое непустое подмножество выполнимых формул из Ф(С,Х);

Л - отображение, которое каждой программе РеРгод сопоставляет непустое множество формул А(Р)сФ(С,Х), называемых запросами, соответстующими программе Р;

U - интерпретатор, представляющий собой алгоритм, который для каждой программы РеРгод и запроса QeA(P) либо останавливается с положительным ответом, либо - с отрицательным ответом, либо - с неопределенным ответом, либо функционирует бесконечно. Положительный ответ может быть как со значением, так и без него. Результат применения U к Р и О обозначим U(P,Q). Если U на Р и О останавливается с положительным или отрицательным ответом, то будем говорить, что U(P,Q) — определено. Интерпретатор U должен быть логически корректным:

если U останавливается на Р и О с отрицательным ответом, то есть U(P,Q)-no, то Р/* О;

если U останавливается на Р и О с положительным ответом без значения, то есть U(P,Q)-yes, то Р/= Q;

если U останавливается на Р и О с положительным ответом со значением, то есть U(P,O)=x0, где х0 - вектор значений вектора переменных х, то О имеет вид ЗхА[х) и Р/=А(х0), где А(х0) формула, полученная из формулы А[х) в результате подстановки значений х0 вместо свободных вхождений переменных х.

Под предложенное определение логического языка программирования подпадают такие языки, как: языки ^-программирования, языки хорновского программирования, языки баз данных и т. д.

В разделе 3.2 определяется функциональный язык программирования и его семантика с логической точки зрения. Доказываются Теорема 3.2.1 о том, что семантика функциональной программы является ее логической сущностью, и вытекающая из нее Теорема 3.2.2 о логической корректности и полноте интерпретатора функционального языка программирования. Зафиксируем пятерку Mi, Сь X,, Т,, Ut, задающую некоторый функциональный язык программиривания (см. раздел 1.2) и опишем шестерку М, С, X, Prog, A, U, определяющую его как логический язык программирования (см. раздел 3.1). М=М, Ц true,false}.

С=С,и{=}, где =e{M2¡ {true,false}} и для любых т,,т2&М значение =(m¡,m2) есть true, если m¡ совпадает с т2, и - false в противном случае.

X—Xtu{y¡, где у —переменная типа M¡.

Prog - множество формул вида

(F1=ti)&...&(F=TJ, (2)

где F,£X¡, F^Fj, если г,еТ„ TypefzJczTypefFJ, Var(r¡)c:{F„..., FJ, Type(Fi)=[Mf —>M)-]; k>l, i,j=l,...,n, n>0.

Утверждение 3.2.1. Всякая формула вида (2) является выполнимой.

Пусть РеРгод и имеет вид (2). Определим множество запросов Л(Р), соответствующих программе Р. А(РМЗу(Р,(10)~у<&у*-1)/х0=<х°,...,х°к>, х° еМ„ i=l,...,k}

Теорема 3.2.1. Пусть РеРгод и имеет вид (2), ОеЛ(Р) и имеет вид 3y(F, (хд [, — семантика функциональной программы

(1), тогда:

a) P/=Q о существует единственное y0eM¡, такое, что /^ЛХо^Уо&Уо^М

b) fi(xj=y0 и У0*1 о P/-F,(х0)=y0¿¿y0*±;

c) P¡=Q

Используя алгоритм интерпретатора U¡, определим интерпретатор U. Пусть РеРгод и имеет вид (2) (это же обозначение Р мы будем использовать для функциональной программы (1)}, пусть ОеЛ(Р) и имеет вид By(F,(xg )~у0&у^1). Тогда:

если U¡(P, x0)=y0?tl, то U(P,O)—y0;

если U¡(P, х0)=1, го U(P,Q)=no;

если U, на Р и хд функционирует бесконечно, то U на Р и О функционирует бесконечно.

Теорема 3.2.2. Пусть РеРгод и имеет вид (2), QeA(P) и имеет вид 3y(F,(xa j=ya&y0^l), тогда:

a) если U(P,Q)=y0eM¡, то PJ=F,(x0)=y0&y0*M

b) если U(P,Q)=no, то Pf*Q;

c) если Р/=0, то U(P,Q)—y0£M¡.

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

смысле, а не те, которые выполняют некоторые действия в процессе функционирования интерпретатора или являются способом выражения управляющей информации. Описывается шестерка М, С, X, Ргод, Л, U, определяющая ПРОЛОГ, как логический язык программирования. Доказывается Теорема 3.3.1 о логической корректности интерпретатора ПРОЛОГа, использующего любые встроенные предикаты (логическая корректность интерпретатора ПРОЛОГа в случае отсутствия встроенных предикатов следует из результата К.Апта и М.ван Эмдена о полноте SLD-резолюции2). Дело в том, что интерпретатор ПРОЛОГа устроен таким образом, что некоторые встроенные предикаты (используемые языком ПРОЛОГ), реализуются им не так, как если бы они были представлены "чистой" ПРОЛОГ-программой (например >), а некоторые из них и вовсе не представимы "чистой" ПРОЛОГ-программой (например arg). Эта ситуация требует исследования того, какое именно расширение SLD-резолюции на случай использования встроенных предикатов используется интерпретатором ПРОЛОГа. Нами описано такое правило вывода, что и использовано при доказательстве Теоремы 3.3.1.

ГЛАВА 4 посвящена вопросам, связанным с интерпретацией и преобразованием логических программ (баз знаний). Описан общий подход к рассматриваемой проблеме. В качестве иллюстрации общего подхода выбраны чистый ПРОЛОГ и некоторое (естественное) множество преобразований. Глава 4 состоит из четырех разделов 4.1-4,4.

В разделе 4.1 обсуждается суть вопроса. Начнем с процедурных программ, то есть с программ, написанных на процедурных языках программирования: АЛГОЛ, ПАСКАЛЬ и т. п. Очевидно, что процедурная программа является частным случаем базы знаний, а именно алгоритмом (на соответствующем процедурном языке), реализующим некоторую функцию. Преобразования процедурных программ (и их моделей) исследовались в работах Ю.И.Янова, А.П.Ершова, Р.И.Подловченко и других авторов. Естественно, что преобразования процедурных программ должны быть эквивалентными (как это принято называть) в том смысле, что преобразованная программа должна вычислять ту же функцию, что и исходная. Преобразования процедурных программ предназначены для улучшения (оптимизации) различных характеристик процедурных программ, таких как: быстродействие, объем используемой памяти и т. д. Перейдем к общему случаю. Логическая

2 Apt K.R., van Emden M.H. Contribution to the theory of logic programming.// Journal of the ACM, v.29, N3, 1982, p.841-862.

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

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

С какой целью должны преобразовываться логические программы? На наш взгляд, одной из целей (помимо, конечно, оптимизационных) может быть расширение области определения интерпретатора. Дело в том, что в реальных системах логического программирования (см. напр. раздел 3.3) интерпретаторы не отвечают на все запросы из допустимого множества запросов. На некоторых из них они либо зацикливаются, либо останавливаются с неопределенным ответом. Это происходит по двум причинам:

1. необходимость в реальное время ответить на запрос, и

2. несуществование разрешающего интерпретатора для более или менее богатого языка логического программирования.

Однако, преобразовывая логические программы, можно в некоторых случаях расширить множество тех запросов, на которые интерпретатор даст определенный ответ. Теперь поговорим о запросах. Запрос - это тоже логическая формула. Следовательно, можно преобразовывать и запросы. Естественно встают все те же вопросы: как и с какой целью? Дело в том, что, оказывается, результат интерпретатора логического языка программирования может зависеть и от того, "как спросишь". Естественно, что преобразования запросов должны быть такими, чтобы исходный и преобразованный запросы одновременно либо являлись логическим

следствием программы, либо нет. Возможно и одновременное преобразование программы и запроса.

Раздел 4.2 посвящен формализации описанных в разделе 4.1 соображений. Пусть Ф(С,Х) - множество формул, построенных с использованием С и X, где С - множество констант, а X - множество переменных некоторых типов. Пусть Ф'сФ(С,Х) и Ф'^0. Под преобразованием формул множесва Ф' мы будем понимать пару (А,А'), где ДА' еФ'. Пусть Т - некоторое непустое множество преобразований формул множества Ф'. Будем говорить, что формула

г

АеФ' Т-преобразуема в формулу ВеФ' (обозначим А~*В), если существует такая последовательность преобразований

(Л/y42J,.. принадлежащих Г, что А,=А, Ап—В, п>1.

Рассмотрим произвольный логический язык программирования, определяемый шестеркой М, С, X, Prog, A, U. Пусть РеРгод. Введем обозначения:

Yes(P)={QeA(P)\ Р/=ОЛ Ans(U,Pj={QeA(P)\ U(P,Q) - определено;.

Интерпретатор U назовём разрешающим (соответственно логически полным), если для любой программы РеРтод имеем: Ans(U,P)=A(P) (соответственно Yes(P)cz Ans(U,P)).

Введем отношение /1-эквивалентности на множестве программ Prog. Пусть Р,,Р2 еРтод. Будем говорить, что Р, и Р2 /4-эквива-

4

лентны (обозначим Р,~ Р2), если А(Р,1=А(Р2) и Yes(Pt)=Yes(P2j.

Пусть Т - некоторое множество преобразований программ Prog, которое для каждой программы РеРгод содержит преобразование (Р,Р).

Интерпретатор U назовем ^разрешающим (соответственно /^логически полным), если для любой программы РеРгод

т д

существует такая программа Р'еРгод, что: Р—>Р', Р~Р' и Ans(U,P')=A(P'J (соответственно Yes(P')czAns(U,P')).

Пусть Quer есть множество, состоящее из запросов, соответствующих всем программам множества Prog. Пусть Tq - некоторое множество преобразований запросов Оиег, которое для каждого запроса QeQuer содержит преобразование (Q,Q).

Интерпретатор U назовём Т, Tq-разрешающим (соответственно ^-логически полным), если для любой программы РеРгод и любого запроса QeA(P) существуют такие Р'еРгод и Q'eA(P'), что:

T Tq д

Q~>Q', Р~Р', Q cYes(P) <=Ю' eYcs(P') и Q'eAns(U,P') (соответственно Q' eYes(P')=>Q' eAns(U,P')).

Легко видеть, что имеет место следующее: U- разреш. => U - Т- разреш. => U - Т,Т„— разреш.

u и W

[/-лог.полный => U - Т-лог.полный => U- Т,7"1?-лог.полный

В разделе 4.3 рассматривается чистый ПРОЛОГ, т.е. ПРОЛОГ, не использующий предикаты от предикатов и не использующий встроенных предикатов. Доказывается Теорема 4.3.1 о том, что отношение zl-эквивалентности и его дополнение не являются частично разрешимыми в случае чистого ПРОЛОГа.

В разделе 4.4 определяется множество преобразований, которые переставляют и удаляют предложения ПРОЛОГ-программ, переставляют атомы в телах правил ПРОЛОГ-программ и в ПРОЛОГ-запросах. Устанавливаются исчерпывающие результаты для некоторых подмножеств чистого ПРОЛОГа, характеризующие его интерпретатор относительно выбранного множества преобразований (Теоремы 4.4.1-4.4.5).

ГЛАВА 5. Теоретической основой современных систем логического программирования является теория хорновского программирования, основания которой изложены в монографии Дж.Ллойда3. Однако реальные системы логического программирования используют встроенные предикаты, реализация которых отлична от той, которая бы соответствовала их представлению хор-новскими дизъюнктами (см. раздел 3.3). Кроме того, как это будет видно из результатов данной главы (раздел 5.2), не всякий встроенный предикат представим "чистой" хорновской программой. Поэтому весьма актуальным является создание теории хорновского программирования со встроенными предикатами, разработке которой посвящена настоящая глава. Глава 5 состоит из пяти разделов 5.1-5.5.

В разделе 5.1 вводятся начальные понятия и обозначения. Зафиксируем три непересекающихся счетных множества и ЯГ. 9 — множество функциональных символов с приписанной каждому символу местностью, причем для любого п>0 содержит счетное число символов местности п. "X— множество предметных переменных. Из элементов множеств ? и "X строятся функциональные термы (ф.термы). Через М обозначим множество всех ф.термов, не использующих предметных переменных.

3 Lloyd J.W. Foundations of logic programming.// Springer-Verlag, 1984, 120p.

р = где — множество предикатных символов с при-

писанной каждому символу местностью, причем для любого п>0 "Рх содержит счетное число символов местности п; — некоторое множество интерпретированных предикатных символов — встроенных предикатов, каждый i-местный (к>0) встроенный предикат представляет собой вычислимое отображение M^'-^írue, false}. Атом определяется традиционным образом. Атом, не использующий предметах переменных назовем основным. Атом, использующий предикатный символ из Р, назовем предикатным термом. Атом, использующий встроенный предикат из Рг назовем условием. Литерой назовем агом или его отрицание. Дизъюнкт представляет собой либо литеру, либо дизъюнкцию конечного числа литер. Традиционным образом определяется формула логики предикатов первого порядка, использующая логические операции -., &, v, з и кванторы Э, V. Далее, говоря "выражение Е", мы будем понимать ф.терм, атом, дизъюнкт или множество дизъюнктов. Обозначим через Vai(E) множество всех предметных переменных, входящих в выражение Е.

Напомним определения подстановки, унификатора, наиболее общего унификатора. Подстановка а есть множество вида: {t¡/x¡,...,tn/xj, где t,— ф.терм, x¡ — предметная переменная, t^x,, i^j=>x¡^j, i,j=l,...,n, п>0. Пустую подстановку условимся обозначать е. Традиционым образом вводится композиция подстановок, которая является ассоциативной операцией. Введем обозначения: Arg(<y)={x,,..,,xj, Var(aj=Var(t¡)u... uVar(tr). Пусть Е — выражение. Через Ест обозначим выражение, полученное из Е путем одновременной подстановки термов t¡,...,tn вместо переменных xh...,xa соответственно. Напомним, что для любых подстановок а, 8 и выражения Е имеем: (Еи)8=Е(о8). Будем говорить, что выражения Е„...,Еп (п>1) унифицируемы, если существует такая подстановка ó, что Ei8=...=E„8. Подстановку 8 назовем унификатором этих выражений. Унификатор су назовем наиболее общим унификатором выражений Е,,...,Еп (a=mqu(E„...,EJ), если для любого их унификатора д существует подстановка у такая, что <r/=S.

Опишем рассматриваемые нами интерпретации. Предметным множеством рассматриваемых интерпретаций будет множество М. Функциональные символы интерпретируются следующим образом: каждому 0-местному символу из "? сопоставляется он сам, каждому л-местному (п>0) символу fe? сопоставляется отображение М"—>М, которое n-ке <t¡,...,tn>, где t¡еМ, i=l,...,n ставит в соответствие

терм iff,,...,(J. Каждому О-местному символу из Р\ сопоставляется один из элементов множества {true, false}, а каждому ri-местному (п>0) символу из Рх сопоставляется некоторое отображение Mn->{tme,false}. Обозначим описанное множество интерпретаций через Н. Заметим, что интерпретации из Н могут отличаться одна от другой лишь отображениями, сопоставляемыми символам множества Pv Поэтому каждую интерпретацию 1еН можно отождествлять с множеством тех основных предикатных термов, значения которых на I есть true. Легко видеть, что множество Н будет полной решеткой, если в качестве частичного порядка на Н взять отношение включения.

Пусть F — формула, не использующая предметных переменных и I — интерпретация из Н. Через Val^F) условимся обозначать значение формулы F на интерпретации I. Если Val,(F)=true, то интерпретацию I назовем моделью формулы F. Если формула F не использует символов множества Р1г то значение F на любой интерпретации из Н будет одним и тем же. Условимся обозначать его ValfFJ.

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

Логическая программа Р (далее просто программа) есть множество предложений {S,,...,Saf, и>0. Предложение S, является либо фактом А„ либо правилом А,:-Вп,..., Bim. представляющим собой

дизъюнкт Ai v -iBuv...s/—iBim. , где Д- — предикатный терм, а

каждое из BiV ...,Bim.— либо предикатный терм, либо условие,

т,>0 , г—/,...,и. Пусть Var(Pj={xh...,xJ, v>0. Программе Р сопоставим формулу F(P):

\/x1...Vxr(S1&...&Su).

Всякую модель формулы F(P) условимся называть моделью программы Р.

Будем говорить, что ¿-местное отношение ТсМк, к>1, программируемо, если существует программа Р и ¿-местный предикатный символ pePi такие, что <t,,...,tk>eT <=> p(t,,...,tk)eIP, где 1РеН и является наименьшей моделью программы Р, t,eM, i=l,...,k.

Каждому предикату и : Мк -¿{true,false}, к>1, соответствует к-местное отношение ТлсМк, представляющее собой область истинности предиката п. Будем говорить, что предикат п программируем, если программируемо отношение Тл.

Пусть О — О-местный, s — i-местный символы из р. Рассмотрим множество термов N={0,s(0),s(s(0)),...}, называемых натуральными числами. Всякое TcN*, к>1, назовем i-местным арифметическим отношением. Известно, что любое рекурсивно перечислимое арифметическое отношение программируемо при Р2=0

Утверждение 5.2.1. Если Р2=0, то не всякое рекурсивное отношение ТсМк, к>1, программируемо.

Примером рекурсивного не программируемого отношения может служить следующее 2-местное отношение Тс: М2.

T={<tht2> I t,еМ, t2eN и t2 есть местность самого левого функционального символа терма t¡}

Следствие утверждения 5.2.1. Если тс> не всякий

вычислимый предикат тс. Mk->{ true,false}, к>1, программируем.

Пусть <р: M N — вычислимое взаимно однозначное отображение из M на N. Определим предикат к М3-¿{true,false} следующим образом: v(t ¡,t2)=true, если ço(t!)=t2, и v(t,,t2)—false, если <p(ti)ït2, tht¡eM. Легко видеть, что v— вычислим.

Утверждение 5.2.2. Если veP2, то всякое рекурсивно перечислимое отношение ГсМ\ к>1, программируемо.

Следствие утверждения 5.2.2. Если vep3, то всякий вычислимый предикат m Mk->{true,false}, к>0, программируем.

Введем понятие запроса. Запрос О имеет вид: ?-C¡,...,Ck, где С,- —либо предикатный терм, либо условие, i=l,...,k, к>0. Если к—О, то запрос назовем пустым. Пустой запрос имеет вид: ?-. Пусть Q — непустой запрос и Vai(0)={y¡,...,Yr}, i>0. Запросу О сопоставим формулу F (О):

Зу1..Зуг1С1&...&Ск).

Опишем множество ответов на непустой запрос О к программе Р определенное согласно логической семантике и обозначим его Log(P,Q).

Если Р fe О то Log(P,Q)={no};

если Р /=0 и Var(Q)=0, то Log(P,Q)={yes};

если Р /=0 и Var(0)={y¡,...,yr}, т>0, то Log(P,0) состоит из таких наборов термов <t,,...,tr>eMr, что P/=Q0, где Q — {t,/y„...,t/yJ.

Заметим, что, если Р — программа, О — запрос, имеющий вид ?-ССк (к>0) и в — подстановка такая, что Var(Q0)=0, то Р /-= Q0 <=> Cfielp, если С, — предикатный терм, и Val (С ¡0)—true, если С; — условие, i=î,...,k.

В разделе 5.3 определяются модифицированные правила SLD-резолюции и процедурная семантика. Определим множество модифицированных правил SLD - резолюции £. Правило вывода pe'R получает новый запрос либо по запросу, либо по запросу и предложению, в обоих случаях исходный запрос не пуст. Может оказаться так, что р не применимо к данному запросу или р не применимо к данным запросу и предложению. Если р применимо к запросу Q, то результат применения р к О обозначим p(Q). Если р применимо к запросу О и предложению S, то результат применения р к Q и S обозначим p(Q,S). Каждое правило вывода peTS определяется заданием двух функций Ч'р и Ер . Значениями аргументов этих функций являются непустые запросы. Пусть Q есть запрос ?-Сь...,Ск (к>0). Опишем Ч'р(0) и Ер(0).

Wp(Q)e{l,...,k). Пусть ¥p(Q)=s, l<s<k, тогда SP(Q) не определено, если Cs — предикатный терм, и Ep(Q) равно некоторому (возможно пустому) множеству подстановок, если Cs

— условие. Пусть SP(Q) — определено. Опишем свойства множества SP(Q) в этом случае. Каждая подстановка aeEp(Q) должна удовлетворять следующим трем условиям:

a) Атд (ст) cVarf Cs),

b) Var(a)r->(Var(Q)\Var(Cs))=0,

c) Val(Csoy)=true для любой подстановки у такой, что Vai(Csay)=0.

Кроме того, для любой подстановки 6 такой, что Var(CsSj—0 и Val(Cs5)~true должны существовать подстановки creEp(Oj, у и у, такие, что oy=5y¡ и, если х еVar(Q)\ Var(Cs), то t/xey<=>t/xeS, Легко видеть, что в этом случае Qay=Q8. Заметим, что SP(Q)=0, если не существует подстановки 5 такой, что Vai(CsS)—0 и Val(CsS)=true.

Рассмотрим применение правила р к запросу Q: ?-ССк (к>0). Правило р применимо к О, если 4^(0)—s, l<s<k, С5-условие и Sp(Q)^0. В этом случае р(О) есть запрос

?~С,c,...,Cs_icr,Cs+1o,...,Cka, где ereEP(Q).

Рассмотрим применение правила р к запросу Q: ?-ССк (к>0) и предложению S: А:-В,,...,В]П (т>0). Правило р применимо к О и S, если: О и S не имеют общих переменных, iFp(Q)—s, l<s<k, Cs

— предикатный терм, и Cs с А — унифицируемы. В этом случае p(0,Sj есть запрос:

?-C¡cr,...,Cs_,o, Bi<r,...,Bm<j,Cs+t(j,...,Cko , где o^mgufC^A).

Правило pe^R назовем эффективным, если вопрос о принадлежности подстановки к множеству SP{Q) решается эффективным образом для всех запросов О, для которых £P(Q) опредлено. Естественно, что нас будут интересовать эффективные правила ре%?. Пусть ре%. Будем говорить, что из программы Р и непустого запроса О р-выводим запрос G и обозначим это {P,Q)¡-pG, если существует конечная последовательность запросов Q¡,...,Qn такая, что Q,=Q, On=G и, либо 0м=р(0^, либо QM=p(QbSj.), где Sj. еР,

i—l,...,n-l. Последовательность Q¡,...,Qn назовем />выводом запроса G из (P,Q). Определим множество ответов на непустой запрос Q к прграмме Р, соответствующее процедурной семантике, основанной на правиле вывода peí? и обозначим его Procp(P,Q). Если (P,Q)//-/-, то Piocp(P,QMno}; если (Р,0)/-р?- и Var(Q)=0, то Piocp(P,Q)={yes}; если (Р,0)/-р ?- и Var(0)={y¡,.. .,yj, г>0 , то набор термов <t,,...,tr> из М принадлежит Piocp(P,Q), если существует такой р-вывод Q i,...,Qn пустого запроса из пары (Р,0) и такая подстановка 3, что {tt/y¡,...J/yJcza,...a^S, где o¡ — подстановка, соответствующая тому применению правила р, результатом которого является запрос 0¡+,, i=l,...,n-l.

Теорема 5.3.1. Пусть Р — программа, Q — непустой запрос и р„р2еЯ. Тогда Рг ocp¡ (P,Q) = Рг ос р2 (Р,0 )■

Раздел 5.4 посвящен доказательству логической полноты и непротиворечивости процедурной семантики. Будем говорить, что процедурная семантика, основанная на правиле вывода peTS логически полна (соответственно логически непротиворечива), если Log(P,Q)cProCp(P,Q) (соответственно Procp(P,Q)cLog(P,Q)) для любых программы Р и непустого запроса Q, Пусть

%,—{р\ре£и 4'P(Q)=\ для любого непустого запроса О} Теорема 5.4.1. Для любых программы Р, непустого запроса О и peZi имеем: Procp(P,Q)=Log(P,Q).

Следствие теорем 5.3.1 и 5.4.1. Для любых программы Р, непустого запроса Q и pe"R имеем: Procp(P,Q)= Log(P,Q).

Раздел 5.5 посвящен практическим правилам вывода. Начнем с примеров. Рассмотрим два встроенных предиката системы ПРОЛОГ: is и >. Пусть Q есть запрос, имеющий вид: ?-0 is dfx„...jcJ, . . . ,

где d(x„...jcn) — многочлен с целочисленными коэффициентами от л переменных хи...рст п>1. Легко видеть, что вопрос о применимости правила pe1R¡ к О эквивалентен вопросу о существовании целочисленного решения диафангова уравнения d(x¡,...,xn)=0, что является алгоритмически неразрешимой проблемой. Интерпретатор ПРОЛОГа, встретившись с таким запросом, делает аварийную остановку, что по существу является остановкой с неопределенным ответом. Рассмотрим другой запрос О, имеющий вид:

?~х>0,...,

где х — переменная. Легко видеть, что peg¡ применимо к Q, однако можно затратить очень много времени на подбор такого значения переменной х, которое бы привело к пустому запросу, если, конечно, запрос О логически следует из программы. Интерпретатор ПРОЛОГа и в этом случае решает вопрос просто: делает аварийную остановку. Таким образом, на практике применяются правила вывода, область определения которых уже области определения правил множества /?. Рассмотрим такие правила.

Пусть peg. Определим множество правил Ц,. Каждому правилу р' e'Rp , так же как и правилу р, соответствуют две функции Ч*р и Ер. Причем, Ч'р^Ч'р, область определения функции Ер. входит в область определения функции Ер и, если SP{Q) определено, то Zp\Q)=Ep(Q), где О — непустой запрос. Пусть Q — непустой запрос, для которого ¥¿(0) соответствует предикатному терму и S — предложение, тогда р' применимо к О и S тогда и только тогда, когда р применимо к О и S, и p'(Q,S)=p(Q,S). Пусть О — непустой запрос, для которого Ki'p{0) соответствует условию, тогда возможны следующие три ситуации: р' применимо к Q, р' не применимо к О, р' ломается на О — это особый, по существу аварийный вариант неприменения р' к Q. Опишем эти ситуации:

р' применимо к О, если Ер.(0) определено и 0, причем результаты применения р' к О совпадают с результатами применения р к О;

р' не применимо О, если Ep(Q)=0; р' ломается на О, если Ef,(Q) не определено. Обозначим через Bieak(p') множество запросов, на которых ломается правило р'. Введем частичный порядок на множестве . Пусть р',р" тогда р'-ч р", если Вгеак(р")сВгеак(р'). Легко видеть, что 75р полная решетка, наибольшим элементом которой является

правило р, а наименьшим — правило, которое ломается на всех тех запросах, для которых SP(Q) определено. Пусть р'еЯр , Р — программа и О — непустой запрос. Отметим, что р'-вывод из пары (P,Q) определяется аналогично тому, как это делалось для правил множества К и, если запрос С р'-выводим из (Р,0) , то это обозначается (Р,0)/~рС. Опишем множество Ргоср(Р,0), соответствующее процедурной семантике, основанной на правиле вывода р'.

Если (Р.О)/-Р?~, то Ртоср(Р,0) определяется аналогично тому, как это делалось для правил множества Я?;

если (P,Q)Jf-p?~ и все тупиковые р'-выводы из пары (Р,0) оканчиваются запросами, к которым не применимо р', то Proc/y(PjQ)={no};

если (P,Q)//-,??- и существует р'-вывод из пары (Р,0), оканчивающийся запросом, на котором ломается р', то Рюср(Р,О)=0.

Утверждение 5.5.1. Для любых программы Р, непустого запроса Q, pe'R, р',р" е имеем:

a) р'<р" => Procp(P,Q)cProcp~(P,Q),

b) Procp.(P,Q)<= Piocp(P,Q)

Логическая непротиворечивость процедурной семантики, основанной на любом практическом правиле вывода р'еК р , где реЯ следует из Теоремы 5.5.1.

Теорема 5.5.1. Для любых программы Р, непустого запроса О, ре% и р' €%р имеем: Procp(P,Q)c±og(P,Q).

Охарактеризуем правило вывода, используемое интерпретатором ПРОЛОГа. Введем некоторые определения. Будем говорить, что условие С реализуемо, если существует такая подстановка в, что Var(C9)=0 и Val(C0)=true. Реализуемое условие С назовем универсально реализуемым, если существует подстановка а, удовлетворяющая следующим двум условиям:

1. Val(CcrS)=true для любой подстановки д такой, что Var(CaS)~0;

1. для любой подстановки в такой, что Vai(C6)=0 и Var(C9)=true существует такая подстановка у, что Сау=Св.

Если С универсально реализуемое условие, то подстановку а назовем универсальным реализатором условия С. Например, условие х—у универсально реализуемо ({х/у} — универсальный реализатор), а условие is(x,y) — нет, х,у — переменные. Правило pelR, назовем универсальным, если для любого Q: ?-C¡,...,Ck (к>0), где С,

— универсально реализуемое условие, множество Ер(0) состоит из универсальных реализаторов условия С,. Отметим, что правило вывода, используемое интерпретатором ПРОЛОГа и введенное нами в разделе 3.3, принадлежит всякой решетке , где р — универсальное правило. Таким образом, область определения интерпретатора ПРОЛОГа можно расширять, продвигаясь вверх по одной из таких решеток.

Хорновское программирование (см. монографию Дж. Ллойда) является теорией в рамках логики предикатов первого порядка. Правилами вывода теории хорновского программирования являются правила 5123-резолюции, которые представляют собой модификации правила резолюции Дж.Робинсона4, ориентированные на хорнововские дизъюнкты. Хорновское программирование со встроенными предикатами (см. наст, главу) является теорией в рамках логики предикатов первого порядка со встроенными предикатами. Поэтому естественной выглядит задача обобщения метода резолюций Дж.Робинсона на случай логики предикатов первого порядка со встроенными предикатами.

ГЛАВА 6 посвящена модификации метода резолюций Дж.Робинсона на случай использования встроенных предикатов и состоит из трех разделов 6.1-6.3.

В разделе 6.1 обсуждаются используемые понятия и обозначения, которые в основном совпадают с понятиями и обозначениями раздела 5.1. Введем недостающие. Литеру, использующую предикатный символ из Рь назовем интерпретированной литерой (и.литерой). Дизъюнкт, не содержащий ни одной литеры, называется пустым дизъюнктом. Пустой дизъюнкт условимся обозначать □. Будем говорить, что интерпретация 1еН есть модель непустого дизъюнкта Д если Уа//Д<х£=гше для любой подстановки <х такой, что Уат(Оа)=0.

Пусть 5 — непустое множество непустых дизъюнктов. Будем говорить, что множество 5 противоречиво, если не существует такой интерпретации 1еН, которая бы была моделью всех дизъюнктов множества Б.

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

4 Robinson J A. A machin-oriented logic based on the resolution principie.//Journal of the ACM, 12, N1, 1965, p.23-41.

следующие три вспомогательных правила: склейку Rs, бинарную резолюцию Rb, унарную резолюцию Ru. Напомним правила Rs и Rb, используемые в определении правила резолюции Дж.Робинсона, и введем правило Ru. Ввиду того, что дизъюнкция является комутативной и ассоциативной логической операцией, то дизъюнкт мы будем рассматривать как множество литер.

Правило Rs применимо к любому непустому дизъюнкту D. Rs(D)=Da, где либо а=£, либо (r=mgu(L„...,Lmj, где L„...,Lm некоторые унифицируемые литеры из D, т>1.

Правило Rb применимо к паре дизъюнктов D, D', если они не имеют общих переменных и существуют такие унифицируемые атомы А и А', что AeD и -A' eD'.

Rb(D,D')=Rb(D',nj=(Da\{Au}ju(D'a\{-A'a}), где а=тди(А,А').

Правило Ru. применимо к дизъюнкту D, если существуют такие и.литера LeD и подстановка а, которые удовлетворяют следующим трем условиям:

a) Агд(а) с Var(L),

b) Var(a) Г) (Var(D)\Var(L)j=0,

c) Val(Lcry)~false для любой подстановки у такой, что Var(Loy)=0

В этом случае будем говорить, что Ru I-применимо к D и Ra(D)=Dcr \{La }.

Определение правила R:

R(D)=Ru (Rs(D)), R(D,D')=Rb(Rs(D),Rs(D')), где D, D' — дизъюнкты, не имеющие общих переменных.

Рассмотрим правило Ru. Правило Ru. является не эффективным правилом, так как проверка пункта (с) "упирается" в алгоритмически неразрешимую проблему. Введем понятие разумного ограничения Ru. Пусть Ru I-применимо к дизъюнкту D, где L — и.литера из D. Рассмотрим множество всех L-применений Ru к D. Каждое такое L-применение определяется некоторой подстановкой ст. Пусть S(D,L) есть множество подстановок, определяющих все возможные I-применения Ru к D. Рассмотрим подмножество некоторых ¿-применений Ru к D, определяемое подмножеством подстановок S'(D,L)czS(D,L). Будем говорить, что данное подмножество L-применений Ru к D разумно, если для любой подстановки 5 такой, что Vai(L5)=0 и Val(LS)=false существуют такие подстановки cre£'(D,L), у и у„ что ay~8y¡ и, если xeVar(D)\Var(L), то t/xey<=>Vke8, где t — ф.терм. Очевидно, что в зтом случае Day=D8.

Пусть для каждого дизъюнкта D и каждой и.литеры L таких, что Ru L-применимо к D выделено некоторое разумное подмноже-

ство ¿-применений Яи к Б: Е'(Б,Ь). Ограничимся только такими применениями Яи. В этом случае будем говорить, что имеем некоторое разумное ограничение правила Яи. Обозначим его через Я'и. Правило К'и. назовем эффективным разумным ограничением Яи, если вопрос о принадлежности подстановки к множеству Е'(Б,Ь) решается эффективным образом для любых О и I. Заметим, что, если для любых Б и Ь Е'(Б,1)=Е(Б,Ц, то Я'а=Яи и Я'и есть разумное ограничение Яи, однако эффективность Я'и зависит от множества встроенных предикатов Рг. Если же для любых Б и Ь Е'{Б,Ц состоит из всех тех подстановок сгеЕ(Б,Ц, для которых Уаг(Ь(т)=0 и УаУ/Хо^=Мье, то Я'и будет эффективным разумным ограничением Яи при любом Р2.

Будем говорить, что правило Я' есть (эффективное) разумное ограничение правила Л, если для некоторого Я'и — (эффективного) разумного ограничения Яи имеем:

Я'(Б) = Я'и(Яв(Б)), Я'(О,В') - Я (Б, Б'), где Б, Б' —дизъюнкты, не имеющие общих переменных.

Раздел 6.3 посвящен доказательству полноты любого разумного ограничения правила Я. Пусть Я' — некоторое разумное ограничение правила Я и Б — некоторое непустое множество дизъюнктов. Будем говорить, что из множества Б ^'-выводим дизъюнкт Б и обозначать это Б/^Б, если существует конечная последовательность дизъюнктов Б,,...,Бп (п>1), такая, что Бп=Б и каждый дизъюнкт Ц (1<\<п) либо принадлежит Б, либо получен из предыдущих дизъюнктов последовательности с помощью правила Я'.

Теорема 6.3.1 (о полноте). Пусть Я' — разумное ограничение правила Ли Б — конечное непустое множество непустых дизъюнктов. Тогда, 5 противоречиво <=> 5/-,,О.

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

• доказана семантическая теорема о существовании наименьшего решения канонической системы рекурсивных уравнений,

использующей переменные и константы монотонных типов любых порядков;

• дано определение функционального языка программирования;

• доказана теорема об универсальном интерпретаторе для всего класса языков, использующих переменные и эффективно представимые константы монотонных типов любых порядков;

• предложена методика построения интерпретаторов для класса языков, использующих монотонные, но не непрерывные функционалы.

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

3. В рамках этой концепции исследован язык ПРОЛОГ:

• доказана логическая корректность интерпретатора ПРОЛОГа не использующего предикаты от предикатов и использующего любые встроенные предикаты;

• для ряда подмножеств чистого ПРОЛОГа получены исчерпывающие результаты, характеризующие его интерпретатор относительно некоторой (естественной) системы преобразований.

4. Построена теория хорновского программирования со встроенными предикатами:

• определено множество правил вывода % , представляющих собой модификации правил SLD-резолюции, на случай использования встроенных предикатов;

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

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

5. Разработан метод резолюций для логики предикатов первого порядка со встроенными предикатами:

• определены правило вывода R, представляющее собой модификацию правила резолюции Дж.Робинсона на случай использования встроенных предикатов, и его (эффективные) разумные ограничения;

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Нигиян С А. О разрешимости алгоритмических проб-лем.//Сб. Прикладная математика, вып.2, ЕГУ, Ереван, 1983, стр.8290.

2. Нигиян СЛ. О функциональной и конечной эквивалентнос-тях схем программ.//ДАН Арм.ССР, том LXXX, N2, 1985, стр.115116.

3. Nigiyan S.A. Functional languages of programming.// In: Sixth Conference of Program Designers, Eotvos Lorant University, Budapest, 1990.

4. Нигиян СЛ. Функциональные языки программирования. //Программирование, N5, 1991, стр.77-86.

5. Нигиян СЛ. Об интерпретации функциональных языков программирования.//Программирование, N2, 1993, стр.58-68.

6. Нигиян СА. Функциональная концепция языков програм-мирования.//ДНАН Армении, том 94, N3, 1993, стр.131-137.

7. Нигиян СЛ. Интерпретатор ПРОЛОГа с точки зрения логической семантики.//Программирование, N2, 1994, стр.64-73.

8. Нигиян СА. Логическая концепция языков программиро-вания.//ДНАН Армении, том 93, N1, 1995, стр.26-29.

9. Нигиян С А. Хорновское программирование со встроенными предикатами.//Программирование, N1, 1996, стр.30-38.

10. Нигиян СЛ., Хачоян Л.О. Интерпретация и преобразование логических программ.//ДНАН Армении, том 96, N2-4, 1996, стр.32-37.

11. Нигиян СЛ. Модификация метода резолюций Робинсона на случай использования встроенных предикатов.//Известия НАН Армении, серия Математика, том 31, N5, 1996 (анг. пер. Nigiyan S.A. Modification of the Robinson's resolution method for built-in predicates.//Journal of Contemporary Mathematical Analysis, Vol.31, N5, 1996, pp.49-58).

12. Нигиян СЛ., Хачоян Л.О. О преобразованиях логических программУ/Программирование, N5, 1997.

13. Nigiyan S.A. Mathematical theory of programming languages (functional approach).//Proceeding of Conference on Computer Sciense and Information Technologies (CSIT-97), Yerevan, 1997, pp.2325.