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

Снятков Алексей Сергеевич

Разрешимость теорий иерархий

согласованных со сложением функций

Специальность 01.01.06 математическая логика, алгебра

и теория чисел

Автореферат

диссертации на соискание учёной степени

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

Ярославль 2012

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

Научный руководитель доктор физико-математических наук, доцент Дудаков Сергей Михайлович

Официальные оппоненты : Соколов Валерий Анатольевич, доктор физико-математических наук, профессор, заведующий кафедрой теоретической информатики Ярославского государственного университета им. П. Г. Демидова Чагров Александр Васильевич, доктор физико-математических наук, профессор кафедры функционального анализа и геометрии Тверского государственного университета

Ведущая организация Московский государственный университет им. М. В. Ломоносова

Защита состоится 23 ноября 2012 г. в 1400 часов на заседании диссертационного совета Д 212.002.03 при Ярославском государственном университете им. П. Г. Демидова по адресу: Российская Федерация, 150008, Ярославль, ул. Союзная, 144, ауд. 426.

С диссертацией можно ознакомиться в библиотеке Ярославского государственного университета им. П. Г. Демидова.

Автореферат разослан октября 2012 г.

Ученый секретарь Яблокова диссертационного совета Светлана Ивановна

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

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

Этим вопросом стали заниматься примерно с середины двадцатых годов 20 века. В начале и середине тридцатых годов были получены знаменитые теоремы Гёделя о неполноте и результат Чёрча о неразрешимости.

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

Одно из направлений исследований поиск разрешимых обогащений арифметики Пресбургера. Один из наиболее значительных результатов был получен А.Л.Семеновым. Он рассматривал расширение арифметики Пресбургера редкими предикатами1 и функциями, согласованных со сложением2, которые были введены также им. А.Л. Семёнов доказал, что оба варианта обогащения являются разрешимыми. Дудаковым С.М.3 было рассмотрено одновременное обогащение арифметики Пресбургера одноместным функциональным и одноместным предикатным символами, и показано, что такая теория допускает элиминацию кванторов. Из других результатов, связанных с функцией экспонеты, можно выделить следующий: если гипотеза Шануэля для действительных чисел верна, то теория поля действительных чисел с экспонентой является разрешимой4.

Исторически первым и до сих пор являющимся основным методом доказательства разрешимости является метод эффективной элиминации кванторов, это алгоритмический процесс, порождающий по заданной логической формуле другую, эквивалентную ей формулу, свободную от вхоСемёнов А.Л. О некоторых расширениях арифметики сложения натуральных чисел. // Изв. АН СССР, 43(5), 1979. С.1175–1195.

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

Дудаков С.М. Трансляционная теорема и автоматные структуры. // Вестник ТвГУ сер. Прикл.

матем., 4(21), 2006. С. 5–35.

Macintyre A.J., Wilkie A.J. On the decidability of the real exponential eld, Kreisel 70th Birthday Volume, ждений кванторов. Элиминация кванторов далеко не всегда возможна, но когда это так, алгоритм элиминации кванторов приносит исключительную пользу для исследователя, так как вскрывает структуру теории и её моделей. При использовании метода элиминация кванторов, часто требуется расширение сигнатуры, что показывает выразительную силу таких теорий.

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

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

При изучении сложности алгоритма нужно остановиться на какомнибудь определённом уточнении понятия алгоритма. В качестве разрешающих процедур обычно выбирают алгоритмы, представленные в виде машины Тьюринга, так как сложность разрешающих процедур на машинах Тьюринга отличается от других моделей алгоритма не более чем на полином. Фишер и Рабин5 нашли достаточные условия для доказательства трудности задач разрешения теорий в различных классах сложности. В частности, ими показано, что разрешающая процедура для арифметики Fischer, M. J., and Rabin M.O., Super-Exponential Complexity of Presburger Arithmetic.// Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7, 1974, 27– Пресбургера обладает сложностью по меньшей мере 22. Там же установлено, что разрешающая процедура для теории вещественно замкнутых полей обладает сложностью по меньшей мере 2n. Однако, эту оценку точной назвать пока нельзя: Oппенен6 показал, что для арифметики Пресбургера существует разрешающий алгоритм, который работает шагов и вопрос о том какая оценка точнее пока открыт.

Цели работы. Данная работа посвящена исследованию свойств теорий вида:

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

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

1. Доказано, что если все функции являются периодичными по любому натуральному модулю, то любая формула в теориях Tf эквивалентна экзистенциальной. Следовательно, эти теории являются модельно полными. Показано, что преобразование каждой формулы к экзистенциальной может быть эффективным, если все гиперфункции являются эффективно периодичными по любому натуральному модулю. Установлено, что если обогатить теорию обратными для fi функциями, то получается теория с элиминацией кванторов. Элиминация будет эффективной при упомянутом выше условии. Таким образом, при выполнении условия эффективной периодичности гиперфункций, теории являются разрешимыми.

Derek C. Oppen: A 22 Upper Bound on the Complexity of Presburger Arithmetic. J. Comput. Syst.

Sci. 16(3): 323-332, 2. Установлено, что если функция f0 периодичная по любому модулю p > 1 с периодом меньше p, то гиперфункция от f0 является эффективно периодичной по любому модулю p > 1 с периодом 1. Также установлено, что если функция f0 периодичная по любому модулю p > 1 с периодом меньше p, а функция f1 (x) периодичная функция, то гиперфункция от функции f (x) + f1 (x) является периодичной по модулю p для любого p > 1. Следовательно, теории, для которых выполняется одно из двух условий, являются разрешимыми.

3. Показано, что представленный в работе разрешающий алгоритм для любой формулы длины n для определения её истинности в Tf требует памяти не больше чем 22. Следовательно, разрешающий алгоритм 4. Предложен метод кодирования последовательности с помощью бинарного дерева. Используя этот метод, доказано, что для любого разрешающего алгоритма существует формула длины n, для которой время работы алгоритма, определяющего истиность формулы в Tf, будет не меньше чем 22. Таким образом, задача разрешения указанных теоO(n) раз Теоретическая и практическая ценность. Работа носит теоретический характер. В ней используются методы математической логики, теории алгоритмов и теории сложности.

Апробация работы. Начиная с 2006 года содержание глав данной диссертации неоднократно докладывалось на семинаре Теоретические основы информатики в ТвГУ.

Доклад по теме диссертации был сделан в 2008 году в СанктПетербургском отделении Математического института им.В.А.Стеклова РАН на семинаре по математической логике под руководством академика РАН Ю.В.Матиясевича.

Также доклад по теме диссертации был сделан в 2011 году на международной конференции Актуальные проблемы прикладной математики, информатики и механики (Воронеж).

Исследования по теме работы были поддержаны РФФИ, проект № 08-01-00241-а.

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

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

Объем и структура работы. Диссертация состоит из титульного листа, оглавления, четырёх глав основной части, заключения и списка литературы. Общий объем диссертации составляет 83 страницы. Библиография включает 46 наименований.

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

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

Функция f является эффективно периодичной, если для любого натурального p функция f периодична по модулю p с периодом, который определяется эффективно по p. Если для функции f выполняются следующие условия:

(1) f периодична по модулю n для всех n, n 2;

(2) для всякой неограниченной конечной суммы существует такое, что либо S(x + ) > f (x) для всех x, (3) f монотонно возрастает, то она называется согласованной со сложением. Если константы в пунктах (1) и (2) находятся эффективно, то f называется эффективно согласованной со сложением.

Последовательности функций fi, где i называется иерархией функций fi, если fi является гиперфункцией от fi1, то есть определяется так, что fi+1 (x + 1) = fi (fi+1 (x)).

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

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

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

tji (v, ai, ai+1,..., aj ) = fi (fi+1 (... (fj1 (fj (v + aj ) + aj1 )... ) + ai+1 ) + ai ), где i j, все ak константы. Затем доказываются для них ряд важных в дальнейшем свойств (леммы 7–10).

В третьей главе исследуются свойства теории Tf. В параграфе 3.1 доказывается следующая основная теорема:

Теорема 1. Если f0 согласована со сложением и все fi периодичны по модулю p для любого натурального p, то в теории Tf любая формула эквивалентна экзистенциальной формуле, матрица которой является булевой комбинацией предикатов делимости и сравнений сумм вида где все ak, bi, c, d константы, v переменные из формулы.

Для доказательства теоремы демонстрируется, что формула вида эквивалентна экзистенциальной, если бескванторная формула, причем при этом преобразовании, матрица формулы не теряет нужного нам вида. Для этого модифицируется метод А.Л. Семёнова. Отмечается, что Qj (ti0 (u, a0, a1,..., ai ))+a) эквивалентна булевой комбинации формул вида Qk (u + b) для некоторых k и b и некоторых линейных неравенств для u. В лемме 11 доказывается, почему можно ограничиться рассмотрением термов вида bti0 (v, a0, a1,..., ai ) и cv. Далее каждое неравенство из приводится к виду где суммы sk содержат только слагаемые с переменными xi, а суммы rk и wk таких слагаемых не содержат. Далее термы по каждой переменной группируются в суммы, вида Среди всех таких сумм выбирается максимальная по величине. Пусть sk остаток суммы sk (без ). Возможны две ситуации:

1. по модулю превосходит каждое sk не менее чем в два раза, 2. по модулю меньше 2sk для некоторого k.

Используя леммы 1–10, показывается, что в первом случае количество элиминируемых кванторов можно уменьшить, добавляя новые кванторы существования перед отрицанием, а во втором сократить их количество, используя вместо кванторов дизъюнкцию.

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

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

Следствие 1. Если функция f0 согласована со сложением и все функции fi периодичны по модулю p для любого p > 1, то теория Tf является модельно полной.

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

Теорема 2. Пусть f0 согласованная со сложением функция и все функции fi периодичны по модулю p для любого натурального p. Тогда если теорию Tf обогатить предикатами делимости и обратными функциями для f0, f1, f2,..., fn, то в ней любая формула эквивалентна бескванторной формуле.

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

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

В параграфе 3.3 устанавливаются некоторые достаточные условия для f0, при которых функции fi будут эффективно периодичными по любому натуральному модулю.

Теорема 3. Пусть для любого p > 1 функция f (x) периодична по модулю p с периодом меньше p. Тогда гиперфункция F (x) от функции f (x) является эффективно периодичной по модулю p > 1 с периодом 1 для любого p.

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

Теорема 4. Пусть f функция, согласованная со сложением, и для любого p > 1 функция f (x) периодична по модулю p с периодом меньше p. Пусть f1 (x) периодичная функция. Тогда гиперфункция F (x) от функции f (x) + f1 (x) является периодичной по модулю p для любого p > 1.

Для доказательства показывается, что существует последовательность q0, q1,..., qk такая, что qk < qk1 < · · · < q0, и f (x) периодична по модулю q0 с периодом q1, по модулю q1 с периодом q2,..., по модулю qk1 с периодом qk, по модулю qk с периодом 1, где q0 период f1 (x).

Далее показывается, что если доказать периодичность F (x) по модулям q0, q1,..., qk, то будет доказана периодичность F (x) по модулю p, начиная с некоторого x. И, наконец, доказывается периодичность F (x) по модулям q0, q1,..., qk.

В четвёртой главе исследуется вычислительная сложность задачи разрешения теории Tf. В параграфе 4.1 оценивается время работы алгоритма из параграфа 3.2. Доказывается ряд лемм(12–27), при помощи которых оцениваются константы, используемые в разрешающем алгоритме из параграфа 3.2. В лемме 28 устанавливается, что формула длины n после одной итерации алгоритма из теоремы 1 в первом случае будет иметь длину не больше n20 для достаточно больших n. Далее в лемме устанавливается, что формула длины n после одной итерации алгоритма из теоремы 1 во втором случае будет иметь длину не больше n5 для достаточно больших n. Затем доказывается, что время работы разрешающего исходная формула была длиной n:

Теорема 5. Пусть это формула ¬(x1... xg ). Пусть длина равна n. Тогда после одной итерации алгоритма из теоремы 1 длина для станта.

Доказательство этой теоремы сводится к рассмотрению всех случаев из теоремы 1 и оценки длины формулы на каждом этапе, используя леммы 12–29.

Из этой теоремы получается следующее следствие.

Следствие 2. Если формулу длины n привести к экзистенциальному виду по алгоритму, представленному в теореме 1, то её длина для Из теоремы 2 и следствия 2 получаем следующие результаты:

1. Если формулу длины n привести к бескванторной по алгоритму из теоремы 2, то её длина для достаточно больших n не будет преn 2. Разрешающий алгоритм из теоремы 2 для любой формулы длины n работает не больше, чем 22 для достаточно больших n.

В параграфе 4.2 Доказано, что для любого разрешающего алгоритма существует формула длины n из теории Tf, для которой время работы алгоритма будет не меньше чем 22. Фишером и Рабином был продемонстрирован следующий метод для установления нижней границы времени для разрешения теорий со сложением. Пусть для функции g, которая растёт не медленнее экспоненты, в теории со сложением T существует константа c > 0 такая, что для любого числа n N и для любого двоичного слова w длины n существуют формулы In (b), Jn (b), S(a, i), Hw (x) длины, не превосходящей cn. In (b) означает, что b < g(n)2, Jn (b) означает, что b = g(n), S(a, i) означает, что в a на iом месте стоит 1, Hw (x) означает, что первые g(n) элементов последовательности x имеют вид w0g(n)n. Тогда для любого алгоритма, разрешающего T, время его работы занимает больше, чем g(qn) шагов, где q некоторая константа. Фактически доказано, что задача разрешения теории T является трудной в классе TIME(g(O(n))).

Теорема 6. Пусть в произвольной теории со сложением T существует формула логики первого порядка, которая любую пару натуральных чисел (u, v) взаимно однозначно кодирует натуральным числом. Тогда для теории T существует константа c > 0 такая, что для каждого n существует формула n (a, y, x), которая кодирует любую последовательность натуральных чисел a0,... ag(n+1)1, то есть для любой такой последовательности существует a и для любого Также длина n (a, y, x) не превосходит cn.

Формула n (a, y, x) строится по индукции. Для n = 0, она получается из условия теоремы. Чтобы построить n+1 (a, y, x), сначала через n (a, y, x) определяются упомянутые выше формулы Sn (x, y), Jn (y), In (y).

Формула Hw (x) строится, используя формулу Sn (x, y).

x0, x1,..., x2h 1 элементы в листьях дерева, а любая внутренняя вершина содержит код пары своих сыновей:

Кодом дерева (и всей последовательности) будет число, стоящее в корне.

Чтобы закодировать путь от корня к листу с номером y, нам достаточно для каждого j знать, к какому сыну: левому или правому следует идти от вершины на глубине j. Следовательно, весь путь можно закодировать последовательностью нулей и единиц длины h. Используя n (a, y, x), можно эту последовательность закодировать, благодаря чему, имеем возможность построить n+1 (a, y, x). Благодаря тождественным преобразованиям и свойствам n (a, y, x), длина n+1 (a, y, x) возрастает не более чем на некоторую константу.

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

Теорема 7. Если в теории системы Th(, 0, 1, 2 f (x) для любого x, то в ней существует формула, которая взаимно однозначно кодирует два натуральных числа.

При выполнении условия из теоремы, получается:

Пара чисел (x, y) кодируются следующим образом:

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

Как следствие получаем:

1. Если в теории системы Th(, 0, 1, 2 f0 (x) для любого x, то задача разрешения