Элиминация итеративных операторов в некоторых теориях первого порядка Золотов Александр Сергеевич

Содержание к диссертации

Введение

1 Основные определения 14

1.1 Итеративные операторы: синтаксис и семантика 14

1.2 Разрешимость и сложность 17

2 О разрешимости теорий с итеративными операторами 19

2.1 О разрешимости теории с транзитивным замыканием по одной паре переменных 19

2.1.1 Формулы с равенствами 19

2.1.2 Предикаты делимости 25

2.1.3 Звенья разных знаков 32

2.1.4 Неравенства 37

2.1.5 Внешние ограничения 45

2.2 О неразрешимости арифметики Пресбургера и арифметики Ско лема с оператором транзитивного замыкания 60

2.2.1 Арифметика Пресбургера 60

2.2.2 Арифметика Сколема 61

2.3 О разрешимости теории с оператором наименьшей фиксированной точки 66

2.3.1 Экзистенциальные формулы с равенствами 66

2.3.2 Шаблоны разных знаков 74

2.3.3 Предикаты делимости 77

2.3.4 О фиксированной точке для двух кластеров 79

2.3.5 О вложенном операторе наименьшей фиксированной точки 90

2.4 Об одноместном операторе инфляционной фиксированной точки 117

3 Оценки сложности разрешающих алгоритмов для теории с FP оператором 122

3.1 О временой сложности разрешающего алгоритма для теории с оператором наименьшей фиксированной точки 123

3.2 О нижней границе временной сложности разрешающих алгоритмов для теории с оператором наименьшей фиксированной точки

3.2.1 Об экспоненциальном сдвиге 129

3.2.2 О моделировании клеточных автоматов 132

3.2.3 Об экспоненциальном сдвиге посредством экзистенциальных формул 140

Заключение 144

Литература

• Разрешимость и сложность
• Звенья разных знаков
• О разрешимости теории с оператором наименьшей фиксированной точки
• нижней границе временной сложности разрешающих алгоритмов для теории с оператором наименьшей фиксированной точки

Введение к работе

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

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

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

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

^xAho А.V., Ullman J.D. Universality of data retrieval languages. // Proc. of 6th Symp. on Principles of Programming Languages — 1979. — p.110-120.

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

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

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

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

²Fischer, M. J., Rabin M.O. Super-Exponential Complexity of Presburger Arithmetic.// Proceedings of the SIAM-AMS Symposium in Applied Mathematics — 1974 — Vol. 7 — p.27-41

с оператором наименьшей фиксированной точки мы строим оценки временной сложности разрешающего алгоритма.

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

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

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

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

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

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

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

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

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

7. Построен алгоритм эффективной элиминации оператора транзитивного замыкания. Доказана разрешимость теории целых чисел с одной функцией следования и оператором транзитивного замыкания по одной паре переменных.

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

3. Построен алгоритм эффективной элиминации одноместного оператора наименьшей фиксированной точки для экзистенциальных формул. Доказана разрешимость фрагмента теории целых чисел с одной функцией следования и одноместным оператором наименьшей фиксированной точки, где FP-оператор применяется только к экзистенциальным формулам.

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

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

является полной в классе TIME 12 I .

о(п) J

Теоретическая и практическая ценность. Работа носит теоретический характер.

Апробация. Доклады по теме диссертации были сделаны автором в 2013 и в 2016 годах на международной конференции «Актуальные проблемы прикладной математики, информатики и механики» (г. Воронеж) и в 2014 году на международной конференции «Алгебра и математическая логика: теория и приложения» (г. Казань).

Список публикаций автора по теме диссертации включает 9 наименований: [1, 2, 3, 4, 5, 6, 7, 8, 9]. Работы [1, 2, 3, 4, 5] опубликованы в изданиях, входящих в список рекомендованных ВАК ведущих рецензируемых изданий. Работа [6] опубликована в издании, входящем в международные реферативные базы данных и системы цитирования.

Объем и структура работы. Работа состоит из титульного листа, оглавления, трех глав основной части, заключения и списка литературы. Общий объем диссертации составляет 150 страниц. Список литературы включает 36 наименований.

Разрешимость и сложность

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

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

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

Проблеме разрешимости математических теорий посвящены многие работы математиков XX и начала XXI века. Одни из первых неразрешимых теорий найдены в [22], [23] и [32]. Сведения о неразрешимости арифметики со сложением и умножением можно найти в [21] и [32]. В [31] показано, что арифметика Пресбургера с бинарным предикатом делимости неразрешима.

Разрешимость арифметики со сложением, но без умножения была показана Пресбургером в [30], также доказательства этого можно найти в [21]. Одним из основных способов доказательства разрешимости теории является метод элиминации кванторов, он и применяется при доказательстве арифметики Пресбур-гера. Примеры разрешимых теорий также были найдены Тарским: евклидова геометрия и теория вещественно замкнутых полей разрешимы (см. [33]), теория булевых алгебр разрешима (см. [34]).

В работе [13] и [14] доказывается разрешимость обогащений арифметики Пресбургера функциями, эффективно согласованными со сложением, а также редкими предикатами.

Алгоритмические свойства конечных автоматов описаны в [17] и [10]. В работе [20] вводится понятие автоматной структуры и показывается, как можно использовать конечные автоматы для доказательства разрешимости теорий. Показано, что если для всякого предиката системы существует распознающий его конечный автомат, то теория оказывается разрешимой. В работе [35] показано, что существует не являющаяся автоматной алгебраическая система с разрешимой теорией. В работе [11] рассматриваются обогащения автоматных систем рекурсивным оракулом, что позволяет доказать разрешимость теории с предикатом вида U С {2ж,ж Є си}. В работе [12] показана разрешимость слабой монадической теории второго порядка.

Определение и алгоритмические свойства оператора транзитивного замыкания можно найти в [27]. Сведения об операторах фиксированной точки можно найти в [25], [16] и [26]. В [16] показана эквивалентность логики наименьшей фиксированной точки для конечных систем и класса РТІМЕ: с одной стороны, вычисление значения оператора фиксированной точки для конечной системы выполняется за полиномиальное время, с другой, по произвольной машине Тьюринга из класса РТІМЕ строится формула с оператором наименьшей фиксированной точки истинная тогда и только тогда, когда исходная машина принимает свой вход. В работе [26] показана эквивалентность логики частичной фиксированной точки для конечных систем и класса PSPACE. Существенное отличие оператора частичной фиксированной точки от оператора наименьшей фиксированной точки заключается в том, что в последнем случае итеративно строящаяся последовательность отношений не является неубыващей.

Общие сведения об алгоритмической сложности можно найти в [1]. Для того, чтобы оценивать вычислительную сложность тех или иных задач, необходима некая единая модель вычислительной машины. В работе [18] показана полиномиальная эквивалентность естественных формализаций понятия алгоритма. Благодаря данному утверждению мы в данной работе имеем возможность выбрать наиболее удобную для себя модель вычислителя. В данной работе в качестве таковой используется клеточный автомат

Звенья разных знаков

Обозначим такую формулу rjij(x, у). Заметим, что формула rjij(zi, Z2) утверждает существование цепочки от z\ до Z2 ограниченной длины. Также заметим, что после элиминации кванторов каждая из формул щ или окажется тождественно ложной, либо примет вид х = sk ij (y) Л Di{sm ij{x)) для некоторых констант kij и rriij. Из истинности этой формулы тривиально следует истинность оператора транзитивного замыкания, так как есть пусть от ж, до z\, от z\ до Z2 и от z2 до У, значит, есть путь и от ж до у. Покажем следование в другую сторону. Пусть истинно ТІ (Ф(ж,г/)), значит, существует соответствующая цепочка, подтверждающая истинность оператора транзитивного замыкания, причем, в узлах этой цепочки есть повторяющиеся остатки от деления на L. В качестве I{z\) и I(z2) рассмотрим самую далеко отстоящую друг от друга пару-повтор, не содержащуюся в другом повторе. Они найдутся, так как в цепочке повторы есть. Заметим, что в узлах, располагающихся между 1{х) и I{z\) и между I(z2) и 1(у) выполнено следующее: 1. Если некоторый узел на промежутке [/(ж), I{z\)) имеет некоторый остаток от деления на L, то ни один узел на промежутке (/( 2), 1{у)] не имеет того же остатка. Действительно, если бы это было так, то это бы противоречило выбору I(z\) и I(z2). 2. Ни один из остатков узлов на промежутке [I(x),I(zi)) и на промежутке (I(z2),I(y)] не совпадает с остатками I(z\) и /( 2), по той же причине. Таким образом, на промежутке [I(x),I(zi)) и промежутке (I(z2),I(y)] в сумме меньше различных остатков, чем на всей цепочке, тогда, там меньше повторов, значит, истинна формула вида (1) для некоторого значения индекса 0 р\ г и формула вида (2) для некоторого значения индекса 0 р2 г, тогда верна формула (3). Теперь рассмотрим часть цепочки от I{z\) до I{z2). Они имеют одинаковые остатки от деления на L, значит, во-первых, истинна формула (4), а, во-вторых, L делит \I(zi) — I{z2)\, тогда и р делит \I(zi) — I{z2)\. Если часть цепочки от I{z\) до I(z2) имеет не более р звеньев, то она совпадает с цепочкой, по которой была построена одна из щ, значит, верна (5). Если же в этой цепочке больше р звеньев, то есть повторяющиеся остатки от деления на р. Пусть повторяются остатки у щ и у a k. Запишем новую цепочку, до а она будет совпадать с прежней, а после будет та часть, что шла после щ+к. Тогда получим новую цепочку, у которой остаток от деления на р у последнего узла совпадет с таким остатков у прежней цепочки, но звеньев будет меньше. Повторяя данную процедуру, ее можно будет сократить до некоторой цепочки С с количеством звеньев не более р. Заметим, что тогда расстояние между начальным и конечным узлом цепочки С будет кратно р и не будет превышать V. Но тогда расстояние между начальным и конечным узлом цепочки С делит L. Значит, существует цепочка из I(z\) до /( 2), где в качестве звена выступает формула, построенная по С. Заметим, что формула, построенная по С, совпадет с одной из rjij. Значит, истинна и формула (5). Таким образом, мы показали, что будут истинны формулы (3), (4), (5), значит, будет истинной и их конъюнкция.

Будем называть элементарную конъюнкцию вида х = ski{y) Л Dp{smi{x)) возможным звеном, а знак числа ki — знаком соответствующего звена. Будем говорить, что звено с номером і положительно, если ki 0 и отрицательно — если ki 0. В приведенном выше доказательстве мы полагали, что все возможные звенья имели один и тот же знак, то есть были все положительны или все отрицатель ны. Теперь покажем, как можно свести к этому виду случай, когда имеются звенья разных знаков. Лемма 2.1.22. Формула вида у х = s 1{у) A Dp(smi (х)) Тх,у \1 % = s 1{у) A Dp(smi(x)) при р max{\ki\} истинна тогда и только тогда, когда существует цепоч i ка, подтверждающая ее истинность, такая, что все ее узлы находятся в промежутке (тіп(/(ж), 1{у)) — h, тах(/(ж), 1{у)) + h), h = р(р2 + 1). Доказательство. Если 1{х) = 1(у), то утверждение доказано, так как существует путь нулевой длины. Рассмотрим случай, когда 1{х) 1(у). Пусть истинна формула / N \ Тх,у \1 х = s 1{у) Л Dp{smi{x)) , г=1 тогда существует цепочка С, подтверждающая ее истинность. Считаем, что в С нет циклов. Рассмотрим в С наименьший узел, обозначим его amin. Если атіп = /(ж), то все узлы цепочки больше /(ж), и уж тем более больше 1{х) — (р3 + р). Если же amin 1(х), то отложим от 1{х) до amin непересекающиеся отрезки длины р. Пусть на [amin, 1{х)] поместилось ровно г целых непересекающихся отрезков длины р, пронумеруем их числами от 1 до г справа налево. Заметим, что поскольку 1{х) І(у), то в С найдется узел и, такой что 1{х) ии номер и цепочке С больше номера атіп (по крайней мере, 1(у) удовлетворяет всем этим условиям). Поэтому цепочку от 1{х) до и можно разделить на две части: цепочку от 1{х) до amin и от атіп до и. Обозначим эти цепочки С и С" соответственно. Рассмотрим узлы цепочки С", выберем из них монотонно убывающую подпоследовательность {bi)f=l, такую, что Ъ\ = /(ж), а ЬІ+\ — узел с наименьшим номером, такой, что он меньше Ъ{. Последний элемент такой подпоследовательности совпадет с атіп. Построим возрастающую подпоследовательность (Q) =1 по узлам цепочки С": С\ = атоаж, q+i — узел с наименьшим номером, такой, что он больше q. Заметим, что последовательность (pi) обладает следующим свойством: если bi bj, то номер bi в цепочке больше номера bj. Аналогично, если q Cj, то номер q в цепочке больше, чем номер Cj. В

О разрешимости теории с оператором наименьшей фиксированной точки

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

Определение 2.3.2. Пусть FPg(y)(0) — FP-формула. Пусть false —какая-либо ложная в нашей системе формула. Определим семейство формул {FPU, \(ф)}іЄш индукцией по і: О / /\ ±Q rmi+l i\ iQ FPQ(y)W) = false i РРсТ(у)(Ф) = Р ф)

Здесь ф!аіае обозначает результат замены каждой подформулы вида Q[t) в ф на false, а фРі ,,Л – результат замены каждый подформулы вида Q[t) в ф на FP1Q/ \{ф){ї). Содержательно говоря, формула FP1Q/ Аф) описывает этап построения фиксированной точки с номером і. Заметим, что FP1Q/ Аф) является формулой первого порядка для каждого і. Определение 2.3.3. Формулу вида / п \ / т \ ф(х,г,у,у) = /\(УІ = s (ж)) Л Л (х = stj(zj)) Л (v = s (х)), г=1 з=\ кі Є uj,tj Є ш,1 Є Z будем называть шаблоном (простым шаблоном). Величину Н(ф), равную К(ф) + Т(ф), где К(ф) = max{ki : і = 1,п}; Т( ) = maxjt,- : j = l,m} будем называть шириной шаблона. Будем говорить, что шаблон имеет сдвиг, если выполнено одно из двух условий: I 0 и I К(ф) или же I 0 и —I Т(ф); в противном случае, шаблон не имеет сдвига. При I 0 определим величину сдвига шаблона 3(ф) как I — К(ф), в противном случае положим 3(ф) равной I + Т(ф). Обозначим число I через 1(ф). Знаком шаблона будем называть знак его величины сдвига. Всюду далее считаем, что под FP-оператором стоит формула, где проведена элиминация кванторов по всем переменным, кроме тех, которые стоят под символом Q. Также считаем, что формула приведена к дизъюнктивной нормальной форме. Рассмотрим формулу FPg )(0) и запишем ее в виде FPg(w)(0o V ф\) так, чтобы фо не содержала Q, а в каждом дизъюнктивном члене ф\ было хотя бы одно вхождение Q. Далее считаем, что фо и ф\ нетривиальны. Лемма 2.3.4. Пусть формула Ф = FPg(w)(0o V фі)(г,х) такова, что п т Фо = у (v = zi)i Ф\ = V (З і)... (Bv iQivi) Л Л Qivki) Лфі(у\,..., г ,г )), г=1 г=1 где фі — шаблоны одного знака. Тогда существует формула, эквивалентная Ф, и не содержащая FP-оператора.

Доказательство. Для определенности будем полагать, что все шаблоны положительны. Случай с отрицательными шаблонами рассматривается аналогично. Существует конечное число вариантов упорядочений для переменных Zi,..., zn, их можно перебрать, записав конечную дизъюнкцию. Пусть фиксирован некоторый такой вариант упорядочения, для удобства записи пусть он имеет вид z\ z2 zn. Пусть Н = max h(ifji). Определим вспомогательные формулы: і н р н(х, у) = у (х = s\y) V у = s\x))] р н(х, у) = х s (у) V у s (х). г=0 Как нетрудно заметить, первая формула утверждает, что расстояние между х и у не превосходит Н, вторая формула утверждает противоположное.

Будем говорить, что множество точке образует Н-кластер, если расстояние между соседними из них не превосходит Н. При фиксированном упорядочении переменных zi,... , zn существует конечное число вариантов того, какие из значений этих переменных образуют .//-кластеры, поэтому все варианты расположения .//-кластеров можно перебрать, записав конечную дизъюнкцию. Сначала рассмотрим случай, когда выполняется P H{ZUZ2) Л Л p H(zn-hzn). Тогда истинна формула р (п-1)нЫ, zn), то есть расстояние между точками не превосходит (п — 1)Н. Если построение FP длится дольше, чем (п — 1)Н шагов, то непременно появятся точки, которые окажутся больше I(zn). Положим L = max/i( )+max5 ( ) + l. Начнем откладывать отрезки длины L, начиная с I(zn). Будем называть их L-отрезками, обозначим Zi отрезок с номером і. Если процесс построения фиксированной точки длится достаточно долго (более (п — 1)Н шагов), то некоторые из точек каких-то из этих отрезков попадут в множество Q.

Всего существует 2L вариантов принадлежности точек отрезкам длины L. Поэтому если построение FP длится дольше, чем L 2L + (п — \)Н шагов, то среди отрезков {Zi : 1 і 2L + 1} найдутся такие Z и Zi2, на которых расположение множества Q будет одинаковым. Так как при добавлении новых точек учитываются только те из уже построенных, которые располагаются не более, чем на L левее, то далее фрагмент между Z и Zi2 будет повторяться бесконечно. При этом минимальная длина повторяющегося фрагмента заранее неизвестна, но можно утверждать, что она не превосходит L 2L и кратна L, а значит, делит L(2L)!, то есть в отрезке такой длины содержится целое число повторов.

Таким образом, при построении FP, можно выделить следующие этапы: 1. Добавляем точки, лежащие между I(z\) и I(zn). Данный этап длится не более (п — 1)Н шагов. Построение либо завершается, либо переходит к следующему этапу. 2. Добавляем точки правее I(zn), при этом повторов L-отрезков может не быть. Данный этап не может длиться дольше шагов. Построение либо завершается, либо переходит к следующему этапу. 3. Добавление точек правее I(zn), при этом L-отрезки повторяются. Можно утверждать, что фрагмент длины L-(2L)\ повторяется. Данный этап длится бесконечно долго, так как является циклическим. Пронумеруем отрезки слева направо и определим формулы. «х и у имеют одинаковые остатки от деления на L»: /L-l \ V (DL(S%(X)) Л Di{s%{y)) г=0 аь(х,у) = (Di(s%(x)) Л Di{s%{y)) ; г=0 «х принадлежит L-отрезку Zi , если отрезки откладывать от z»: ь /3 (ж, z) = у х = sJ+v (z); 3=1 Пусть R = (n — \)H + L 2L + L (2L)!. Выбор данной константы обусловлен следующими фактами: первый этап построения не может длиться дольше (п — 1)Н шагов, второй - не дольше L 2L, а длину повторяющегося фрагмента можно считать равной L (2L)!.

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

Рассмотрим произвольную проблему Р, для которой нижняя и верхняя оценки временной сложности равны F(0(n)). Примером такой проблемы может служить проблема разрешимости теории иерархий согласованных со сложением функций (см. [15]). В качестве модели вычислительного устройства будем рассмотри клеточный автомат.

Рассмотрим клеточный автомат С, разрешающий Р. Заметим, оценка времени работы М равна F(c\n + С2) для входа длины п и некоторых констант Сі, c i. Тогда требуемая память также ограничена F{c\n + CQ). Без ограничения общности считаем, что С в качестве ответа выдает N или Y. Как и выше, будем пользоваться двухсимвольными кодами: единице будет соответствовать код 10, нулю - код 01.

Наша дальнейшая задача заключается в том, чтобы построить формулу с оператором наименьшей фиксированной точки, которая была бы истинна тогда и только тогда, когда С останавливается на входе X длины п и дает положительный ответ. Пусть в автомате С для клетки существует q различных символов, тогда для двоичной записи номера одного символа достаточно двоичной строки строки длины q = [log2(g)] +1. Поскольку один двоичный символ мы кодируем двумя точками, то на описание символа в одной клетке потребуется 2q точек.

Замечание 3.2.7. Рассмотрим последовательность {Ai(x y)}ieuj из теоремы 3.2.5. Пусть N = 2q(cin + С2), N = С\п + С2. Формула А (х у) истинна тогда и только тогда, когда 1{х) четно и 1(у) = 1{х) + G, где G 2 F(N), при этом, очевидно, G 2q F(Nf), а /еп(Адг) = 0(п).

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

Пусть для построения оператора фиксированной точки используются символ Q и переменная v.

Определение 3.2.8. Пусть Ъ - четное число, w - двоичное слово, А С ш. Будем говорить, что в А с позиции Ъ записан код слова w, если 1. Если w = 0, то Ь їАиЬ + ІєА. 2. Если w = 1, то ЬєАиЬ + ІфА. 3. Если w = aw , \w \ 0, а Є {0,1} то с позиции Ъ в А записан код а, а с позиции Ъ + 2 в А записан код w .

Лемма 3.2.9. Пусть унарное отношение А есть значение для предикатного символа Q. Тогда для всякой непустой конечной двоичной строки w длины п существует формула фш{х) истинная тогда и только тогда, когда отношение 133 А таково, что начиная с точки 1{х) в А записан код w и 1{х) четно. При этом len((j)w) = 0(п). Доказательство. Определим искомые формулы индукцией по \w\. При этом каждая из формул будет иметь один из двух видов: (Зжі)(Ф";(ж, Х\)) для нечетных п и (Эх2){Фт{х,XQ)) для четных п. Для случаев w = 0 и w = 1 формулы строятся непосредственно: ф [х) = (Зх\){х\ = х А 2 2(жі) Л Q(s(xi))), ф [х) = (Зх\){х\ = х Л 2 2(жі) Л Q{x\)). Пусть w = «/О, \w\ = п 1. Если п четно, тогда построенная для w формула имеет вид фт [х) = (Зжі)(Ф"; (х,х\)), в качестве фт рассмотрим формулу фи}{х) = (Зж2)((Зжі)(Ф"; (ж, жі) Л Х і = s {х\) Л Q{s{x2))))-Для нечетных п построенная для w формула имеет вид фт [х) = (Зж2)(Фад (ж,Ж2))5 тогда в качестве фи} рассмотрим формулу фи}(х) = (Зжі)((Зж2)(Ф"; (ж, Х2) /\Х\ = S {Х2) Л Q(s(#l)))). Аналогичным образом рассматривается случай, когда w = w l: вместо Q(s(xi)) или Q(s(x2)) необходимо записать Q{x\) и Q{x2) соответственно. При увеличении длины слова на единицу длина формулы увеличивается на неко торую константу в каждом из случаев, при этом под кванторами используется только две переменных, так что длина результирующей формулы пропорцио нальна длине слова w. Лемма 3.2.10. Для всякой непустой конечной двоичной строки w длины п существует формула i\)w\х, v), обладающая следующим свойством. Зафиксируем значение переменной х и обозначим его Ъ, причем Ъ четно. Пусть теперь А есть множество таких точек а, чтог[)т(Ь а) истинна. Тогда, начиная с позиции Ъ, в А записан коды, а других точек в А нет. При этом len(ifjw) = 0(п).

Доказательство. Определим искомые формулы индукцией по \w\. При этом каждая из формул будет иметь один из двух видов: (3xi)( w(x,v,Xi)) для нечетных п и (3x2){ w{x,v, Х2)) для четных п. Для случаев If = О и If = 1 формулы строятся непосредственно: ф (x,v) = (Зжі)(жі = х Л D i{x\) Л v = s(xi)), ф (x,v) = (Зжі)(жі = х Л 2 2(жі) Л -и = жі). Пусть if = if O, \w\ = n 1. Если n четно, тогда построенная для if формула имеет вид i\)w (x,v) = (3xi)( fw (x,V,X\)), тогда в качестве i\)w рассмотрим формулу i\)w{x v) = {3x i){i 3x\){fyw (ж,г ,жі) V {х і = s {x\) Av = s(x2)))). Для нечетных n построенная для if формула имеет вид l\)W (x,v) = (Зж2)(Фад (x,V,X2)), тогда в качестве фш рассмотрим формулу i\)w{x v) = {Зх\){І Зх і){ Ґ (x,v,X2) V (жі = S (Ж2) Л f = s( i)))). Аналогичным образом рассматривается случай, когда if = if l: вместо v = s(xi) или v = s(x2) необходимо записать v = Х\ и v = Х2 соответствен но. При увеличении длины слова на единицу длина формулы увеличивается на некоторую константу в каждом из случаев, при этом под кванторами ис пользуется только две переменных, так что длина результирующей формулы пропорциональна длине слова if. Определение 3.2.11. Пусть а Є х ,а 0. Двоичную запись числа а из q знаков будем обозначать bin{a,q), q [log2(a)] + 1. Для а = 0 определим Ып(а, q) как последовательность из q нулей. Теперь мы готовы доказать основную теорему статьи. Теорема 3.2.12. Пусть С - клеточный автомат, разрешающий проблему Р, для которой нижняя и верхняя оценки временной сложности равны F(0(n)). Тогда для всякого входного слова X длины п существует формула 0х истинная тогда и только тогда, когда С принимает X. При этом 1еп(Ох) = 0(\Х\) = 0(п).

Доказательство. Пусть в автомате С имеется q 0 различных символов, занумеруем их числами {1,... ,д}. Тогда для записи номеров этих символов достаточно q = [log2(g)] + 1 бит. Пусть все клетки автомата, в которых не записано входное слово, имеют номер символа 1.

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

Запись X на ленте автомата есть в наших обозначениях последовательность 2i,... ап, а,і Є {1,... , q}. Индукцией по п запишем формулу, которая бы говорила, что в начальный момент времени на ленте записан код слова X. Построим формулу stx(v), причем, данная формула будет иметь один из двух видов: (3xi)(Stx(xi,v)) для нечетных п и (3x2)(Stw(x2,v)) для четных п.