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

• Золотов, Александр Сергеевич
• кандидат наук
• 2016

Оглавление диссертации кандидат наук Золотов, Александр Сергеевич

Оглавление

Введение

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

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

Цели работы

Методы исследования

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

Апробация

Структура работы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Заключение

Литература

Введение диссертации (часть автореферата) на тему «Элиминация итеративных операторов в некоторых теориях первого порядка»

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В работе [29] приводится разрешающий алгоритм для арифметики Пресбур-гера с временной сложностью 22 . В работе [24] устанавливается нижняя граница временной сложности для арифметики Пресбургера и аддитивной теории действительных чисел, она оказывается равной 2 и 2 соответственно.

В работе [15] показано, что проблема разрешимости арифметики Пресбурге-

О *

ра с функцией экспоненты имеет временную сложность не менее В работе

О(п)

[28] показана гиперэкспоненциальная сложность проблемы разрешимости слабой монадической теории следования второго порядка. Существование задач с такими большими оценками временной сложности будет использовано нами в дальнейшем для установления нижней границы временной сложности для фрагмента теории с унарным оператором наименьшей фиксированной точки.

Цели работы

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

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

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

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

Методы исследования

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

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

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

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

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

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

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

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

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

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

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

полной в классе Т1МЕ | 22

О(п)

Апробация

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

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

Структура работы

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

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

В главе 2 идет речь об алгоритмических свойствах теорий с итеративными операторами.

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

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

В разделе 2.1.2 мы используем некоторые известные свойства делимости натуральных чисел. При построении пути при помощи оператора транзитивного замыкания мы рассматриваем различные остатки от деления на константу у

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

В разделе 2.1.3 мы рассматриваем такие операторы транзитивного замыкания, в ходе работы которых новая точка может оказаться как слева, так и справа от исходной, то есть допустимы сдвиги в обе стороны. Мы показываем, что если есть некий путь между двумя точками а и Ь , то есть и такой путь, что все его точки не меньше шт(а, Ь) — 1 и не больше тах(а, Ь) + 1 для подходящей константы 1. Используя это обстоятельство, мы показываем, как перейти от сдвигов в обе стороны к сдвигам только в одну сторону.

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

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

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

В параграфе 2.2 мы рассматриваем обогащения арифметики Пресбургера и арифметики Сколема оператором транзитивного замыкания по одной паре переменных и показываем их неразрешимость. Для этого мы показываем представимость сложения и умножения в арифметике Пресбургера с оператором транзитивного замыкания (раздел 2.2.1) и арифметике Сколема (раздел 2.2.2).

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

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

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

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

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

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

В параграфе 3.1 мы показываем, что построенный нами алгоритм элиминации оператора наименьшей фиксированной точки имеет гиперэкспоненциаль-

2

О *

ную сложность, то есть сложность порядка Для этого мы оцениваем,

О(п)

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

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

тогда, когда х делится на 3 и у = х +1 для кратной 3 константы 1, мы записываем формулу с двумя свободными переменными х,у, которая будет истинна

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

В качестве основного результата главы 3 мы формулируем утверждение о полноте проблемы разрешимости фрагмента теории с одноместным оператором наименьшей фиксированной точки, примененным к экзистенциальным форму-

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

тогда и только тогда, когда х делится на 3 и у = (1 + 3) • 2^/3. Затем в раз-

Q.

лам, в классе TIME

Глава 1

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

Будем рассматривать теорию целых чисел с равенством, одноместной функцией следования в, счетным множеством одноместных предикатов делимости От, символом нуля, двухместным предикатным символом <.

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

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

Определение 1.1.1 (см. [27]). Пусть ф (х,у) — формула, при этом наборы переменных х,у совпадают по количеству элементов, не пересекаются и состоят из переменных, свободно входящих в ф. Тогда Тх,у (ф (х,у,х)) — также формула, называемая транзитивным замыканием формулы ф (х,у,х) по переменным х,у. Переменные из набора г будем называть внешними.

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

Рассматривается следующая интерпретация I. Ее областью являются целые числа, то есть каждой переменной ставится в соответствие некоторое целое число. Здесь и далее в работе I(х) — элемент интерпретации, приписываемый переменной х. I приписывает символу 0 нуль, символу в — функцию прибавления единицы. Также I дает определяет истинность бесконечно многих одноместных предикатных символов ..., Оп,... : I предписывает, что Оп(х) истинно

тогда и только тогда, когда п делит I(х). Также I предписывает, что х < у

должно быть истинно тогда и только тогда, когда I(х) меньше I(у), х = у должно быть истинно тогда и только тогда, когда I(х) равно I(у).

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

Определение 1.1.3 (см. [27]). Считаем Т^ (ф (х,у)) истинным, если I(х) = I(у) или если существует последовательность наборов элементов области интерпретации а\,... ,ап, такая, что выполнено

ф(а\,й2) Л ф(а2, аз) Л • • • Л ф(ап-1, ап) Л I(х) = а\ Л I(у) = а,п.

Замечание 1.1.4. Предикат 01(х) истинен для любого х, так как всякое число делится на 1 без остатка.

Определение 1.1.5. Совокупность последовательности а1,...,ап, и форму-

лы

ф(х1,х2) Л ф(х2, х3) Л • • • Л ф(хп-1, хп) Л х = х1 Л у = х

таких, что выполнено

ф(а1,а2) Л ф(а2, аз) Л • • • Л ф(ап-1,ап) Л I(х) = а1 Л I(у) = ап

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

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

Определение 1.1.7. Будем обозначать через вк (х) многократное применение в: в(в(... в(х)...).

к раз

Замечание 1.1.8. В формулах вида х = вк (у) будем допускать отрицательные к. Так, формула вида х = в-к(у), к > 0 является обозначением для вк (х) = у.

п

Определение 1.1.9 (см. [25]). Формулой РР-логики называется формула, построенная по правилам логики первого порядка, а также с помощью оператора инфляционной фиксированной точки РР: если ф(х,у) — формула со свободными переменными х и у, содержащая несигнатурный предикатный символ Q, входящий в ф только положительно, то РРд(у)(ф) — формула исходной сигнатуры со свободными переменными х и у.

Определение 1.1.10 (см. [25]). Пусть А — это алгебраическая система, ф(х,у) — формула, с новым предикатным символом Q, т — количество элементов набора у. Зафиксируем значение переменных х — а € |А|. Определим семейство множеств следующим образом:

Qa = 0; Q?+l = {у € |А|: (ЗД) = ф(а,у)}, для г € и.

Считаем формулу РРд(^) (ф)(а, у) истинной, если существует такой номер п € и, что у € Qn, и ложной в противном случае.

Замечание 1.1.11. Так как символ Q входит в ф положительно, то

Qa ^ Q?+l.

Определение 1.1.12 (см. [25]). Формулой 1РР-логики называется формула, построенная по правилам логики первого порядка, а также с помощью оператора инфляционной фиксированной точки 1РР: если ф(х,у) — формула со свободными переменными х и у, содержащая несигнатурный предикатный символ Q, то 1РРд(у)(ф) — формула исходной сигнатуры со свободными переменными х и у.

Определение 1.1.13 (см. [25]). Пусть А — это алгебраическая система, ф(х,у) — формула, с новым предикатным символом Q, т — количество элементов набора у. Зафиксируем значение переменных х — а € |А|. Инфляционной фиксированной точкой 1РРд(у)(ф)(а) называется множество Qa построенное следующим образом. Пусть

Qa = 0; Qf+l = Qa и {у € |А|: (А, Q?) = ф(а,у)},

для г € и.

Если Оп = Яп+\_ для некоторого п € ш, то полагаем Оа = Qan. Наименьшее п, удовлетворяющее такому условию, назовем степенью оператора 1РРят(ф)(а). В этом случае считаем формулу ГРРд(у)(ф)(а, у) истинной, если у € оа, и ложной, при у € оа.

Если указанного числа п не существует, то считаем, что значение оператора ГРРд(у)(ф)(а) (и формулы ГРРд(у)(ф)(а, у)) не определено.

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

В качестве модели вычислителя нами используется клеточный автомат. В каждый момент времени конфигурация автомата представляет собой бесконечную в обе стороны ленту, где только конечно много ячеек не пусты. Программа автомата представляет собой конечное множество команд вида ав^ ^ 5, где а, в, 7, 5 — символы ленты. Такое правило означает, что если в клетке записан символ в, слева от нее - а, а справа - 7, то заменить символ в рассматриваемой клетке на 5. Для каждой левой части ав7 прорамма должна содержать в точности одно правило. На каждом шаге работы автомата для каждой клетки находится подходящее правило и происходит изменение символа. Заметим, что каждая клетка автомата меняется одновременно со всеми остальными и независимо от них. Считаем, что автомат останавливается, когда лента перестает меняться.

Определение 1.2.1 (см. [1]). Алгоритм А имеет верхнюю оценку временной сложности /, если для всякого входа х длины не более п время работы А на х не превосходит /(п).

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

Определение 1.2.2 (см. [1]). Алгоритм А имеет верхнюю оценку пространственной сложности /, если для всякого входа х длины не более п в ходе работы А на х не более /(п) ячеек ленты клеточного автомата меняют свои состояния.

Алгоритм А имеет нижнюю оценку пространственной сложности /, если

для всякого числа n найдется такой вход x длины не более n такой, что не менее f (n) ячеек ленты клеточного автомата меняют свои состояния во время вычисления A на x.

Определение 1.2.3. Обозначим F(n) функцию гиперэкспоненты, то есть функцию натуральных чисел, определяемую следующими соотношениями

F (0) = 1; F (i + 1) = 2f (i).

В работе рассматривается класс временной сложности TIME(F(O(n))).

Определение 1.2.4. Будем говорить, что задача принадлежит классу сложности TIME(F(O(n))), если для ее решения существует алгоритм с верхней оценкой временной сложности F(O(n)).

Определение 1.2.5 (см. [1]). Будем говорить, что множество A полиномиально сводится к множеству B, если существует рекурсивная функция f, вычислимая за полиномиальное время, такая, что выполняется условие

(Vx)(x е A ^ f (x) е B).

Определение 1.2.6 (см. [1]). Задача X называется полной в классе C (относительно полиномиальной сводимости), если она сама лежит в C и всякая задача из C полиномиально сводится к X.

Список литературы диссертационного исследования кандидат наук Золотов, Александр Сергеевич, 2016 год

Литература

[1] Ахо А. Построение и анализ вычислительных алгоритмов/Ахо А., Хопк-рофт Дж., Ульман Дж.; пер. с английского Слисенко А.О. под ред. Мати-ясевича Ю.В. - М.:Мир, 1979. - 536 с.

[2] Золотов А.С. Применение оператора транзитивного замыкания для формул с одной функцией следования и предикатами делимости. // Вестник ТвГУ. серия Прикладная математика. — 2013. -№15. — с.101-117.

[3] Золотов А.С. О неразрешимости аддитивных и мультипликативных теорий натуральных чисел с оператором транзитивного замыкания. // Вестник ТвГУ. серия Прикладная математика. — 2014. —№3. — с.117-124.

[4] Золотов А.С. Об элиминации оператора фиксированной точки для некоторых формул в теории одного следования. // Вестник ТвГУ. серия Прикладная математика. — 2015. —№4. — с.27-37.

[5] Золотов А.С. О применении конечных автоматов к исследованию разрешимости теории с оператором фиксированной точки. // Вестник ТвГУ. серия Прикладная математика. — 2016. —№1. — с.103-115.

[6] Золотов А.С. О нижней границе временной сложности проблемы разрешимости теории целых чисел с функцией следования и оператором наименьшей фиксированной точки. // Вестник ТвГУ. серия Прикладная математика. — 2016. —№3. — с.97-109.

[7] Золотов А.С. Исследование разрешимости теории с оператором транзитивного замыкания. // Сборник трудов международной конференции «Актуальные проблемы прикладной математики, информатики и механики» / Под ред. д.ф.-м.н А.И. Шашкина — M.: ФИЗМАТЛИТ, 2015, с.117-120.

[8] Золотов А.С. О разрешимости теории целых чисел с оператором транзитивного замыкания. //Материалы конференции «Алгебра и математическая логика: теория и приложения» (г. Казань, 2-6 июня 2014 г.) и сопутствующей молодежной летней школы «Вычислимость и вычислимые структуры». — Казань: КФУ, 2014, с. 176.

[9] Золотов А.С. О нижней границе временной сложности проблемы разрешимости теории целых чисел с функцией следования и оператором наименьшей фиксированной точки. //Сборник трудов международной конференции «Актуальные проблемы прикладной математики, информатики и механики» — Воронеж : Издательство «Научно-исследовательские публикации», 2016, с. 372-374.

[10] Пентус А.Е. Теория формальных языков. / Пентус А.Е., Пентус М.Р. — М.: Изд-во ЦПИ при механико-математическом ф-те МГУ, 2004. — 80 с.

[11] Петров А.Е. Разрешимость теорий обобщений автоматных систем. // Вестник ТвГУ. серия Прикладная математика. — 2010. — №17. — с.21-40.

[12] Рабин М.О. Разрешимость теорий второго порядка и автоматы над бесконечными деревьями. // Кибернетический сборник — 1971 — 8 — с.72-116.

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

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

[15] Снятков А.С. Нижняя граница времени для разрешения теории с функцией экспоненты // Вестник ТвГУ, Серия: Прикладная математика. — 2012 — 2 (25). — с.5-10.

[16] Тайцлин М.А. Языки запросов для баз данных / М.А.Тайцлин —Тверь: ТвГУ, 1999. — 57с.

[17] Трахтенброт Б.А. Конечные автоматы. Поведение и синтез./Трахтенброт Б.А., Барздинь Я.М. — М.: Наука, 1970. — 400 с.

[18] Трахтенброт Б.А. Сложность алгоритмов и вычислений/ Трахтенброт Б.А. — Новосибирск.: изд-во НГУ — 1967.

[19] Aho A.V., Ullman J.D. Universality of data retrieval languages. // Proc. of 6th Symp. on Principles of Programming Languages — 1979. — p.110-120.

[20] Blumensath A. Automatic structures./Blumensath A., Graedel E. // Proc. 15th IEEE Symp. on Logic in Computer Science — 2000. — p.51-62.

[21] Boolos G. S., Computability and logic./Geogre S. Boolos, Richard C. Jefferey. — Cambridge University Press, 1994 — p.397

[22] Church A., A note on the Entscheidungs problem // Journal of Symbolic Logic. — 1936. — №1 — p.40-41;

[23] Church A., An unsolvable problem of elementary number theory // Amer. Journ. of Math. — 1936. — №58 — p.345-363

[24] 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

[25] Gurevich Y., Shelah S. Fixed-point extensions of first-order logic. // Annals of Pure and Applied Logic — 1986 — 32 — p.265-280 .

[26] Gradel E. Finite Model Theory and Descriptive Complexity / Erich Gradel -Aachen: RWTH University. — 2007.

[27] Immerman N. Nondeterministic space is closed under complementation // SIAM Journal on Computing — 1988 — 17 — pp. 935-938.

[28] Meyer A.R. The inherent complexity of theories of ordered sets // Proceedings of the International Congress of Mathematics — 1975 — p. 477-482.

[29] Oppen D.C. A 22 Upper Bound on the Complexity of Presburger Arithmetic //J. Comput. Syst. Sci. — 1978 — 16(3) — p.323-332

[30] Presburger M. Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation

hervortritt/Presburger M.// Comptes Rendus du I congres de Mathématiciens des Pays Slaves. Warszawa — 1929 — p. 92-101.

[31] Robinson J. Definability and decision problems in arithmetic.//The Journal of Symbolic Logic — 1949. — №14 — p.98-114.

[32] Rosser J. B., Extensions of some theorems of Godel and Church // Journal of Symbolic Logic. — 1936. — №1 — p. 87.

[33] Tarski A. A Decision Method for Elementary Algebra and Geometry./Tarski A. — Berkeley, Los Angeles, 1951.

[34] Tarski A. Arithmetical classes and types of Boolean algebras: Preliminary report. // Bull. Amer. Math. Sos. — 1949 — №55 — p. 64.

[35] Tsankov T. The additive group of the rationals does not have an automatic presentation.// The Journal of Symbolic Logic - 2011/ - 76(4) - p. 1341-1351.

[36] Zolotov A.S. On decidability of the theory with the transitive closure operator. // Lobachevskii Journal of Mathematics. — 2015. — Vol. 36(4). — p.434-440.