Выразительная сила языков первого порядка для конечных алгебраических систем над бесконечными универсумами тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ имени М В ЛОМОНОСОВА

МЕХАНИКО-МАТЕМАТИЧЕСКИЙ ФАКУЛЬТЕТ

На правах рукописи УДК 510 67

Дудаков Сергей Михайлович

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

Автореферат

диссертации на соискание ученой степени доктора физико-математических наук

01 01 06 — математическая логика, алгебра и теория чисел

□ОЗОБ4ВСЫ

Москва - 2007

003064876

Диссертация выполнена на кафедре информатики Тверского государственного университета

Научный консультант

доктор физико-математических наук, профессор М А Тайдлин

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

доктор физико-математических наук, профессор А Л Семенов доктор физико-математических наук, профессор А В Чагров доктор физико-математических наук, профессор В Г Дурнев

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

Санкт-Петербургское Отделение Математического Института им В А Стеклова РАН

Защита диссертации состоится 28 сентября 2007 г на заседании диссертационного совета Д 501 001 84 в Московском государственном университете имени M В Ломоносова по адресу 119991, Российская Федерация, Москва, ГСП-1, Ленинские горы, Московский государственный университет имени M В Ломоносова, Механико-математический факультет, ауд 14-08

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета МГУ (Главное здание, 14 этаж)

Автореферат разослан 28 августа 2007 г

Ученый секретарь диссертационного совета Д 501 001 84 при МГУ доктор физико-математических наук, профессор

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

Актуальность. В настоящее время средства и методы математической логики находят все более широкое применение при проектировании и анализе программного обеспечения ЭВМ Одним из наиболее тесно связанных с информатикой разделом математической логики является теория языков первого порядка Особенно интенсивно развивается теория языков для конечных алгебраических систем Это обусловлено тем, что такие языки широко используются в системах управления базами данных, где служат средством извлечения информации из баз данных Сейчас типичной моделью базы данных является предложенная Э Коддом реляционная модель, в которой база данных мыслится как собрание конечного числа конечных таблиц1 Таким образом, состояние базы данных является конечной алгебраической системой некоторой фиксированной сигнатуры, которая называется сигнатурой базы данных Мы будем называть эти алгебраические системы состояниями В качестве языка запросов, с помощью которого происходит извлечение информации, используются различные стилизации языка логики предикатов первого порядка

Хорошо известно, что не всякое свойство алгебраических систем может быть выражено формулами-первого порядка Например, если сигнатура базы данных содержит только один одноместный предикатный символ Р, то невозможно записать в этой сигнатуре формулу первого порядка, выделяющую среди состояний в точности те, в которых количество элементов Р является четным Другой пример для двухместного предиката Е, задающего граф, невозможно написать формулу, которая будет истинной тогда и только тогда, когда этот граф является связным2

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

1Codd ЕРА relational model for large shared data banks // Communications of the ACM, V 13, 1970 P 377-387

Codd Б F Relational completeness of data base sublanguages // Database Systems (ed Rustin R), Prentice-Hall, 1972 P 33-64

2Aho A V , Ullman J D Universality of data retrieval languages // Proc of 6th Symp on Principles of Programming Languages, 1979 P 110-120

одно отношение состояния, называется активной областью состояния

Так как не всякое свойство конечных алгебраических систем может быть выражено формулой языка первого порядка сигнатуры этих систем, то активно ведется поиск методов увеличения выразительной силы Один из путей состоит в следующем3 Обычно, на универсуме, элементы которого хранятся в таблицах, определены какие-либо стандартные отношения, образующие сигнатуру универсума Для числовых множеств такими отношениями являются сложение и умножение, порядок и тд На множестве слов используется конкатенация и лексикографический порядок Таким образом, универсум тоже является алгебраической системой, но, в отличие от состояния, бесконечной

Возможно, что если при построении формул первого порядка использовать не только отношения сигнатуры базы данных, но и отношения универсума (такие формулы называются расширенны ми), то можно будет выразить какие-то свойства, которые невозможно выразить, используя только отношения сигнатуры базы данных (такие формулы называют ограниченными) Разумеется, для сравнения имеет смысл рассматривать только формулы, истинность которых определяется исключительно отношениями сигнатуры базы данных, а не способом связи между этими отношениями и отношениями универсума Иначе говоря, истинность формул, которые используются для сравнения выразительной силы, не должна зависеть от способа вложения состояния в универсум, формулы должны сохранять свою истинность при произвольных изоморфизмах состояния внутри универсума Такие формулы называются =-инвари-а н т н ы м и4 Если для некоторого универсума любая ^-инвариантная расширенная формула эквивалентна ограниченной, то говорят, что для универсума имеет место коллапс к равенству Коллапс к равенству означает, что используемые в расширенных формулах отношения универсума не позволяют выразить никаких новых свойств состояния по сравнению с ограниченными формулами

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

3Kanellakis Р, Kuper G Revesz Р Constramt query languages // Journal of Computer and system sciences, V51, 1995 P 26-52

4 Chandra А , Harel D Computable quenes for relational databases // Journal of compuer and system sciences, V 21(2), 1980 P 156-178

Одним из главных вопросов этого направления является задача сравнения выразительной силы ограниченных и расширенных языков

Ю Ш Гуревич указал свойство состояний, которое нельзя выразить, используя только отношения сигнатуры базы данных, но можно, если добавить к ним произвольный линейный порядок Таким образом, для любых упорядоченных универсумов не выполняется коллапс к равенству Естественно рассматривать следующую задачу какие отношения можно добавить к отношению линейного порядка, чтобы еще увеличить выразительную силу языка7 Поскольку мы будем сравнивать выразительную силу расширенного языка с выразительной силой языка с порядком, то нужно рассматривать не только =-инвариантные формулы, но и те, истинность которых зависит от отношений сигнатуры базы данных и способа упорядочения ее элементов Такие формулы должны сохранять истинность при произвольных сохраняющих порядок изоморфизмах состояний внутри универсума Эти формулы называют <-инвариантными5 Ряд универсумов обладает следующим свойством всякая расширенная <-инвариантная формула эквивалентна некоторой <-ограничен-н о й (то есть формуле с использованием отношений сигнатуры базы данных и порядка) Такое свойство универсума называют коллапсом к порядку6 Известно6, что это верно для арифметики Пресбургера, теории действительных чисел, коммутативных групп и других теорий С другой стороны, имеются неразрешимые теории, в которых это не выполняется, например, арифметика натуральных чисел со сложением и умножением

Свойства коллапса могут быть выражены в виде множества формул первого порядка сигнатуры универсума Поэтому свойствами коллапса обладают не только универсумы, но и их элементарные теории

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

1) возможна ли эффективная трансляция <-инвариантных формул в <-ограниченные6?

2) все ли разрешимые теории обладают свойством коллапса к порядку6?

5Hull R , Yap С К The format model, a theory of database organization // Journal of the ACM, № 31, 1984 P 518-537

6Belegradek О V , Stolboushkm A P , Taitshn M A Extended order-generic queries // Annals of Pure and Applied Logic 97, 1999 P 85-125

3) верно ли то же самое для обогащений арифметики Пресбургера7'''

4) верно ли, что для коллапса к порядку необходимо наличие бесконечного множества без независимой формулы8 ?

В указанных работах предложено много достаточных условий для коллапса к порядку отсутствие независимой формулы, первое и второе свойства изолированности, первое и второе свойства псевдоконечной однородности, сводимость и ограниченность Однако взаимоотношения между этими свойствами оставались во многом неясными Было установлено только, что из отсутствия независимой формулы следуют сводимость и ограниченность, из сводимости и ограниченности следует второе свойство изолированности, а из первого (второго) свойства изолированности следует первое (второе) свойство псевдоконечной однородности Известно также, что первые свойства изолированности и псевдоконечной однородности не совпадают друг с другом Поэтому в (6) также поднят вопрос о том, как соотносятся вышеперечисленные свойства между собой Цели работы

1) Установить, имеет ли место коллапс к порядку в семеновских обогащениях9 арифметики Пресбургера

2) Установить, существуют ли разрешимые теории, в которых коллапса к порядку нет

3) Исследовать случайный граф на предмет свойства коллапса

4) Установить связь между сводимостью, изолированностью, псевдоконечной однородностью и коллапсом к порядку

5) Установить, имеются ли сводимые обогащения арифметики Пресбургера с независимой формулой

6) Разработать методы эффективной трансляции для расширенных <инвариантных формул в <-ограниченные

7Тайцлин М А Ограниченные псевдоконечная однородность и изолированность // Вестник Тверского государственного университета, серия «Прикладная математика», Тверь Тверской государственный университет, 2003 2(1) С 5—15

8Baldwin J , Benechkt М Stability theory, permutations of indiscernibles, and embedded finite models // AMS Trans , 352(11), 2000 С 4937-4969

9 Семенов А Л Логические теории одноместных функций на натуральном ряде // Изв АН СССР, 47(3), 1983 С 623-658

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

Научная новизна и основные положения, выносимые на защиту.

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

1) В обогащениях Семенова арифметики Пресбургера имеет место коллапс к порядку

2) Коллапс к порядку имеет место в предикатных обогащениях начального фрагмента нестандартных моделей арифметики Пресбургера

3) Среди упорядочений случайного графа существуют разрешимые

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

5) Свойство сводимости, второе свойство псевдоконечной однородности и второе свойство изолированности эквивалентны Каждое из них влечет свойство коллапса к порядку

6) Первое свойство изолированности является менее общим чем второе Первое свойство псевдоконечной однородности является менее общим чем второе или эквивалентно ему

7) Если теория имеет эффективно сводимые модели, то она имеет эффективно тотально сводимые модели

8) Если теория имеет эффективно /-сводимую модель и тип неразличимого множества I рекурсивен, то возможно выполнение эффективной трансляции расширенных <-инвариантных формул в ^ограниченные

9) Эффективная трансляция расширенных <-инвариантных формул в <-ограниченные возможна для арифметики Пресбургера, ее эффективных семеновских обогащений, для теории действительных чисел

10) Существуют разрешимые обогащения арифметики Пресбургера, в которых нет коллапса к порядку

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

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

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

Результаты диссертации могут найти практическое применение при анализе языков запросов для систем управления базами данных Апробация работы. Содержание диссертации многократно излагалось на семинаре «Теоретические основы информатики», проходящем в Тверском государственном университете, семинарах МГУ по математической логике под руководством академика РАН С И Адяна и профессора В А Успенского, семинаре ПОМИ РАН по математической логике под руководством члена-корреспондента РАН Ю В Матиясевича Доклад, посвященный одному из разрабатываемых в диссертации вопросов, был сделан на международной конференции по теоретической информатике CSR-2006 [8] (Санкт-Петербург, июнь 2006) и опубликован в сборнике научных трудов «Computer Science — Theory and Applications» (Lecture Notes m Computer Science)

Публикации. Содержание диссертации опубликовано в ведущих рецензируемых журналах, рекомендованных ВАК «Математические заметки» [1] и [4], «Известия РАН Серия математическая» [2], «Успехи математических наук» [3], «Вестник Новгородского государственного университета» [7], «Фундаментальная и прикладная математика»10 Кроме того, имеются публикации в журнале «Вестник Тверского государственного университета» [5, 9] и других изданиях [6]

Список публикаций приведен в конце автореферата Все работы, кроме [3], выполнены без соавторов В [3] автору принадлежит последняя часть седьмого параграфа (теорема 7 5 и предшествующие определения)

10 Дудаков С М Достаточные условия эффективной трансляции локально генериче-ских запросов // Фундаментальная и прикладная математика (в печати)

и параграфы 8, 9, 10 целиком

Структура диссертации. Диссертация содержит 176 страниц, состоит из введения, шести глав основной части, заключения, списка литературы и предметного указателя Список литературы содержит 46 наименований

Краткое содержание работы

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

Система (21,/) обладает первым (вторым) свойством псевдоконечной однородности, если выполнено следующее

1) / — неразличимая в системе 21 (в системе (21,/)) последовательность,

2) для любой специальной системы (21',/') = (21,/), любых псевдоконечных в 21' (в (21,/)) множеств С /', любых конечных множеств Е1,Е% С |21'|, если существует элементарное в 21' (в (21',/')) отображение 1г и Е\ --■> и Е2, то оно может быть продолжено на любой элемент х € |21'|, если система (21',/Эх,£>2, Л) (система (21', /', £>1, /?2, /г)) является ш-насыщенной

Теория Т обладает первым (вторым) свойством псевдоконечной однородности, если она имеет модель 21, в которой есть множество / такое, что (21,1) обладает первым (вторым) свойством псевдоконечной однородности

Система (21,/) обладает первым (вторым) свойством изолированности, если выполнено следующее

1) / — неразличимая в алгебраической системе 21 (в системе (21, /)) последовательность,

2) для любой специальной алгебраической системы (21',/') = (21,/), любого псевдоконечного в 21' (в (21',/')) множества /) С /', любого конечного множества Е С |21'| и любого элемента х € |21'| тип Ьр(х/(В и Е)) изолируется в системе 21' (в системе (21', /')) типом tp(x/G) для некоторого счетного множества С С Ди£

Последнее означает, что тип tp(x/(.D и Е)) является единственным типом в 21' (в (21', /')) над множеством БиЕ, который является расширением типа tp(x/<J?). Теория Т обладает первым (вторым) свойством

изолированности, если она имеет модель 21, в которой есть множество I такое, что (21,1) обладает первым (вторым) свойством изолированности

В (6'7) показано, что из первого (второго) свойства изолированности следует первое (второе) свойство псевдоконечной однородности, из любого свойства псевдоконечной однородности следует коллапс к порядку

Глава 2 Термально изолированные множества

Основным методом изучения свойства коллапса в данной главе являются термально изолированные неразличимые множества Пусть 21 — алгебраическая система сигнатуры I — неразличимое в 21 последовательность Пусть Т — множество всех термов одной переменной сигнатуры £ Назовем множество I термально изолированным в 21, если для любых термов Ь\(х),12{х) е Т имеет место один из двух случаев

1) существует константа М^ € о;, и для всех х £ I выполнено £г(х) ^ <Мг2У

2) для любых элементов х, у & I таких, что х < у, выполнено (х) < < «2(У)

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

Пусть £* = ( и>, 0,1, +, ) какое-либо обогащение арифметики Пресбургера счетной сигнатуры Тогда существует элементарное расширение 21 >- £*, в котором существует неразличимое термально изолированное множество I

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

Важный класс разрешимых обогащений арифметики Пресбургера найден А Л Семеновым (9) Одноместная функция / на множестве натуральных чисел называется согласованной со сложением, если она удовлетворяет следующим условиям

1) для любого натурального п значение f{x) периодично по модулю п для всех х, начиная с некоторого,

2) для всякой неограниченной конечной суммы

s(x) - Ylatf(x+&*)

г

существует такое Е ш, что либо S(x + s's) > f(x) для всех хеш, либо S(x + Sg) < —f(x) для всех хеш,

3) / строго возрастает

Алгебраическая система £sf = (ш, 0,1, +, /), где функция / согласована со сложением, называется арифметикой Семенова Для систем &sf доказывается теорема 2 4

Пусть 21' — специальная модель Th(£,I' С 21' — неразличимая термально изолированная в 21' последовательность, D С I' — псевдоконечное множество в 21', и Е С |21'| — конечное множество, х € 21' Тогда тип tp(x/F), где F = D U Е, изолируется типом tp(x/G) для некоторого счетного G С F

В доказательстве термальная изолированность используется при построении G Далее используется результат A J1 Семенова о приведении любой формулы к экзистенциальному виду После показывается, что любая истинная формула следует из бескванторной формулы с константами из G Как следствие получается теорема 2 5

Теория системы £sf обладает свойством коллапса к порядку

Другой пример использования термально изолированных множеств — предикатные обогащения нестандартных моделей арифметики Пресбур-гера

Пусть теория Т = Th(ш, 0,1, +, (Рг)г), где Рг — произвольные предикаты, допускает элиминацию кванторов Пусть 21 >- (ш, 0,1, +) — элементарное строгое расширение арифметики Пресбургера Изучается теория Т" = Th(2l, (Рг)г) Отмечается следующее свойство (лемма 2 6)

Теория Т' допускает элиминацию кванторов

Доказательство использует элиминацию кванторов в исходной теории Т Доказывается, что элементы термально изолированного неразличимого множества ведут себя как линейно независимые элементы над полем рациональных чисел (лемма 2 7), и, используя это, получается теорема 28

Пусть 93 — произвольная модель Т' Пусть I — произвольное термально изолированное неразличимое множество в 2В, все элементы которого больше w® Тогда система (93,1) обладает первым свойством изолированности

Отсюда легко следует теорема 2 9

Пусть теория Т = ТЬ(ш, 0,1, +, (Pt)t), где Рг — произвольные предикаты, допускает элиминацию кванторов Пусть 21 >->- (о>,0,1,^,+) — элементарное (строгое) расширение арифметики Пресбургера Тогда в теории Т' = Th(2l, (Pi)г) имеет место коллапс к порядку

Глава 3. Случайный граф

Случайны м11 называется граф 0 = (V, Е), обладающий следующим свойством Для любых четырех конечных множеств вершин Ai, Аг, A3, A4, для которых Ai П А2 = As П A4 = 0, существует вершина х такая, что

1) (х,у) € Е для любой вершины у € Ai,

2) (х, у) ^ Е для любой вершины у € Аг,

3) (у,х) G Е для любой вершины у € A3,

4) {у :х) ^ Е для любой вершины у G A4

Ранее показано12 в упорядоченном случайном графе коллапса к порядку нет, теория дискретно упорядоченного случайного графа неразрешима Легко получается следующий результат (теорема 3 2)

Теория случайного графа Th(ö5) не обладает свойством коллапса к равенству, если сигнатура базы данных содержит хотя бы один двухместный предикатный символ

Чтобы показать, что плотное упорядочение случайного графа может быть разрешимо, используется счетность множества Q рациональных чисел Занумеровав их натуральными числами, по индукции строится отношение Е из определения случайного графа таким образом, чтобы элемент

uRado R Universal graphs and universal functions // Acta Arith , № 9, 1964 P 331-340

12Benedict M , Dong G , Libkm L , Wong L Relational expressive power of constraint query languages // Proc 15th ACM Symp on Principles of Database Systems, 1996 P 516

х, удовлетворяющий пунктам 1)—4), существовал на любом непустом открытом интервале Таким образом доказываются следствие 3 3 1

Система (<0>, Е) — случайный граф

и теорема 3 4

Теория системы (<0?, Е, допускает эффективную элиминацию кванторов

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

Если свойство ¿> конечных алгебраических систем не может быть выражено ограниченными формулами, то оно не может быть выражено и формулами расширенной сигнатуры на случайном графе

Для доказательства непосредственно используются игры Эренфойхта Глава 4. Сводимые теории

Формула первого порядка <р(х,у) сигнатуры (£, Р) называется сводимой в системе (21,/) (или просто /-сводимой), где / — неразличимая в 21 последовательность, если существует бескванторная порядковая формула фр(х,2) такая, что в системе (21,/) истинна следующая (£,Р)-формула

(Щ(32 е Р)(Ух е Р)(ф,у) <-> Фг{х,2))

Система (21, /) называется / -сводимой, если каждая формула сигнатуры £ является /-сводимой Теория ТЬ(21) в этом случае тоже называется сводимой Сводимость называется эффективной, если построение формулы ф^ по формуле <-р может быть выполнено алгоритмически Сводимость называется тотальной, если сводимой является каждая формула сигнатуры (£, Р) Теория Т называется (эффективно, тотально) сводимой, если существует (эффективно, тотально) сводимая система (21,/), где 21 |= Г

Система (21,/) называется малой, если 21 является |/|+-насыщенной Ранее показано, что если теория сводима, то существует сводимая малая ее модель

Главный результат первой части данной главы — теорема 4 20

Каждая малая 1-сводимая алгебраическая система является тотально I-сводимой

Для доказательства (параграфы 4 2-4 4) используется механизм вспомогательных формул первого порядка — обобщенных (к, ¿)-формул (к и I — натуральные числа) Показывается возможность некоторых преобразований выполнимых обобщенных (к, £)-формул, при которых они остаются выполнимыми Доказывается, что для выполнимых обобщенных (к, I)-формул к не может быть сколь угодно большим После этого показывается, что все Р-ограниченные кванторы могут вынесены в начало формулы и используются ранее доказанные в работах (8,т) теоремы

Ввиду того, что все перечисленные построения выполняются эффективно, если только исходная сводимость была эффективной, получается следствие 4 20 1

Каждая малая эффективно 1-сводимая алгебраическая система является тотально эффективно I-сводимой

Еще одно следствие — теорема 4 21

Если тип неразличимой последовательности I в эффективно I-сводимой системе (21,1) является рекурсивным и система (21,1) является малой, то тип I в системе (21,1) тоже рекурсивен (в частности, теория системы (21,/) разрешима)

И, наконец, используя результаты, полученные другими авторами, имеем теорему 4 22

Если теория Т сводима, то теория Т обладает вторым свойством изолированности, и, следовательно, в теории Т имеет место коллапс к порядку

Вторая часть этой главы посвящена доказательству обратного результата В начале вводится вспомогательный механизм различающих пар и доказываются вспомогательные теоремы 4 23 и 4 24, основной результат которых — для сводимости элементарных расширений системы необходимо и достаточно, чтобы для каждой формулы количество различающих пар было ограничено

Используя эти результаты, доказывается лемма 4 25 о том, что для несводимых теорий в специальных элементарных расширениях их моделей существуют псевдоконечные множества с определенными свойствами совместности формул над ними Из этого получается теорема 4 26

Пусть теория не имеет сводимых моделей, тогда она не обладает ни первым, ни вторым свойством псевдоконечной однородности

В качестве итога всей главы формулируются теорема 4 27

Если теория обладает первым (вторым) свойством псевдоконечной однородности, то она обладает вторым свойством изолированности

и теорема 4 28

Для любой теории Т следующие утверждения эквивалентны

1) Т обладает вторым свойством псевдоконечной однородности,

2) Т обладает вторым свойством изолированности,

3) Т является сводимой

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

Глава 5. Автоматные системы и их обобщения

Пусть £ = (ш, 0,1, +) — обычная арифметика Пресбургера Добавим в сигнатуру новые одноместный функциональный и одноместный предикатный символы Полученную сигнатуру будем обозначать £д = (0,1, <, +, 4х, И) Обогатим систему £ до системы £д сигнатуры Ед Значением функционального символа будет степень по основанию 4 4х, а значением предиката Я — множество значений гиперэкспоненты по основанию 4 Точнее, определим функцию Н4(х) следующим образом Я4(0) = 0, Я4(х + 1) = 4Я4(ж) Эта функция — гиперэкспонента по основанию 4, а множество ее значений и будет нашим предикатом II Я — {Н^х) По индукции доказывается теорема 5 1

Для каждого натурального р > 1 значение Н4{х) является константой по модулю р, начиная с некоторого х

Используя эту теорему, далее доказывается теорема 5 3

В теории Tr любая формула эквивалентна экзистенциальной формуле, матрица которой является булевой комбинацией предикатов делимости для термов вида v + а и сравнений сумм вида

с + Х^4" + b»v)<

V

где а, Ь, с — константы, а v — переменные из формулы

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

Обогатим сигнатуру константой f) и обозначим полученную сигнатуру = (0,1, +, 4х, R, [)) Будем рассматривать алгебраические системы сигнатуры fif,

= ([0, Ц, Щ,Ьь) ~

начальные фрагменты системы £д, ограниченные числом I) £ й Отношения ^f, и Rfj — обычные ограничения отношений ^ и R на множество [О, Щ Отношение будет ограничением с насыщением обычного сложения, то есть a+t)b = a + b, если a + Ь < f), иначе — a +f, b — f) Аналогично ограничивается экспонента Главным результатом является лемма 5 4

Для каждой формулы <.р сигнатуры fif, можно построить формулу ф(§, f)i) сигнатуры Л ft такую, что

Здесь l)i — элемент R, непосредственно предшествующий I) Более того, можно считать, что все кванторы формулы ф ограничены константой I), и значение каждого встречающегося в ней терма превосходит f) не более чем в два раза

Далее, в лемме 5 5, показывается, что построенная формула ф эквивалентна линейным неравенствам для f) Доказывается лемма аналогично теореме 5 3, только вместо появления новых кванторов оказывается возможным определить значения переменных с помощью явных термов Отсюда получается теорема 5 6

Значение любой формулы на конечной алгебраической системе вида Sf, эквивалентно булевой комбинации линейных неравенств для Ï)

В дальнейшем рассматриваются состояния вида £>[, Свойство состояний, которое исследуется на предмет выразимости

«Состояние является одной из систем вида

порядки iCf, и ^ согласованы, и количе- (1)

ство элементов предиката Щ четно »

Здесь ^ — порядок универсума Очевидно, что если какая-то формула выражает указанное свойство, то она является С-инвариантной, так как свойство свойство (1) не меняется при сохраняющих порядок ^ изоморфизмах состояния внутри универсума Первые два утверждения этого свойства формулами первого порядка выразить можно (лемма 5 7) Из теоремы 5 6 следует теорема 5 8

Свойство (1) нельзя выразить формулами первого порядка сигнатуры (fif,, ни в каком универсуме

Далее рассматривается обогащение арифметики Пресбургера двухместным предикатом Е, предложенное в (7) Каждое натуральное число может быть разложено единственным образом в сумму различных степеней двойки, и х Е у означает, что х — степень двойки, которая входит в разложение у Если х не является степенью двойки, то х у для любого у По любой формуле данной системы £Е = (и>, 0,1, +, Е) может быть построен конечный автомат, распознающий истинность формулы, если ему на вход подать двоичные записи значений переменных Поэтому данная система называется автоматной13 Система эта изоморфна идеалу Фреше счетной атомной булевой алгебры, в которой атомы упорядочены по типу натуральных чисел Оказывается, существует формула ср, обладающая следующим свойством (леммы 5 9 и 5 10)

Если любую систему вида D (, вложить в систему £Е, то формула <р будет определять функцию, которая по каждому элементу множества Щ дает уникальный атом

13Blumensath А , Graedel Б Automatic structures // Proc 15th IEEE Symp on Logic in Computer Science, 2000 P 51-62

Поэтому можно выразить четность R^ (теорема 5 11), поскольку существует формула, выделяющая любое конечное множество атомов

Свойство (1) может быть записано в системе в виде расширенной формулы

Таким образом нами доказана теорема 5 12

В автоматной системе £е коллапса к порядку нет

Это дает ответы на открытые вопросы из статей (6) и (7) (теорема 5 13)

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

Полученному результату можно придать более общую форму и сформулировать достаточные условия, при которых коллапса к порядку в теории нет (теорема 5 14)

Пусть в теории Т сигнатуры Е линейный порядок является дискретным и полным, и имеются две формулы <р(х, у) и ф(х, z), которые обладают следующими свойствами

1) Длина набора х в обеих формулах одинакова

2) Существует определимое в теории Т множество Н, и для любых ух ф у2 существует х £ Н, для которого

Ф 4>{х,у2)

3) Для любого конечного К С Н и любого L С К существует zkl, для которого

(Ух 6 К)(х ф(х, zKl))

Тогда теория Т не обладает свойством коллапса к порядку

Далее рассматриваются обобщения £Е В £Е атомы образуют множество U = {2г г € w} Если взять бесконечное подмножество U* С U, то можно определить отношение Е* i Е* j ö а: Е i/ A i € U* Если существует константа п такая, что для любых а\, а^, ,ап — подряд идущих

атомов и, хотя бы один из них входит в 17*, то такое 17* и соответствующее ему отношение Е* назовем плотными, в противном случае — редкими

Замечая, что если отношение Е* плотно, то с помощью него можно определить Е, мы доказываем теорему 5 15

Если отношение Е* плотно, то в системе (ш, 0,1, +, Е*) коллапса к порядку нет

Сложнее доказать результат для редких отношений Е* (теорема 5 16)

Если отношение Е* является редким, то система , + , Е*) обладает свойством коллапса к порядку

Для этого строятся элементарные расширения, в которых есть термально изолированные множества / специального вида Затем, используя игры Эренфойхта, доказывается, что построенные системы являются /-сводимыми Отсюда следует коллапс к порядку

Формула <р(х, у) называется независимой на множестве X, если следующее утверждение выполняется для любого натурального числа N «существуют наборы а\, ,а¡у € X длины \х\ и для любого К С {1, ,ЛГ} существует набор Ък длины \у\ такой, что для любого г = 1, , N выполнено г е К (р(аг,Ъх) »

Несмотря на коллапс к порядку в системе (а>,0,1,^,+,Е*), имеет место теорема 5 23

В системе (о;,0,1,^,+,Е*) на каждом бесконечном множестве есть независимая формула

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

Глава 6. Эффективная трансляция

Пусть П — сигнатура базы данных Формулу сигнатуры (Г2, Р, в которой все кванторы ограничены по Р, а других вхождений Р нет, назовем Р-формулой Активной называется формула, все кванторы которой ограничены активной областью

Методом последовательного преобразования доказывается лемма 6 1

Пусть ф — Р-формула, а множество I — интерпретация символа Р — является плотно упорядоченным множеством без концевых элементов Тогда <р эквивалентна относительно конечных состояний над I активной <-ограниченной формуле

Способ преобразования является эффективным (следствие 6 11) Используя аналогичный метод, доказывается и лемма 6 2

Пусть система (21,1) сигнатуры (Е, Р) является тотально I-сводимой Тогда всякая расширенная формула эквивалентна в области I формуле вида (Зё € Р)(ф(с) Л 9(с)), где формула ф — в сигнатуре (Е, Р), а в является Р-формулой

Для эффективной сводимости имеет место следствие 6 2 2

Если система (21,1) является малой и эффективно I-сводимой, то по всякой расширенной формуле можно эффективно построить эквивалентную ей в области I формулу вида (Зс е еР)(ф(с)лв(с))

Используя эти леммы и следствия, доказывается теорема 6 3

Пусть система (21,1) эффективно I-сводима и тип последовательности I рекурсивен Тогда по всякой <-инвариантной формуле ¡р в сигнатуре (О,, Е) эффективно строится эквивалентная ей активная формула </?' в сигнатуре (Г2,

Для практического применения теоремы 6 3 формулируются ее более слабый аналог — теорема 6 5

Пусть теория Т сигнатуры Е полна и разрешима Пусть 21 — любая модель Т с неразличимым множеством I, на котором нет независимой формулы и тип которого рекурсивен Тогда по всякой <-инвариантной формуле <р в сигнатуре (ГI, Е) эффективно строится эквивалентная ей активная формула <р' в сигнатуре (О, <)

Множество I без последнего элемента назовем почти неразличимым в алгебраической системе 21, если для каждой формулы ф(х) существует Мф € I такое, что для любых двух одинаково упорядоченных наборов XI е I и х2 е /, все элементы которых больше М-ф, выполнено

21 |= ф(х1) <-» ф(х2) Говоря другими словами, последовательность является почти неразличимой, если каждое условие неразличимости выполняется для всех достаточно больших ее элементов Множество формул, выполняющихся на всех возрастающих последовательностях достаточно больших элементов, назовем типом этой последовательности Почти неразличимую последовательность, на которой нет независимой формулы или выполняется условие эффективной сводимости назовем трансляционным множеством

Используя понятие трансляционного множества, предыдущую теорему можно еще более упростить (теорема 6 7)

Пусть Т — полная разрешимая теория Пусть в некоторой модели 21 теории Т существует трансляционное множество I, тип которого рекурсивен Тогда по каждой <-инвариантной расширенной формуле может быть эффективно построена эквивалентная <-ограниченная формула

Особенно легко находить трансляционные множества для квази-о-ми-нимальных теорий (теорема 6 8)

Пусть Т — полная квази-о-минимальная разрешимая теория Пусть в некоторой модели 21 теории Т существует почти неразличимое множество I Тогда I — трансляционное множество

Используя теоремы 6 7 и 6 8, обнаруживается, что существуют способы эффективной трансляции расширенных формул в эквивалентные им <ограниченные для многих классических теорий Нужно только указать соответствующее трансляционное множество Это решает два открытых вопроса из статьи (6) Теорема 6 10

Существует алгоритм, который по любой < -инвариантной в арифметике Пресбургера расширенной формуле строит эквивалентную ей активную <-ограниченную формулу

Трансляционным является множество факториалов / = {ж1 х € и>} Теорема 6 12

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

Трансляционным является множество степеней двойки, где показателями являются факториалы натуральных чисел I = {2х' х Е ш} Теорема 6 17

Существует алгоритм, который по любой <-инвариантной в системе (с эффективно согласованной со сложением функцией расширенной формуле строит эквивалентную ей активную <-ограниченную формулу

В доказательстве для согласованной со сложением функции / определяется «гиперфункция» Р Р(х + 1) = /(Р(х)'), и показывается, что трансляционным является множество I = хеш}

Более сложное доказательство для арифметики Семенова получается, в частности, из-за того, что арифметика Семенова, в отличие от двух предыдущих теорий, не является квази-о-минимальной (теорема 6 18)

Теория систем £,$ Р не является квази-о-минимальной

Следовательно, для £зр теорема б 8 неприменима

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

Автор выражает огромную благодарность научному консультанту профессору М А Тайцлину за обсуждение полученных результатов Автор благодарит руководителей семинаров, на которых были представлены результаты работы, академика РАН С И Адяна, профессора В А Успенского, члена-корреспондента РАН Ю В Матиясевича и профессора В П Оревкова, а также участников этих семинаров

Список публикаций автора по теме диссертации

[1] Дудаков С М Трансляционный результат для расширений арифметики Пресбургера одноместной функцией, согласованной со сложением // Матем заметки, №76(3), 2004, С 362-371

[2] Дудаков С М Трансляционная теорема для теорий /-сводимых алгебраических систем // Изв РАН Серия матем , №68(5), 2004 С 67-90

[3] Дудаков С М , Тайцлин М А Трансляционные результаты для языков запросов в теории баз данных // Успехи математических наук, №61 2(368), 2006 С 3-66

[4] Дудаков С М Псевдоконечная однородность, изолированность и сводимость // Матем заметки, №81(4), 2007, С 515-527

[5] Дудаков С М Выразительная сила языков запросов первого порядка для баз данных на неупорядоченном случайном графе // Вестник НовГУ №34, 2005 С 51-57

[6] Дудаков С М Трансляционная теорема в предикатных обогащениях начального фрагмента нестандартных моделей арифметики Пресбургера // Сложные системы обработка информации, моделирование и оптимизация, ТвГУ, Тверь, 2002 С 24-37

[7] Дудаков С М Разрешимая теория без трансляционной теоремы // Вестник ТвГУ, серия «Прикладная математика», №6(12), 2005 С 2326

[8] Dudakov S М Isolation and reducibility properties and the collapse result // Proc of mtern conf CSR-2006 (Computer Sciences m Russia, Санкт-Петербург, июнь 2006) LNCS 3967, Springer, 2006 P 171-177

[9] Дудаков С M Трансляционная теорема и автоматные системы // Вестник ТвГУ, серия «Прикладная математика», №4(21), 2006 С 535

филиал ОАО «ТОТ» Кашинская тип , з 444, т 120

Введение

Актуальность.

Обзор литературы.

Цели работы.

Апробация работы.

Структура диссертации.

1 Определения

1.1 Основные обозначения.

1.2 Теории и алгебраические системы.

1.3 Арифметические теории.

1.4 Автоматные системы.

1.5 Свойство коллапса к сигнатуре.

2 Термально изолированные множества

2.1 Определения

2.2 Существование термально изолированных множеств.

2.3 Коллапс к порядку для арифметики Семёнова.

2.4 Свойства предикатных обогащений начального фрагмента нестандартных моделей арифметики Пресбургера.

2.5 Коллапс к порядку для обогащений начального фрагмента нестандартных моделей арифметики Пресбургера.

3 Случайный граф

3.1 Определения.

3.2 Состояния над случайным графом.

3.3 Разрешимое упорядочение случайного графа.

3.4 Монадические сигнатуры.

4 Сводимые теории

4.1 Основные определения.

4.2 Свойства сводимых алгебраических систем.

4.3 (к, /)-формулы

4.4 Тотальная сводимость систем.

4.5 Достаточные условия сводимости.

4.6 Сводимость, изолированность и псевдоконечная однородность

5 Автоматные системы и их обобщения

5.1 Сложное обогащение арифметики Пресбургера.

5.2 Элиминация кванторов в теории Tr.

5.3 Начальные фрагменты системы

5.4 Состояния £>() над системой £Е.

5.5 Обобщения теории ТЕ.

6 Эффективная трансляция

6.1 Достаточные условия эффективной трансляции.

Актуальность

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

Сейчас типичной моделью базы данных является предложенная Э.Коддом реляционная модель, в которой база данных мыслится как собрание конечного числа конечных таблиц (см. [27, 28]). Количество строк в этих таблицах и сами строки могут меняться, но количество столбцов постоянно. Таким образом, база данных может рассматриваться как некоторая конечная сигнатура, а состояние базы данных — как конечная алгебраическая система этой сигнатуры.

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

SQL — сокращение Structured Query Language (язык структурированных запросов). Язык разработан фирмой IBM в 1970 году. В настоящее время является стандартным языком для взаимодействия с системами управления базами данных. запросов предложил использовать язык реляционных выражений, практически эквивалентный языку логики предикатов первого порядка.

Хорошо известно, что не всякое свойство конечных алгебраических систем может быть выражено формулами логики предикатов, то есть не всякая информация может быть получена из базы данных при помощи языков первого порядка. Например, если сигнатура базы данных содержит только один одноместный предикатный символ Р, то невозможно записать в этой сигнатуре формулу первого порядка, выделяющую среди конечных алгебраических систем этой сигнатуры в точности те, в которых количество элементов Р является чётным. Другой пример: для двухместного предиката Е, задающего конечный граф, невозможно записать формулу, которая будет истинной тогда и только тогда, когда этот граф является связным (см. [18]).

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

Так как не всякое свойство конечных алгебраической системы может быть выражено формулой языка первого порядка сигнатуры этой системы, то активно ведётся поиск методов увеличения выразительной силы этих языков. Один из путей состоит в следующем (см. [37]). Обычно, на универсуме, элементы которого хранятся в таблицах, определены какие-либо стандартные отношения. Например, для множеств натуральных или действительных чисел такими отношениями являются операции сложения и умножения, отношение порядка и т.д. Рассматривая множество слов, можно использовать операцию конкатенации или отношение лексикографического порядка. Таким образом, универсум тоже является алгебраической системой, но, в отличие от базы данных, бесконечной. Другое отличие — если состояние базы данных меняется, то универсум является фиксированным.

Можно предполагать, что если при построении формул первого порядка использовать не только отношения базы данных, но и отношения универсума (такие формулы называются расширенными), то в этом расширенном языке можно будет выразить какие-то свойства базы данных, которые невозможно выразить, используя только отношения базы данных (такие формулы называют ограниченными). Разумеется, для сравнения имеет смысл рассматривать только такие формулы, истинность которых определяется исключительно отношениями базы данных, а не способом связи между этими отношениями и отношениями универсума. Говоря другими словами, истинность формул, которые используются для сравнения выразительной силы, не должна зависеть от способа вложения базы данных в универсум. Формулы, обладающими этим свойством, называются локально =-генерическими или =-инвариантными. Если для некоторого универсума любая ^-инвариантная расширенная формула эквивалентна ограниченной, то говорят, что имеет место коллапс к равенству. Таким образом, коллапс к равенству означает, что используемые в расширенных формулах отношения универсума не позволяют выразить никаких новых свойств базы данных по сравнению с ограниченными формулами.

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

Некоторые отношения универсума действительно увеличивают выразительную силу языка первого порядка. Так Ю.Ш.Гуревич продемонстрировал, что примером такого отношения является обычное отношение линейного порядка. Он предложил свойство базы данных, которое нельзя выразить, используя только отношения базы данных, но можно, если добавить к ним произвольный линейный порядок. Иначе говоря, для упорядоченных универсумов не выполняется коллапс к равенству.

Естественно рассматривать следующую задачу:

Какие отношения можно добавить к отношению линейного порядка, чтобы ещё увеличить выразительную силу языка?»

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

Оказывается, что ряд универсумов обладает следующим свойством:

Всякая расширенная <-ипвариантная формула эквивалентна некоторой <-ограничешюй (то есть формуле с использованием только отношений базы данных и порядка).»

Такое свойство универсума называют коллапсом к порядку (или трансляционной теоремой для универсума). Известно, например, что эта теорема верна для арифметики Пресбургера, теории действительных чисел, коммутативных групп и других разрешимых теорий (см. [21, 20, 43]).

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

Диссертация посвящена изучению свойств коллапса и его связи с другими свойствами алгебраических систем, например, сводимостью (см. [19]). Мы изучаем различные универсумы на предмет наличия коллапса. Мы находим примеры систем с разрешимой теорией, в которых коллапс к порядку отсутствует. Так же нами получен метод, который позволяет в некоторых случаях получить эффективное доказательство трансляционной теоремы, то есть построение С-ограниченной формулы эквивалентной С-инвариантной расширенной можно выполнить алгоритмически. Таким образом, мы отвечаем на ряд открытых вопросов, сформулированных и опубликованных разными авторами.

Обзор литературы

Реляционная модель базы данных предложена Э.Коддом в [27, 28]. Там же высказана мысль о том, что для извлечения информации можно использовать алгебру отношений (реляционную алгебру). В своей статье [28] он доказал, что выразительная сила реляционной алгебры не меньше, чем у логики первого порядка. В статье [18] показано обратное: логика предикатов позволяет извлечь любую информацию, которую можно извлечь с помощью операций реляционной алгебры. Таким образом, предложенная Э.Коддом модель языка для извлечения информации из баз данных эквивалентна логике первого порядка.

В [18] показано, что существуют простые свойства алгебраических систем, которые с помощью логики предикатов выразить невозможно. Классическими примерами таких свойств являются чётность количества элементов конечного множества и связность графа. П.Канеллакис с соавторами в [37] высказали идею об использовании в формулах кроме отношений базы данных также отношений универсума, в который база данных вложена. Предполагалось, что использование внешних, «универсальных», не зависящих от базы данных знаний может увеличить выразительную силу языка запросов. Естественно, для сравнения выразительной силы необходимо рассматривать только формулы, истинность которых не зависит от способа вложения базы данных в универсум. Они должны сохранять свое истинностное значение при произвольных изоморфизмах базы данных внутри универсума. Впервые такой класс формул был выделен в статье [26].

В некоторых случаях увеличение выразительной силы действительно возможно. Один из самых замечательных результатов получен Ю.Ш.Гуревичем в 1990 году. Он доказал (см.[20, 9]),2 что наличие среди отношений универсума линейного порядка действительно расширяет множество свойств базы данных, выразимых формулами логики предикатов. Этот результат совершенно не зависит от типа линейного порядка и от того, как при вложении упорядочиваются элементы базы данных.

После получения этого результата стали рассматривать формулы, инвариантные относительно сохраняющих порядок изоморфизмов (см. [39, 21]), и изучать, в каких случаях эти формулы эквивалентны формулам с использованием лишь отношений базы данных и порядка. Сам термин «коллапс к порядку» появился в предварительных вариантах работ [20] и [19]

В работах [33, 34, 21] приведены примеры, когда использование отношений универсума приводит к дальнейшему увеличению выразительной силы языка. В [22] показано, что коллапса к порядку нет в арифметике натуральных чисел со сложением и умножением. Аналогичная этой структура — натуральные числа со сложением и возведением в квадрат, в ней выразимо умножение (см. [24, 43]). Каждая из этих теорий неразрешима. Другой приведённый в [22] пример — упорядоченный универсальный случайный граф, теория которого, как показано там же, неразрешима, если порядок дискретный.

С другой стороны, для многих разрешимых теорий было установлено, что они обладают свойством коллапса к порядку. Так, например, в [21] показано, что коллапс к порядку имеет место для всех о-минимальных теорий (которые были введены в [40, 38, 41]), в частности, для теории действи

2Сам Ю.Ш.Гуревич свои результаты не опубликовал. тельных чисел. Там же продемонстрировано, что коллапс к порядку имеет место в любой системе вида (С/, Pi, Р2,.), где ^ — линейный порядок, a Pi, Р2,. — произвольные одноместные предикаты.

В работе [39] доказано, что трансляция расширенных <-инвариантных формул в <-ограниченные может выполняться эффективно в системе действительных чисел со сложением (К, В [45] этот результат обобщён на произвольные упорядоченные абелевы группы с делением.

В работе [20] О.В.Белеградека, А.П.Столбоушкина и М.А.Тайцлина приведены необходимые и достаточные условия для того, чтобы заданная С-инвариантная формула была эквивалентна <-ограниченной. Далее там приводится несколько достаточных признаков, позволяющих установить для теории свойство коллапса к порядку, в частности, в этой работе введены понятия псевдоконечной однородности и изолированности (позже, в работе [17], эти свойства будут уточнены и названы первыми свойствами псевдоконечной однородности и изолированности соответственно). Доказательства используют теоретико-модельные построения и теорему компактности, из них невозможно получить алгоритм, который выполнял бы построение такой <-ограничеипой формулы. Показано, что первое свойство псевдоконечной однородности является более широким, чем первое свойство изолированности. В качестве открытых проблем в этой работе, в частности, указаны:

Задача 1. Поиск эффективного алгоритма трансляции расширенных <инвариантных формул в <-ограниченные для арифметики Пресбургера (проблема 1).

Задача 2. Верно ли, что для любой разрешимой теории, для которой имеет место коллапс к порядку, существует эффективный алгоритм трансляции (проблема 2)?

Задача 3. Верно ли, что для любого разрешимого обогащения системы натуральных чисел с порядком (ш, имеет место коллапс к порядку (проблема 3)? Высказано предположение, что это верно.

Задача 4. Усиление предыдущего, Верно ли, что если для некоторого обогащения системы (и>, коллапса к порядку нет, то в этом обогащении существует формула ip(x,y), которая способна из любого мноэюества векторов длины выделить произвольное конечное подмножество (проблема 4)? Точнее, для любого мноэюества А = {ai,., а^} наборов натуральных чисел существует вектор Ьа такой, что

Va) (ip (а, Б а) & а е А).

Авторы предполагали, что это имеет место.

Дальнейшие результаты связаны с использованием этих необходимых и достаточных признаков. Например, введённые в [20] первые свойства псевдоконечной однородности и изолированности гарантируют наличие коллапса к порядку для универсума. В [46] предложены более общие условия (21, /)-псевдоконечной однородности и (21, /)-изолировашюсти, из которых следует то же самое. Используя этот метод, в [20] удалось доказать коллапс к порядку для введённых авторами квази-о-минимальных теорий, которые являются обобщениями о-минимальных теорий. В частности, коллапс к порядку был установлен для коммутативных упорядоченных групп и вещественно замкнутых полей.

В работе [16] коллапс к порядку установлен для обогащений арифметики Пресбургера слабо монотонными согласованными со сложением функциями (см. [13]). Там же сформулированы более слабые варианты гипотез из [20]:

Задача 5. Для любого разрешимого обогащения арифметики Пресбургера (о;, 0,1, +) имеет место коллапс к порядку (гипотеза 1).

Задача 6. Если для некоторого обогащения арифметики Пресбургера коллапса к порядку нет, то в этом обогащении существует формула ip (х, у), которая способна из любого множества векторов длины \х\ выделить произвольное конечное подмножество (гипотеза 2). Точнее, для любого множества А = {ai,. наборов натуральных чисел существует вектор bа такой, что

Va) (<р (а, Вд) <=> а Е А).

В [17] кроме первых свойств псевдоконечной однородности и изолированности были введены их аналоги — вторые свойства псевдоконечной однородности и изолированности. Подобно первым свойствам, вторые тоже влекут коллапс к порядку.

Другой подход, который, однако, всё ещё использует неэффективные теоретико-модельные построения, предложен в работе [19] Дж.Болдвина и М.Бенедикта и усовершенствован в [46]. В [19] рассматриваются теории без независимой формулы (о самом понятии независимой формулы можно прочитать в [44]). В этой работе введены /-сводимые алгебраические системы, которые используются как техническое средство для доказательства коллапса к порядку в теориях без независимой формулы, / является неразличимой последовательностью в алгебраической системе. В [19] показано, что каждая теория, в которой отсутствует независимая формула, имеет /-сводимые модели. В работе в виде открытого вопроса высказана следующая задача:

Задача 7. Верно ли, что кол/ianc к порядку для универсума имеет место тогда и только тогда, когда в нём существует бесконечное определимое множество без независимой формулы?

Основной целью работ [46] и [17] было доказательство того, что определённый класс теорий (имеющих /-сводимые модели, в которых каждая формула эквивалентна Р-ограниченной формуле) обладает свойством коллапса к порядку. Однако для доказательства этого в [46] и [17] использовано не только свойство /-сводимости моделей, но и ещё одно условие: каждая формула должна быть эквивалентна Р-ограниченной формуле. В работе [19] показано, что существование таких моделей также следует из отсутствия в теории независимой формулы. Но связи между этим свойством и /-сводимостью в [19] так и не было найдено. Осталась не установленной и связь между псевдоконечной однородностью, сводимостью и отсутствием независимой формулы, что было отмечено в [20].

В работах А.Л.Семёнова [14, 15] доказано, что обогащение арифметики Пресбургера согласованными со сложением предикатами и функциями разрешимы, если «согласование» осуществляется эффективно. К таким функциям относятся, найример, показательная функция по натуральному основанию или факториал числа.

Понятие (универсального) случайного графа введено в работе [42]. В [23, 22] показано, что для упорядоченного универсального случайного графа свойство коллапса к порядку отсутствует. Если база данных содержит одноместный предикат, то возможно записать чётность количества его элементов. Хорошо известно (см., например, [24]), что дискретное упорядочение случайного графа не разрешимо, он не может служить опровержением гипотез о коллапсе к порядку для разрешимых теорий (задачи 3, 4). После опубликования работы автора [7] О.В.Белеградек (в устной форме) сформулировал следующую задачу.

Задача 8. Имеет ли место коллапс к равенству для неупорядоченного случайного графа?

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

Одним из интереснейших достижений последнего времени в области арифметических теорий явилось оригинальное обогащение арифметики Пресбургера, предложенное в [25] А.Блюменсатом и Э.Гределем. Это обогащение разрешимо и, в то же время, имеет независимую формулу (чем была опровергнута гипотеза из [19], что таких обогащений не существует). В построенной системе каждая формула эквивалентна (в определённом смысле) некоторому конечному автомату и наоборот, поэтому введённые в [25] системы названы автоматными. В [17] предложено аналогичное обогащение при помощи предиката Е (см. определение в главе 1) и показано, что такое обогащение не обладает свойствами изолированности. Далее, в [17] ставится следующий вопрос.

Задача 9. Обладает ли теория системы (и>, Е) свойством коллапса к порядку?

Цели работы

1) Установить, имеет ли место коллапс к порядку в семёновских обогащениях арифметики Пресбургера.

2) Установить, существуют ли разрешимые теории в которых коллапса к порядку нет (задачи 3, 4),

3) в частности, установить, есть ли такие системы среди обогащений арифметики Пресбургера (задачи 5, 6),

4) в частности, установись, имеет ли место коллапс к порядку для системы (ш, Е) (задача 9).

5) Детально исследовать случайный граф на предмет свойства коллапса (задача 8).

6) Установить связь между сводимостью, изолированностью, псевдоконечной однородностью и коллапсом к порядку.

7) Установить, имеются ли сводимые обогащения арифметики Пресбургера с независимой формулой (задача 7).

8) Разработать механизмы эффективной трансляции для расширенных <инвариантных формул в <-ограниченные (задачи 1, 2).

Апробация работы

Содержание диссертации опубликовано в журналах: «Математические заметки» (см.[3, 4]), «Известия РАН. Серия математическая» (см.[6]), «Фундаментальная и прикладная математика» (см.[10]), «Успехи математических наук» (см.[9]), «Вестник Тверского государственного университета» (см.[7, 11]), «Вестник Новгородского государственного университета» (см. [8]), других изданиях (см. [5]).

Содержание диссертации многократно излагалось в 2001-2006 годах на семинаре «Теоретические основы информатики», проходящем в Тверском государственном университете, семинаре по математической логике Московского университета, семинаре по математической логике Санкт-Петербургского отделения математического института РАН.

Доклад, посвящённый одному из разрабатываемых в диссертации вопросов, был сделан на международной конференции по теоретической информатике CSR-2006 (Санкт-Петербург, июнь 2006, см. [29]).

Структура диссертации

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

Основные результаты

В работе доказаны следующие основные утверждения.

1) В обогащениях арифметики Пресбургера одноместной согласованной со сложением функцией или предикатом имеет место коллапс к порядку.

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

3) Для случайного графа, на котором коллапса к порядку нет, существуют разрешимые упорядочения.

4) Для неупорядоченного случайного графа коллапс к равенству имеет место тогда и только тогда, когда сигнатура базы данных является мона-дической. Это даёт исчерпывающий ответ к задаче 8.

5) Свойство сводимости, второе свойство псевдоконечной однородности и второе свойство изолированности эквивалентны. Каждое из них влечёт свойство коллапса к порядку.

6) Первое свойство изолированности является менее общим чем второе. Первое свойство псевдоконечной однородности является менее общим чем второе или эквивалентно ему.

7) Если теория имеет эффективно сводимые модели, то она имеет эффективно тотально сводимые модели.

8) Если теория имеет эффективно /-сводимую модель, и тип неразличимого множества / рекурсивен, то возможно выполнение эффективной трансляции расширенных <-инвариантных формул в <-ограничеиные. Таким образом получен частичный ответ на открытый вопрос 2 из работы [20] (задача 2).

9) Эффективная трансляция расширенных С-инвариантных формул в <ограниченные возможна для арифметики Пресбургера, её эффективных семёновских обогащений, для теории действительных чисел. Это даёт утвердительный ответ на открытый вопрос 1 из работы [20] (задача 1).

10) Существуют разрешимые обогащения арифметики Пресбургера, в которых нет коллапса к порядку. Таким образом получен отрицательный ответ на открытые вопросы 3 и 4 из работы [20] (задачи 3, 4), опровергнуты гипотезы 1 и 2 из [16] (задачи 5, 6), и дай отрицательный ответ на вопрос из [17] (задача 9).

11) Существуют обогащения арифметики Пресбургера, в которых есть коллапс к порядку, но всякое бесконечное множество имеет независимую формулу. Таким образом получен отрицательный ответ на открытый вопрос из [19] (задача 7).

Направления дальнейших исследований

Мы опровергли несколько предположения из работ [20] и [16]. Однако видим, что при построении контрпримера (свойство (5.9)) получается формула с использованием многоместных отношений, и это существенно используется в доказательствах. Поэтому представляет интерес исследование выразительной силы языка первого порядка в системе £Е, когда база данных содержит лишь одноместные предикаты, в частности, один одноместный предикат. В главе 3 мы показали, что такое ограничение может играть решающую роль.

В связи с этим мы можем переформулировать предположения 3 и 4 из работы [20] и гипотезы 1 и 2 из [16] в виде следующего вопроса.

Вопрос 1. В любом ли разрешимом обогащении арифметики Пресбургера невозможно выразить чётность количества элементов произвольного одноместного конечного предиката?

Верно ли, что если в обогащении арифметики Пресбургера возможно выразить чётность количества элементов произвольного одноместного конечного предиката, то в таком расширении существует формула (р(х, у), способная выделить из произвольного конечного множества любое подмножество?

Еще один вопрос заключается в следующем.

Вопрос 2. Существуют ли разрешимые обогащения арифметики Семёнова, в которых пет коллапса к порядку? В частности, существуют ли такие обогащения для системы (и, 0,1, +, 2х) ?

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

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

Вопрос 3. Существуют ли разрешимые обогащения системы £Е, в которых нет коллапса к ?

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

Вопрос 4. Существуют ли теории, которые обладают свойством коллапса к порядку, но не имеют при этом сводимых моделей? Другими словами, являются ли свойства псевдоконечной однородности, изолированности и сводимости необходимыми для коллапса к порядку?

Заключение

1. Булос Дж., Джеффри Р. Вычислимость и логика. М.: Мир, 1994.

2. Верещагин Н.К., Шень А. Языки и исчисления. М.: МЦНМО, 2000.

3. Дудаков С.М. Трансляционный результат для расширений арифметики Пресбургера одноместной функцией, согласованной со сложением // Матем. заметки, №76(3), 2004, С.362-371.

4. Дудаков С.М. Псевдоконечная однородность, изолированность и сводимость // Матем. заметки, №81(4), 2007, С.515-527.

5. Дудаков С.М. Трансляционная теорема в предикатных обогащениях начального фрагмента нестандартных моделей арифметики Пресбургера. // Сложные системы: обработка информации, моделирование и оптимизация, ТвГУ, Тверь, 2002. С.24-37.

6. Дудаков С.М. Трансляционная теорема для теорий /-сводимых алгебраических систем // Изв. РАН. Серия матем., №68(5), 2004. С.67-90.

7. Дудаков С.М. Выразительная сила языков запросов первого порядка для баз данных на неупорядоченном случайном графе. // Вестник НовГУ. №34, 2005. С.51-57.

8. Дудаков С.М. Разрешимая теория без трансляционной теоремы. // Вестник ТвГУ, серия «Прикладная математика», №6(12), 2005. С.23-26.

9. Дудаков С.М., Тайцлин М.А. Трансляционный результат для языков запросов в теории баз данных. // Успехи математических наук, №61:2(368), 2006. С.2-65.

10. Дудаков С.М. Достаточные условия эффективной трансляции локально генерических запросов // Фундаментальная и прикладная математика (принято к публикации)

11. Дудаков С.М. Трансляционная теорема и автоматные структуры // Вестник ТвГУ, серия «Прикладная математика», №4(21), 2006. С.5-35.

12. Кейслер Г., Чен Ч.Ч. Теория моделей. М.: Мир, 1997.

13. Попов И.В. Элиминация кванторов в некоторых обогащениях арифметики Пресбургера. // Сложные системы: обработка информации, моделирование и оптимизация, ТвГУ, Тверь, 2002, С.38-47.

14. Семёнов A.JI. О некоторых расширениях арифметики сложения натуральных чисел. // Изв. АН СССР, 43(5), 1979. С.1175-1195.

15. Семёнов A.JI. Логические теории одноместных функций на натуральном ряде. // Изв. АН СССР, 47(3), 1983. С.623-658.

16. Тайцлин М.А. Трансляционные результаты в теории баз данных. // Сложные системы: обработка информации, моделирование и оптимизация, Тверь: Тверской государственный университет, 2002. С.5-23.

17. Тайцлин М.А. Ограниченные псевдоконечная однородность и изолированность. // Вестник Тверского государственного университета, серия «Прикладная математика», Тверь: Тверской государственный университет, 2003. 2(1). С.5-15.

18. Aho A.V., Ullman J.D. Universality of data retrieval languages. // Proc. of 6th Symp. on Principles of Programming Languages, 1979. P. 110-120.

19. Baldwin J., Benedikt M. Stability theory, permutations of indiscernibles, and embedded finite models. // AMS Trans., 352(11), 2000. C.4937-4969.

20. Belegradek O.V., Stolboushkin A.P., Taitslin M.A. Extended order-generic queries. // Annals of Pure and Applied Logic 97, 1999. P.85-125.

21. Benedict M., Dong G., Libkin L., Wong L. Relational expressive power of constraint query languages. // Proc. 15th ACM Symp. on Principles of Database Systems, 1996. P.5-16.

22. Benedict M., Libkin L. Expressive power: the finite case. // Constraint databases, Berlin: Springer-Verlag, 1996. P.55-87.

23. Benedict M., Libkin L. Languages for relational databases over interpreted structures. // Proc. 16th ACM Symp. on Principles of Database Systems, 1996. P.25-39.

24. Bes A. A survey of arithmetical definability. //A tribute to Maurice Boffa, Soc. math, belgique, 2002. P. 1-54.

25. Blumensath A., Graedel E. Automatic structures. // Proc. 15th IEEE Symp. on Logic in Computer Science, 2000. P.51-62.

26. Chandra A., Harel D. Computable queries for relational databases. // Journal of compuer and system sciences, V.21(2), 1980. P. 156-178.

27. Codd E.F. A relational model for large shared data banks. // Communications of the ACM, V.13, 1970. P.377-387.

28. Codd E.F. Relational completeness of data base sublanguages. // Database Systems (ed. Rustin R.), Prentice-Hall, 1972. P.33-64.

29. Dudakov S.M. Isolation and reducibility properties and the collapse result. // Proc. of intern, conf. CSR-2006 (Computer Sciences in Russia, Санкт-Петербург, июнь 2006). LNCS 3967, Springer, 2006. P.171-177.

30. Ehrenfeucht A. An application of games to the completeness problem for formalized theories. // Fundarnenta Matematicae, № 49, 1961. P.129-141.

31. Erdos P., Spencer J. Probabilistic methods in combinatorics. // New York: Academic Press, 1974.

32. Frai'sse R. Sur quelques classifications des systemes de relations. // Universite d'Alger, Publications Scientifiques, Serie A, № 1, 1954. P.35-182.

33. Grumbach S., Su J. Dense order constraint databases. // Journal of computer and sysem sciences, 55(2), 1997. P.273-298.

34. Grumbach S., Su J., Tollu C. Linear constraint databases. // Proc. of intern, conf. LCC-94 (Logic and computational complexity), LNCS 960, Springer, 2006. P.426-446.

35. Hodges W. Model theory. Cambridge: Cambridge university press, 1993.

36. Hull R., Yap C.K. The format model, a theory of database organization. // Journal of the ACM, № 31, 1984. P.518-537.

37. Kanellakis P., Kuper G. Revesz P. Constraint query languages. // Journal of compuer and system sciences, V.51, 1995. P.26-52.

38. Knight J.F., Pillay A., Steinhorn C. Definable sets in ordered structures II. // AMS Trans, №295(2), 1986. P.593-605.

39. Paradaens J, Van den Bussche J, Van Gucht D. First-order queries on finite structures over real. // Proc. 10th IEEE Symp. on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1995. P.79-87.

40. Pillay A, Steinhorn C. Definable sets in ordered structures I. // AMS Trans, №295(2), 1986. P.565-592.

41. Pillay A., Steinhorn C. Definable sets in ordered structures III. // AMS Trans., №309(2), 1988. P.469-476.

42. Rado R. Universal graphs and universal functions. // Acta Arith., jV 9, 1964. P.331-340.

43. Schweikardt N. On the expressive power of first-order logic with built-in predicates. Berlin: Logos-Verlag, 2002.

44. Shelah S. Classification theory and the number of non-isomorphic models (2nd ed. revised). Amsterdam: North Holland, 1990.

45. Stolboushkin A.P., Taitslin M.A. Linear vs. order constraint queries over relational databases. // Proc. 15th ACM Symp. on Principles of Database Systems, 1996. P.17-27.

46. И7 б, 55 £, 25 £Е, 30 £д, 105 £sf, 27 £sp, 27автоматная, 28 малая, 68 насыщенная, 23специальная, 23 тотально /-сводимая, 69 эффективно, 69 арифметика

47. С-ограниченпая, 32 Щ, 117 £л, 25 30 EG, 55 Еп, 10526 26