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

• Автор: Мучник, Андрей Альбертович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2001
• Место защиты: Москва
• Количество страниц: 47 с. : ил

Предисловие
В настоящей работе приводятся решения некоторых проблем математической логики и теории алгоритмов, использующие связь вопроса об истинности утверждений с определёнными математическими играми. Для иллюстрации рассмотрим известный пример. Пусть, дана замкнутая формула исчисления предикатов, и её предикатные символы проинтерпретированы в некоторой структуре. Нас интересует, истинна ли данная формула в данной структуре. А. Эренфойхт заметил, что с этим вопросом естественно связать игру. Для этого формула приводится к префиксному виду. Игроку, стремящемуся доказать истинность формулы, соответствуют кванторы существования; а игроку, стремящемуся доказать ложность формулы, соответствуют кванторы общности. Ходы в игре делаются в том порядке, в котором расположены кванторы формулы. Ход игрока состоит в указании какого-либо элемента структуры. В конце игры в бескванторную часть формулы вместо каждой переменной подставляется значение, которое определяется так. Если переменная х была связана квантором С} ((} — 3 или <2 = V), то вместо х подставляется тот элемент структуры, который был выбран игроком на ходе, соответствующем квантору <2. Если после подстановки бескванторная часть формулы становится истинной, то выиграл первый игрок; а если бескванторная часть формулы становится ложной, то выиграл второй игрок. Очевидно, что если исходная формула истинна, то у первого игрока есть выигрывающая стратегия; а если исходная формула ложна, то выигрывающая стратегия есть у второго игрока.
Заметим, что в отличие от примера из предыдущего абзаца мы будем рассматривать и игры в которых количество ходов бесконечно. Если для конечных игр просто доказать, что у одного из двух противников есть выигрывающая стратегия, то для бесконечных игр это очень нетривиальное свойство, называемое детерминированностью.
Обратимся к первой главе работы. Как известно, структура натуральных чисел со сложением и умножением имеет неразрешимую теорию первого порядка. Это обстоятельство делает особенно важным нахождение достаточно сильных разрешимых теорий. Одной из таких теорий является монадическая теория бинарного дерева. Бинарное дерево задаётся множеством всех двоичных слов и двумя операциями на нём: приписывание к слову нуля справа и приписывание к слову единицы справа. Монадическая теория состоит из формул, построенных с помощью этих двух операций, переменных

по словам и по множествам слов, предиката принадлежности, пропозициональных связок и кванторов по переменным обоих типов. Наличие в языке переменных по множествам делает эту теорию очень выразительной. К ней сводятся многие интересные вопросы математической логики и теории автоматов. Один из последних примеров такого сведения недавно предложен В. JI. Селивановым в докладе, представленном в [7]. Там изучается круг вопросов следующего типа: “можно ли по монадической формуле (со свободными переменными) эффективно узнать, выражает ли она предикат, выразимый элементарной формулой в той же сигнатуре?”.
Доказательство разрешимости монадической теории бинарного дерева было найдено М. Рабином в 1969 году [14]. Каждой формуле рассматриваемого языка эффективно сопоставляется конечный автомат, работающий на бинарном дереве, вершины которого размечены подходящим конечным алфавитом. Ключевым оказывается переход от автомата, распознающего какое-то множество разметок дерева, к автомату, распознающему дополнение до этого множества. Доказательство Рабина было очень сложным и, в частности, оно использовало трансфинитную индз'кцию по всем счётным ординалам. В докладе на международном математическом конгрессе в Ницце Рабин поставил проблему нахождения более простого доказательства, которое не использовало бы трансфинитной индукции [15].1 В теореме 1.1 мы предлагаем такое доказательство, основанное на играх. Оно было изложено в курсе лекций «Разрешимые теории», который был прочитан А. Л. Семёновым на кафедре математической логики Московского государственного университета в 1979/1980 учебном году. В 1981 году на той же кафедре автор защитил дипломную работу, содержащую этот результат. Соответствующая публикация автора в российском журнале “Семиотика и информатика” [3] была переведена международным журналом “Bulletin of the European Association for Theoretical Computer Science” [6].
Автор признателен Сергею Ивановичу Адяну, который посоветовал более формально выразить различие между доказательством из [14] и нашим доказательством, изложенным в § 2. Точные утверждения для выявления указанного различия вероятно связаны с проблемой аксиоматизации, поставленной П. С. Новиковым. Эта проблема была решена для одной функции следования в [17]. План решения этой проблемы для двух функций следования обсуждается в § 3.
1 Первая из поставленных в этом докладе проблем гласила: «1. Упростить доказательство теоремы 2(й), возможно, за счёт устранения трансфинитной индукции, использованной в [2]». Здесь теорема 2(п) — это ключевое утверждение из рассуждения Рабина, [2] — статья [14] из нашего списка литературы.

Во второй главе работы рассматривается общая теория алгоритмов, то есть теория изучающая свойства алгоритмов, не зависящие от конкретных моделей вычислений. С точки зрения математической логики значительная часть этой теории может рассматриваться как теория некоторой структуры, введённой X. Фридманом в [10]. Мы показываем, что для обширного класса формул истинность в этой структуре выражается посредством некоторой игры, которая не использует понятия вычислимости ([4]). Предлагаемая интерпретация позволяет прояснить известный в общей теории алгоритмов феномен релятивизуемости. Под релятивизацией понимается замена вычислимости на вычислимость относительно какого-то оракула. Построить истинную формулу общей теории алгоритмов, которая становится ложной при релятивизации любым невычислимым оракулом, — это просто. Тем не менее, как показывает математическая практика, релятивизации всех “естественных” истинных утверждений тоже истинны.
Третья глава работы посвящена вопросу, которым интересовались математики ещё в XVIII веке. А именно, математическому уточнению понятия случайной двоичной бесконечной последовательности. А. Н. Колмогоров в [1] сравнивает два способа такого уточнения. В первом способе используется введённое Колмогоровым понятие энтропии конечной двоичной последовательности. Для бесконечной двоичной последовательности а функция К (а I п) сопоставляет натуральному числу п энтропию начала а длины п. Неформально говоря, последовательность тем более случайна, чем больше значения функции К. Второй способ уточнения понятия случайности исходит из классического закона больших чисел. То есть частота нулей и единиц должна стремиться к 1/2. Но последовательность 010101... явно неслучайна! Может быть потребовать, чтобы закон больших чисел выполнялся для всякой подпоследовательности? Так тоже не получится, потому что можно рассмотреть подпоследовательность, состоящую как раз из тех членов начальной последовательности, которые равны нулю. Разумным компромиссом оказывается требование выполнения закона больших чисел для подпоследовательностей из достаточно широкого класса. Колмогоров в [1] рассмотрел класс всех подпоследовательностей, номера членов которых задаются вычислимыми монотонно возрастающими функциями. Колмогоров доказал, что для этого класса последовательности случайные в смысле второго способа уточнения бывают “максимально неслучайными” в смысле первого способа уточнения. А именно, он построил случайную в смысле закона больших чисел
в нумерации Н. Так как функция И: № —>■ N вычислима относительно д и является главной нумерацией функций вычислимых относительно д, то формула Ф истинна в структуре (М, И) (Г — это построенная после со ходов функция). Поэтому указанная для игрока I стратегия является выигрышной. Отметим, что эта стратегия не зависит от формулы Ф.
Пусть у игрока I существует вычислимая выигрышная стратегия. Фиксируем оракул А. Предположим, игрок II строит на нечётных номерах какую-нибудь главную А-нумерацию. Тогда построенная игроками функция Г1 тоже является главной А-нумерацией, и {М, Р) |= Ф. Поскольку все А-вычислительные структуры изоморфны, формула Ф истинна в любой из этих структур. □
Релятивизация этого доказательства даёт следующее.
Следствие 11.4.1. Пусть, В — какой-либо оракул. Замкнутая формула Ф произвольного языка в сигнатуре вычислительной структуры истинна для всех А-вычислительных структур с В А тогда и только тогда, когда у игрока I существует в игре Р(Ф) выигрышная стратегия, вычислимая относительно оракула В.
Следствие II.4.2. Пусть, у игрока I существует в игре Р(Ф) выигрышная стратегия. Тогда существует оракул В такой, что формула Ф истинна во всех А-вычислительных структурах с В ^ А.
Доказательство. В качестве оракула В можно взять выигрышную стратегию игрока I. □
Теорема И.4 даёт схему доказательства релятивизуемой истинности некоторого свойства: нужно построить выигрышную стратегию для игрока I в соответствующей игре. Анализ обычных доказательств общей теории алгоритмов показывает, что почти все они легко укладываются в эту схему. Основную часть доказательства составляет описание конкретной стратегии и проверка того, что она выигрышная; вычислимость её устанавливается просто.
Игры Гейла—Стюарта
Описанная выше игра является частным случаем игр Гейла— Стюарта. Согласно Д. Мартину [11] игра Гейла—Стюарта определяется на дереве высоты со с произвольным ветвлением. В ней участвуют два игрока I и II. Игра определяется разбиением множества всех путей, начинающихся из корня, на два множества: множество путей, выигрышных для игрока I, и множество путей, выигрышных для игрока II. Позицией игры является вершина дерева, начальной