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

РОССИЙСКАЯ АКАДЕМИЯ НАУК ИНСТИТУТ ПРОГРАММНЫХ СИСТЕМ

2 1\ фев 1997

На правах рукописи Лисица Алексей Петрович

ВЗАИМООТНОШЕНИЯ МЕЖДУ ВЫРАЗИМОСТЬЮ И

ВЫЧИСЛИТЕЛЬНОЙ СЛОЖНОСТЬЮ : ОЧЕРЧИВАНИЕ И ЯЗЫКИ ОГРАНИЧЕННОЙ ТЕОРИИ

МНОЖЕСТВ

Специальность 05.13.17 Теоретические основы информатики

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

Переславль-Залесский - 1997

Работа выполнена в лаборатории компьютерной логики Исследовательского центра искусственного интеллекта Института программных систем Российской академии наук

Научный руководитель:

кандидат физико-математических наук, Сазонов В.Ю.

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

- доктор физико-математических наук, профессор Семенов А.Л.

- кандидат физико-математических наук Дехтярь М.И.

Ведущая организация:

Институт прикладной математики РАН

Защита диссертации состоится 1997 г. вД^час. на

заседании специализированного совета Д.200.36.01 при Институте программных систем РАН

С диссертацией можно ознакомиться в библиотеке Института программных систем РАН Автореферат разослан

1997 г.

Ученый секретарь специализированного совета Д.200.36.01 при Институте программных систем кандидат физико-математических наук^ Юмагужина В.Н.

Общая характеристика работы

Актуалыгость темы.

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

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

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

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

Наиболее тесно взаимосвязь выражена в утверждениях вида:

Свойство (отображение) выразимо средствами языка С О свойство можно распознать (отображение можно вычислить) со сложностью С,

Примером является известная теорема Р.Фэйджина, где в качестве С выступает экзистенциальный фрагмент логики второго порядка, а в качестве С - сложностной класс КР.

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

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

случаях естественным является рассмотрение выразимости над конечными структурами.

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

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

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

В работах В.Ю. Сазонова были предложены языки ограниченной теории множеств, выражающие операции над наследственно-конечными (НЕ) множествами, вычислимые с ограниченной сложностью и, более того, точно характеризующие вычислимость за полиномиальное время над НР-множествами.

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

Цель работы.

Исследовать выразительную силу очерчивания над конечными моделями в терминах вычислительной сложности.

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

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

Научная новизна.

В диссертации получены следующие основные результаты:

1.Предъявлена конкретная универсальная первопорядовая формула, очерчивание которой определяет coNP-полный класс его конечных моделей. Тем самым дан отрицательный ответ на открытый вопрос, поставленный в работе P.G. Kolaitis, С.Н. Papadimitriou, Some Computational Aspects of Circumscription. Journal of the Association for Computing Machinery 37(1): 1-14, 1990)

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

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

4.Предложены ограниченные теоретико-множественные языки, характеризующие в терминах выразимости вычислимость с логарифмической памятью (детерминированную и недетерминированную) над фундированным универсумом наследственно-конечных множеств.

5.Показано, что при помощи языка логики первого порядка, расширенного оператором индуктивных определений (FO+LFP), можно

определить линейный порядок на конечных строго экстенсиональных графах. Тем самым дан положительный ответ на открытый вопрос из работы Sazonov, V.Yu.: A bounded set theory with anti-foundation axiom and inductive definability. Computer Science Logic, 8th Workshop, CSL'94 Kazimierz, Poland, September 1994, Selected Papers. Lecture Notes in Computer Science 933 Springer (1995) 527-541 о том, верно ли что, предложенный там ограниченный теоретико-множественный язык определяет в точности полиномиально вычислимые операции над антифундированным универсумом наследственно-конечных множеств при графовом кодировании.

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

Научно-практическая ценность работы.

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

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

• на семинаре по теоретической информатике Института программных систем РАН

• на международном семинаре "Алгоритмы, сложность и обыденные рассуждения" ( Workshop on Algorithms, Complexity and Commonsence Reasoning), проходившем во время Европейской конференции по искусственному интеллекту-94 (ECAI-94), Амстердам, август 1994

• на пятой медународной конференции по теории баз данных (ICDT-95) (International Conference on Database Theory), Прага, январь 1995

• на втором международном семинаре по теории конечных моделей (Workshop on Finite Model Theory), Марсель, апрель 1995

• на международном семинаре по теории конечных моделей и дескриптивной сложности (Workshop on Finite Model Theory and Descriptive Complexity), Принстон, январь 1996

Публикации. Основные результаты диссертации опубликованы в работах 1-7.

Структура диссертации. Диссертация состоит из введения, трех глав и списка литературы из 67 названий. Общий объем диссертации 102 страницы.

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

В Главе 1 мы исследуем выразительную силу очерчивания над конечными моделями в терминах вычислительной сложности.

Глава 2 посвящена разработке версий ограниченных теоретико-множественных языков, выражающих (N)LOGSPACE вычислимые операции над универсумом HF наследственно-конечных множеств и получению характеризации (N)L0GSPACE-Bbi4HanHM0CTH в терминах выразимости.

В Главе 3 мы показываем выразимость линейного порядка на вершинах конечных строго экстенсиональных графов средствами FO+LFP - языка логики первого порядка обогащенного индуктивным оператором наименьшей неподвижной точки. Это влечет результат о точной характеризации полиномиальной вычислимости над наследственно-конечными антифундированными множествами, в терминах выразимости в соответсвующем теоретико-множественном языке.

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

Очерчивание (circumscription) - это логический формализм для представления обыденных рассуждений (commonsence reasoning), введенный Джоном МакКарти (J. McCarty) в 1980 году. Во время рассуждений обычно имеются неявные предположения о предмете рассуждения. Например, обычным является предположение , что мир о котором мы рассуждаем нормален настолько, насколько возможно, или, другими словами, мы предполагаем минимальность его ненормальных свойств. Очерчивание позволяет описывать минимальность такого типа естественным и прямым способом. Пусть <р(Р) - формула первого порядка с отмеченным предикатным символом Р. Тогда очерчивание <р* (Р) предикатного символа Р в формуле <р(Р) утверждает, что не только <f(P) имеет место, но и что предикат Р, удовлетворяющий ip(P), минимален относительно отношения включения. Формально это может быть записано при помощи формулы второго порядка:

<P*(P)^<f(P)kVP' С Р-чр(Р')

где Р' С Р - сокращение, для формулы первого порядка, утверждающей, что Р' есть собственное подмножество Р. Аналогично определяется очерчивание (очерченная формула) f*(P) для случая последовательности предикатов Р.

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

К задачам такого вида могут быть сведены многие вычислительные задачи (не обязательно относящиеся к первоначальному подходу МакКарти), в которых нужно проверить, во-первых, наличие у входной конечной структуры наличие каких-либо свойств (выражаемых, скажем формулой первого порядка), а во-вторых, минимальность некоторых из свойств.

Поскольку очерченная формула есть формулы второго порядка, у которой кванторы второго порядка ( в предваренной форме) универсальны, то задача проверки ее истинности на конечных моделях лежит в сложностном классе coNP (ко-недетерминированного полиномиального времени). Это дает верхнюю оценку сложности подобных задач. Нижнюю оценку выразительной силы очерчивания дали Ф. Колаитис и X. Пападимитриу ( P.G. Kolaitis, С.H. Papadimitriou, Some Computational Aspects of Circumscription. Journal of the Association for Computing Machinery 37(1): 1-14, 1990) предъявив универсально-экзистенциальную (V3) первопорядковую формулу, для которой проверка истинности ее очерчивания на конечных моделях coNP-полна, т.е. относится к числу "самых трудных задач" класса coNP. В той же работе они доказали, что очерчивание любой 3-формулы эквивалентно первопорядковой формуле, и поэтому, в этом случае, проблема проверки истинности на конечных моделях лежит в DLOGSPACE. Случай же универсальных формул они оставили в качестве открытого вопроса : "Предположим, что ф{Р) - универсальное первопорядковое предложение. Верно ли что, проблема проверки истинности очерчивания ф* (Р) разрешима за полиномиальное время ?"

В Теореме 1 мы даем отрицательный, в предположении Р ф NP, ответ на этот вопрос, предъявив конкретное универсальное первопорядковое предложение, определяющее coNP-полный класс его моделей.

Доказательство соКР-полноты основывается на АГР-полноте вычислительной задачи МОНОХРОМАТИЧЕСКИЙ ТРЕУГОЛЬНИК (М. Гэри, Д. Джонсон, Вычислительные машины и труднорешае-мые задачи, Москва, "Мир", 1982)

Предъявленая формула содержит два двуместных предикатных символа - один очерчиваемый, а другой нет, т. е. имеет тип (2,2 | 2), в котором слева от черты перечислены местности всех предикатных символов, участвующих в формуле, а справа местности очерчиваемых предикатных символов.

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

• универсальной формулы типа (2,1,1 | 1,1)

• универсальной формулы типа (3,1 | 1)

• УЗ-формулы типа (2,1 [ 1)

В доказательствах использована ^-полнота задач 3-РАСКРА-ШИВАЕМОСТЬ ГРАФА, 3-ВЫПОЛНИМОСТЬ С ОДНИМ ИСТИННЫМ ЛИТЕРАЛОМ и БЕЗ ОТРИЦАНИЙ, ЯДРО (см. упомянутую выше книгу М. Гэри, Д. Джонсона)

Таким образом показано, что местность очерчиваемого предиката может быть сведена до 1, при сохранении труднорешаемости (соКР-полноты) задач проверки истинности на конечных моделях (за счет добавления неочерченных предикатов), что улучшило ранее известные результаты: упомянутый пример Колаитиса и Папа-димитриу имеет тип (2 | 2).

В Теореме 7 мы показываем, что не только "крайние" случаи со^-полноты (труднорешаемости) и РТ1МЕ-разрешимости могут иметь место для классов конечных моделей, заданных формулами с очерчиванием. Мы предъявляеем формулу, задающую класс конечных моделей, имеющий сложность разрешения (РТ1МЕ-)эквивалентную сложности задачи НЕИЗОМОРФИЗМ ГРАФОВ, которая является обхцепризнаным кандидатом на роль задачи "промежуточной" сложности, не лежащей ни в РТ1МЕ, ни в классе «ДОР-полных задач.

Наконец, естественен вопрос, традиционный для дескриптивной сложности: можно ли любой класс конечных моделей, лежащий в соИР, определить при помощи очерченной формулы, т.е. имеет ли место соответствующий аналог теоремы Фейджина ? Поскольку классы конечных моделей очерченных формул обладают специфическим свойством минимальности, то нетрудно увидеть, что ответ отрицательный (Предложение 1):

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

Однако класс соКР можно-таки "охватить" при помощи очерчивания, если модифицировать понятие определимости.

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

Определение 2 Класс конечных моделей Л4 над словарем <т назовём определимым по Шлипфу относительно очерчивания если

• существует очерченная формула ф'(Ё), над обогащенным словарем а' = а и {Л} и

• существует формула первого порядка ф над а1

такие, что М. есть класс всех конечных моделей, являющихся ре-дуктами моделей из М! = {т | т |= ф*(Ё) Л ф} на словарь а

Замечание. Дж. Шлипф рассматривал аналогичное понятие определимости для очерчивания в случае бесконечных моделей.

Теорема 6 Всякий класс конечных моделей М, лежащий в соИР, определим по Шлипфу относительно очерчивания.

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

Таким образом взаимоотношения между сложностным классом соКР и очерчиванием могут быть представлены в виде двух утверждений:

• Класс конечных моделей М определим формулой с очерчиванием => М лежит в аДОР

• Класс конечных моделей М лежит в coNP => М определим по Шлипфу относительно очерчивания

2. Вторая глава диссертации посвящена разработке и изучению выразительной силы версий ограниченных теоретико-множественных языков, задающих операции над универсумом HF вычислимые с логарифмической памятью, детерминированно и не-детеминированно, и, более того, характеризующих DLOGSPACE-и NLOGSPACE-вычислимость над IIF в теоретико-множественных терминах.

Определение 3 Класс HF наследственно-конечных множеств есть наименьший класс множеств такой что

• пустое множество 0 принадлежит HF

• для любого конечного семейства множеств xi,...xn из HF множество {xi,..., х„} также принадлежит HF

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

Определение 4 Пусть Codes есть некоторый класс кодов. Тогда кодирование v универсума HF есть сюръективное отображение v : Codes — HF.

Так, мы рассматриваем кодирования наследственно-конечных множеств конечными графами с отмеченными вершинами и, более того, графами с разными типами ребер, т. е., фактически конечными реляционными структурами.5

Определение 5 Одноместная операция q : IIF —► HF вычислима относительно кодировании и со сложностью С если следующая диаграмма

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

HF -JU HF

"1 I»

Codes Codes

коммутативна для некоторого вычислимого со сложностью С преобразователя кодов Q.

Нет проблем в понимании данного определения, в случае, когда С - есть класс детерминированной сложности, такой например, как PTIME или DLOGSPACE.

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

Чтобы снять неоднозначность мы используем известный результат Н. Иммермана о характеризации NLOGSPACE- (DLOGSPACE-) вычислимости над конечными линейно упорядоченными структурами в терминах выразимости в FO®(FO°) - языке логики первого порядка, обогащенного оператором транзитивного замыкания ® (соответственно, - оператором детерминированного транзитивного замыкания о)6.

Определение 6 Пусть v : Codes —+ HF есть кодирование HF конечными линейно-упорядоченными структурами. Тогда операцию q : HF —► HF назовем NLOGSPACE(DLOGSPACE) вычислимой если коммутативна следующая диаграмма:

HF -U HF

"I I-

Codes Codes

для некоторого РО®-определимого (ГО®-определимого) преобразователя конечных структур

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

6Иммермап использовал обозначения FO+TC и FO+DTC для рефлексивных версий упомянутых операторов, в настоящей же работе ТС обозначает операцию транзитивного замыкания на множествах

HF HF

•I T-

Codesm Codes

где um : Codesm —» HFm есть кодирование m-кортежей HF-множеств. Обычно в качестве Codesm берут Codes"1, т. е. т-ую декартову степень Codes, но это не обязательно, а для случая (N)LOGSPACE-вычислимости - приводит к трудностям - см. ниже.

Одним из наиболее известных кодирований HF является биективное кодирование Аккермана патуральными числами Аск : N —► HF, определенное следующим образом

Аск(О) = 0 and

Аск(2"' + 2Пз + ... + 2n') = {Ack(ni), Аск(п2),..., Аск(п,)}

ДЛЯ «1 > п2 > ... > rij > 0.

Линейный порядок на универсуме IIF, индуцированный кодированием Аккермана:

аск(п) <hf аск(т) п < т будем называть каноническим

Заметим, что очень простая операция взятия синглетона : х ■—» {ж} соответствует арифметической операции взятия экспоненты к >-+ 1к при таком кодировании и имеет, следовательно, экспоненциальную сложность вычисления (при естественном представлении натуральных чисел в позиционной записи).

Таким образом кодирование Аккермана не очень пригодно для характеризации PTIME (и тем более (N)LOGSPACE ) вычислимости над HF в теоретико-множественных терминах, поскольку самые простые операции становятся невычислимыми при таких сложност-ных ограничениях

Для характеризации PTIME вычислимости над HF посредством выразимости в ограниченных теоретико-множественных языках в работах В.Ю. Сазонова использовалось графовое кодирование множеств, где кодирующей функцией служила операция коллапсиро-вания по Мостовскому.

Обозначим через AG класс всех конечных ориентированных ациклических графов G с выделенной вершиной р в каждом. Рёбра графа G будем обозначать стрелкой с индексом

Определение 7 Операцию V : А(7 —► НР, удовлетворяющую соотношению

1,{0,р)={и(С,р')\р'-+а р}

назовем операцией общего коллапсирования. В частности, если в графе ¿7 у вершины р нет предков, т.е. вершин р' таких, что р' —Р, то имеем ^(<7, р) = 0

Но использование графового кодирования произвольными графами для описания (М)ЬОСЗСРАСЕ-вычислимости наталкивается на принципиальные трудности. Одним из основных является предикат равенства. При графовом кодировании вычисление предиката равенства на НР сводится к задаче распознавания по двум точкам в графе, задают ли они одно и тоже наследственно-конечное множество при коллапсировании, т. е. 1/(С,р) = 1>{С, д) ? Она может быть решена в РТ1МЕ, но как показано Е. Далхаусом является РТ1МЕ-полной. А это означает, что вычисление предиката равенства на НР при графовом кодировании со сложностью ОЬОСЗРАСЕ (или КЬОСЗРАСЕ) влекло бы неправдоподобный положительный ответ на очень трудный открытый вопрос : БЮСБРАСЕ = РТ1МЕ ? (или соответсвенно, ИШСЗРАСЕ = РТ1МЕ ?).

Поэтому, для случая (Г^ЬООБРАСЕ мы рассматриваем в качестве кодов экстенсиональные ациклические графы с выделенными вершинами. Экстенсиональность графа означает, что разным его вершинам соответствуют разные множества при коллапсировании. Это простое свойство выразимо в логике первого порядка : любые две вершины р\ ф р-2 ъС должны иметь различные множества предшественников. т.е. {р : р —рх} ф {р'р —Рг}-

Кроме того, при рассмотрении многоместных операций, чтобы избежать отождествления эквивалентных вершин, которое едва ли вычислимо в (М)ЬОС8РАСЕ, мы рассматриваем кодирования кортежей НРмножеств не кортежами экстенсиональных графов с выделенными вершинами, а кортежами вершин в едином (для каждого кортежа множеств) экстенсиональном ациклическом графе. Таким образом элементами Со</е«т являются в данном случае графы с ш-кортежами выделенных вершин. Кроме того, мы рассматриваем вариации кодирований, при которых графы могут быть снабжены дополнительными отношениями.

Пусть ЕАв т - класс всех конечных ациклических графов с гп выделенными вершинами. Посредством ЕАСт с дополнительными

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

• * - с отношением, являющимся транзитивным замыканием

• < - с отношением канонического линейного порядка на вершинах графа, т. е. порядка соответствующего каноническому порядку на HF относительно коллапсирования.

• -< - с произвольным отношением линейного порядка на вершинах графа.

Определение 8 Пусть Qm - один из определенных выше классов EAGm EAG^,, EAG< m, EAG*<m■ Графовым кодированием m-кортежей наследственно-конечных множеств с кодами из Qm называем отображение ит : Qm -+■ HFm, определенное следующим образом:

Vm((g,ci,...cm)) = (C(g,ci),. ..С(д,ст))

где ci,...,cm - выделенный m-кортеж вершин в графе д, а С есть операция общего коллапсирования.

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

Все рассмотренные теоретико-множественные языки являются расширениями базисного Д*-языка. Определим индуктивно Д"-формулы и Д*-термы слежующим образом:

(Д*-термы) ::= (variables) | {а, 6} | Uа | ТС(а) | {<(х) : х 6(*} а&у?(х)}

(Д*-формулы) ::= а G(t) 6 | <ркф \ <р V У> | | Vx G(t) а<р(х) | Эх aip(x)

где (р и ф есть Д*-формулы, а, 6 и t есть Д*-термы, a х £ FV(a) есть переменная, не свободная в а. Скобки вокруг * означают, что в языке рассматриваются две версии отношения принадлежности: £ и его транзитивное замыкание G*

Для характеризадии выразительной силы языка Д* в разделе 3.4 введен класс SIMPLE простых преобразователей ациклических экстенсиональных графов и показано, что эти преобразователи F0-определимы.

Теорема 9

д. ~hf (eag'-^^eag*)

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

Далее в разделе 3.6 рассматриваются расширения Д* новыми термообразующими конструкциями - г®, служащей для обозначения "горизонтального" транзитивного замыкания, отношения , т.е. множества упорядоченных пар г и "горизонтального" детерминированного транзитивного замыкания г® ^ D{r)®, где D(r) ^ {(ж, у) £ г : 3!г((аг, z) € г)} Выразительная сила этих раширений Д® и Д® охарактеризована в теореме 10 в терминах классов преобразователей расширяющих SIMPLE, а именно SIMPLE® и SIMPLE®, (определимых в fo®h fo°), соответственно:

Д® ~„р (BAG SIMPLE'.EAG) д® ~„F (eag-^^eag-)

Далее мы расматриваем расширения языков Д® и Д® термообразующей конструкцией, интерпретируемой как операция коллапсиро-вания :

С : HF — HF

являющаяся ограничением вышеупомянутой операции общего кол-лапсирования -у на случай EAG, рассматриваемых как элементы HF(i.e. как множества упорядоченных пар). Таким образом С((д,р}) есть множество в HF, полученное применением у к вершине р в графе д, если д есть экстенсиональный и ациклический граф, а иначе

С{{д,р)) = 0.

Расмотренные расширения A®+externaiC и AQ+extenalC имеют специальный вид: допускается лишь внешнее применение операции С, т. е. терм вида С(_) не может быть собственным подтермом какой-либо формулы или терма.

В теореме 11 показано, что эти расширения задают в точности операции над HF, вычислимые при помощи F0®— и, соответсвенно F0®— определимых преобразований EAG'-графов:

А® + external С ~hf ( EAG-—--EAG )

\ ?nlogspace? / A® + external С ~hf (EAG*-—--EAG*]

\ 7dlogspace? )

Таким образом, мы почти получили требуемую характеризацию NLOGSPACE и DLOGSPACE вычислимости над HF в теоретико-множественных терминах - если бы удалось выразить линейный порядок на вершинах графов, кодирующих множества, средствами FO® (F0®), то получили бы совпадение указанных класссов преобразователей с NLOGSPACE- соответственно DLOGSPACE вычислимыми. Выразить линейный порядок, однако, не удалось, и мы предполагаем, что это невозможно этими средствами. Поэтому мы рассматриваем теперь кодирование с кодами из EAG<^.

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

<5>Р)) ^ с((з>р)) если <д - канонический линейный порядок на вершинах EAG^ графа g, и ^ 0 иначе,

и расширив А®, и соответственно А® языки символом <, стандартно интерпретированным отношением канонического порядка на HF, и операцией С, разрешенной только к внешнему применению в теореме 12 получаем характеризацию NLOGSPACE и DLOGSPACE вычислимости над HF Теорема 12.

Д® + external С ~hf (EAG<-—--EAG< )

\ nlogspace J Д® + external С ~hf (EAG!.-—--EAG* )

\ ^ dlogspace v

т.е. классы A® + external С, и A® + external С, определимых операций над ^совпадают с классами операций вычислимых при помощи F0®—, соответственно, ГО®-определимых преобразователей линейно упорядоченных графов, т.е. NLOGSPACE- и DLOGSPACE-вычислимых преобразований кодов.

3. Третья глава посвящена вычислимости и выразимости над универсумом антифундированных наследственно-конечных множесть HFA.

Традиционные теории множеств имеет дело с с фундированными множествами, т.е. множествами X, для которых нет бесконечных цепей X В xi Э Х2... Э хп Э ... в отношении принадлежности. Существование нефундированных множеств запрещается в этих теориях аксиомой фундирования (регулярности). Для произвольных графов с бинарным отношением —> фундированность означает отсутствие в них бесконечных цепей ...—>■ v„ —►...—> ui —<■ uo- Заметим, что для конечных графов это свойство эквивалентно ацикличности.

Толчком к развитию теории нефундированных множеств послужила работа П. Акцеля4 . В этой работе вместо аксиомы фундирования предложена аксиома антифундирования, говорящая о том, что существует единственная теоретико-множественная операция декорации D(G, х) над графами с выделенной точкой, понимаемымии как произвольные множества пар (х,у) ^ {{г}, {ж, у}}, и удовлетворяющая тождеству D(G,y) = {D(G,x) : {х,у) £ G}. Эта аксиома влечет существование в любом универсуме, удовлетворяющем ей, множеств, отношение принадлежности на транзитивном замыкании которых может образовывыть нефундированный граф, имеющий к примеру циклы.

Типичным антифундированным множеством является Г2 = {Q}, содержащее само себя в качестве единственного элемента. Здесь отношение принадлежности образует граф, состоящий из одной вершины и петли.

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

Естественным для всех этих приложений является использование наследственно-конечных множеств. Заметим, что в антифунди-рованном случае существует два различных варианта определения универсума наследственно-конечных множеств; в одном из них HFi наследственно-конечные множества могут иметь бесконечное транзитивное замыкание, тогда как в другом HF1^2 требуется конечность транзитивного замыкания. В настоящей работе мы называем этот последний универсум HFA.

4Aczel, P. Non-Well-Founded Sets. CSLI Lecture Notes, No. 14, 1988

В.Ю. Сазонов2 рассмотрел ограниченную теорию антифундирован-ных множеств. Язык Ар = А + Ree + D этой теории, в отличие от языка Д + Ree + С, соответствовавшего PTIME-вычислимости над HF, содержит функциональный символ D, интерпретируемый как операция декорации на HFA, вместо операции коллапсирования С на HF.

Посредством Ree обозначена термообразующая конструкция

the — leastp.(p = {i £ а : ^(r,p)}

, где перемепные х и р не свободны в а , а все вхождения переменной р в Д-формуле у> имеют вид '— 6 р', позитивны и не находятся внутри никакого сложного подтерма формулы <р. Эти условия на р гарантируют, что <р монотонна по переменной р, а вся конструкция служит обозначением наименьшей неподвижной точки, которая существует при таких условиях.

В той же работе выразительная сила Ad над универсумом HFA охарактеризована в терминах FO+LFP-выразимых3 преобразователей кодов, при этом кодами служат произвольные конечные графы с отмеченной вершиной, а кодирующей функцией является операция декорации. Это означает, что До-выразимые операции q : HFA —+ HFA это в точности те, для которых существует FO 4- LFP-выразимый преобразователь кодов Q, такой что следующая диаграмма коммутативна :

HF -U HFA D| jo

Codes Codes

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

2Sazonov, V.Yu.: A bounded set theory with anti-foundation axiom and inductive definability. Computer Science Logic, 8th Workshop, CSL'94 Kazimierz, Poland, September 1994, Selected Papers. Lecture Notes in Computer Science 933 Springer (1995) 527-541

3FO+LFP - расширение языка логики первого порядка индуктивным оператором наименьшей неподвижной точки.

с классом FO+LFP-определимых преобразователей, и было неясно, можно ли выразить линейный порядок на кодах допустимыми средствами. Более точно: несложное рассуждение показывает, что положительный ответ на вопрос о совпадении Ад-выразимости и PTIME-вычислимости на HFA относительно графового кодирования следовал бы из равномерной выразимости в языке FO+LFP (какого-либо) линейного порядка на вершинах конечных строго экстенсиональных (с.э.) графов.

Граф называется строго экстенсиональным если разные его вершины представляют разные множества в HFA относительно операции декорации.

В Теореме 13, мы показываем, что линейный порядок на классе конечных строго экстенсиональных графов действительно равномерно выразим в FO+LFP, отвечая тем самым положительно на упомянутый открытый вопрос.

Полученный линейный порядок, можно представить себе следующим образом: каждой вершине с.э. графа мы сопоставляем счетную последовательность фундированных наследственно-конечных множеств, являющихся в некотором смысле "приближениями" к соответсвующему антифундированному множеству. Далее, используем канонический линейный порядок на фундированных HF-множествах и переносим его на эти последовательности лексикографически. Такое упорядочивание последовательностей индуцирует линейный порядок на начальном графе. Для того, чтобы доказать, что это можно выразить в FO+LFP, существенно используется известная теорема Я. Московакиса о выразимости в FO+LFP предиката "сравнения шагов" (stage comparison) индуктивных определений.

Далее в Теореме 14 мы предъявляем другое индуктивное определение этого же порядка -< средствами FO+IFP - языка логики первого порядка расширенного оператором инфляционной неподвижной точки, выразительная сила которой над классами конечных моделей равна выразительной силе FO+LFP (согласно известной теореме Ю. Ш. Гуревича и Ш. Шелаха). Это определение использует идею лексикографического упорядочивания классов эквивалентности, получающихся на шагах индуктивного вычисления отношения бисимуляции ps, где х y^D(g,x) = D(g,y). Идея заимствована нами из работы А.Давара, С. Линделла, С. Вайнштейна1 (далее -DLW), где авторы использовали лексикографическое упорядочива-

1А. Dawar, S. Lindeil, S. Weinstein, Infinitary Logic and Inductive definability over Finite Strcutures, Information and Computation, v. 119, 2 , pp. 160-175,1995

ние классов эквивалентности, получаемых на шагах индуктивного определения отношения эквивалентности =к (неразличимости при помощи формул первого порядка, содержащих не более к различных переменных). Они получили результат, которой говорит о том, что на любом классе конечных ¿-жёстких структур, линейный порядок выразим в FO+LFP.

В теореме 15 мы показываем, что конечные строго экстенсиональные графы являются 2-жёсткими, откуда непосредственным применением упомянутого результата из работы DLW, получаем еще одно положительное решение вопроса о выразимости линейного порядка над вершинами строго экстенсиональных графов средствами FO+LFP.

Далее мы показываем (Теорема 16), что определенный выше порядок -< и порядок <С, определенный при помощи метода из DLW, существенно разнятся: в первом случае линейный порядок на классе с.э. графов индуцирует единый линейный порядок на целом универсуме HFA, тогда как во втором случае линейный порядок на классе с.э.г. индуцирует лишь локальные и несогласованные между собой линейные упорядочивания элементов транзитивных замыканий множеств из HFA .

Тем не менее оба подхода достаточны для положительного ответа на вопрос о характеризации PTIME-вычислимых функций над универсумом HFA относительно графового кодирования в терминах А + Ree + D - выразимости.

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

Литература.

1. Alexei P. Lisitsa, Complexity of Universal Circumscription, International Journal of Foundations of Computer Science Vol.4 No. 3 (1993) 241-244.

2. А. П. Лисица, Универсальная формула с CoNP-полной проблемой проверки истинности ее очерчивания на конечных моделях, в Теоретические и прикладные основы программных систем. Сборник трудов. Под редакцией В.И. Гурмана, 1994, Переславль-Залесский, с. 69 - 72

3. Alexei P. Lisitsa, On model checking complexity of circumscription, in Proceedings of Workshop on ALGORITHMS, COMPLEXITY AND COMMONSENCE REASONING'94, held in conjunction with ECAI'94, Amsterdam, August 1994.

4. Alexei P. Lisitsa, The circumscription over finite models: about the border of coNP-completeness. In: Abstracts of the talks of Finite Model Theory Workshop, 10-14 April 1995, Marseille, p.7

5. Sazonov, V.Yu., Lisitsa, A.P., A-languages for sets and sub-PTIME graph transformers. Database Theory - ICDT'95,5th International Conference, Prague, Czech Republic, January 1995, Proceedings. Lecture Notes in Computer Science 893, Springer (1995) 125-138

6. Alexei P. Lisitsa and Vladimir Yu. Sazonov, A-Languages for Sets and LOGSPACE Computable Graph Transformers, Theoretical Computer Science, in press, tentatively v.175, April 1997

7. Alexei P. Lisitsa and Vladimir Yu. Sazonov, On the linear ordering finitely branching graphs and non-well-founded sets, DIMACS Technical Report, 97-05, 12pp.