Введение

Описательная сложность — это раздел математической логики, теории вычислительной сложности и теории конечных моделей, который характеризует классы сложности типом логики, необходимой для выражения языков, им соответствующих. Например, PH, объединение всех классов сложности в полиномиальной иерархии, является точно классом языков, выразимых утверждениями логики второго порядка. Эта связь между сложностью и логикой конечных структур позволяет легко переносить результаты из одной области в другую, облегчая разработку новых методов доказательства и предоставляя дополнительные основания полагать, что основные классы сложности в некотором смысле "естественны" и не привязаны к конкретным абстрактным машинам, используемым для их определения. В частности, каждая логическая система порождает множество запросов, выразимых в этой системе. Эти запросы, при ограничении конечными структурами, соответствуют вычислительным задачам традиционной теории сложности. Первым важным результатом в описательной сложности стала теорема Фагина, доказанная Рональдом Фагином в 1974 году. Она установила, что NP — это точно множество языков, выразимых предложениями экзистенциальной логики второго порядка, то есть логики второго порядка, исключающей всеобщую квантификацию по отношениям, функциям и подмножествам. Позже многие другие классы были охарактеризованы аналогичным образом.

Окружающая обстановка

Когда мы используем логический формализм для описания вычислительной проблемы, входные данные представляют собой конечную структуру, а элементы этой структуры являются областью рассуждений. Обычно входные данные – это либо строка (из битов или по алфавиту), где элементы логической структуры представляют позиции в строке, либо граф, где элементы логической структуры представляют его вершины. Длина входных данных измеряется размером соответствующей структуры. Какова бы ни была структура, мы можем предположить наличие отношений, которые можно проверить, например, "истинно тогда и только тогда, когда существует ребро из x в y" (если структура является графом), или "истинно тогда и только тогда, когда n-й символ строки равен 1". Эти отношения являются предикатами для системы логики первого порядка. У нас также есть константы – специальные элементы соответствующей структуры. Например, для проверки достижимости в графе необходимо выбрать две константы: s (начальная вершина) и t (конечная вершина). В описательной теории сложности часто предполагается наличие полного порядка элементов и возможность проверки их равенства. Это позволяет рассматривать элементы как числа: элемент x представляет число n тогда и только тогда, когда существуют элементы y с... Благодаря этому мы также можем иметь примитивный предикат "бит", где истинно, если и только если k-й бит в двоичном представлении x равен 1. (Мы можем заменить сложение и умножение троичными отношениями, такими что истинно, если и только если, и истинно, если и только если).

ОО без операторов

В сложности цепей показано, что логика первого порядка с произвольными предикатами эквивалентна AC0, первому классу в иерархии AC. Действительно, существует естественное отображение символов FO на узлы цепей, при этом число узлов и размер цепи составляют n. Логика первого порядка в сигнатуре с арифметическими предикатами характеризует ограничение семейства цепей AC0 теми, которые могут быть построены за чередующееся логарифмическое время.

Логика транзитивного закрытия

Логика первого порядка значительно выигрывает в выразительной силе, когда она расширяется оператором, вычисляющим транзитивное замыкание бинарного отношения. Известно, что результирующая логика транзитивного замыкания характеризует недетерминированное логарифмическое пространство (NL) на упорядоченных структурах. Это было использовано Иммерманом для доказательства того, что NL замкнуто относительно дополнения (то есть, что NL = co NL). При ограничении оператора транзитивного замыкания до детерминированного транзитивного замыкания, полученная логика точно характеризует логарифмическое пространство на упорядоченных структурах.

Формулы второго порядка Крома

На структурах, имеющих функцию преемника, класс сложности NL также может быть охарактеризован формулами второго порядка Крома. SO Krom – это множество булевых запросов, определяемых формулами второго порядка в конъюнктивной нормальной форме, где квантификаторы первого порядка являются универсальными, а бескванторная часть формулы представлена в форме Крома, то есть формула первого порядка является конъюнкцией дизъюнкций, и в каждой дизъюнкции содержится не более двух переменных. Любая формула второго порядка Крома эквивалентна экзистенциальной формуле второго порядка Крома. SO Krom характеризует класс сложности NL на структурах с функцией преемника.

Логика наименьшей фиксированной точки первого порядка

FO[LFP] — это расширение логики первого порядка оператором наименьшей неподвижной точки, который выражает неподвижную точку монотонного выражения. Это расширяет логику первого порядка, добавляя возможность выражать рекурсию. Теорема Иммермана — Варди, доказанная независимо Иммерманом и Варди, показывает, что FO[LFP] характеризует класс сложности PTIME на упорядоченных структурах. По состоянию на 2022 год остается открытым вопрос о существовании естественной логики, характеризующей PTIME на неупорядоченных структурах. Теорема Абитебуля — Виану утверждает, что FO[LFP] = FO[PFP] на всех структурах тогда и только тогда, когда P = PSPACE. Этот результат был обобщен на другие типы неподвижных точек.

Формулы второго порядка

При наличии функции преемника, PTIME также может быть охарактеризована формулами Хорна второго порядка. SO Horn – это множество булевых запросов, определяемых формулами SO в дизъюнктивной нормальной форме, где все квантификаторы первого порядка являются универсальными, а квантор-свободная часть формулы имеет вид Хорна, то есть представляет собой большое "И" дизъюнкций, и в каждой дизъюнкции все переменные, кроме, возможно, одной, отрицаются. Этот класс эквивалентен классу P на структурах с функцией преемника. Эти формулы могут быть преобразованы в пренекс-формулы экзистенциальной логики Хорна второго порядка. Поскольку дополнение экзистенциальной формулы является универсальной формулой, непосредственно следует, что co NP характеризуется универсальной логикой второго порядка. В отличие от большинства других характеризаций классов сложности, теорема Фагина и её обобщение не требуют наличия полного порядка на структурах. Это объясняется тем, что экзистенциальная логика второго порядка сама по себе достаточно выразительна, чтобы ссылаться на возможные полные порядки на структуре, используя переменные второго порядка.

Частичная фиксированная точка PSPACE

Класс всех задач, вычислимых за полиномиальное пространство, PSPACE, может быть охарактеризован расширением логики первого порядка оператором частичной неподвижной точки, обладающим большей выразительной силой. Логика первого порядка с частичной неподвижной точкой, FO[PFP], является расширением логики первого порядка оператором частичной неподвижной точки, который определяет неподвижную точку формулы, если она существует, и возвращает "ложь" в противном случае. Логика первого порядка с частичной неподвижной точкой характеризует PSPACE для упорядоченных структур.

Транзитивная закрытие PSPACE

Логика второго порядка может быть расширена оператором транзитивного замыкания так же, как и логика первого порядка, что приводит к SO[TC]. Оператор транзитивного замыкания теперь также может принимать переменные второго порядка в качестве аргумента. SO[TC] характеризует класс сложности PSPACE. Поскольку в логике второго порядка можно ссылаться на отношения порядка, эта характеристика не требует предположения об упорядоченных структурах.

Элементарные функции

Класс временной сложности элементарных функций может быть охарактеризован классом HO, классом сложности структур, распознаваемых формулами логики высшего порядка. Логика высшего порядка является расширением логики первого и второго порядка квантификаторами высшего порядка. Существует связь между алгоритмами порядка *th* и недетерминированными алгоритмами, время работы которых ограничено уровнями экспоненциальных функций.

Определение

Мы определяем переменные высшего порядка. Переменная порядка *n* имеет арность *n* и представляет собой любое множество *n*-кортежей элементов порядка *n*. Они обычно записываются заглавными буквами с натуральным числом в качестве показателя степени для обозначения порядка. Логика высшего порядка – это множество формул первого порядка, к которым мы добавляем квантификацию по переменным высшего порядка; следовательно, мы будем использовать термины, определенные в статье о логике первого порядка, без повторного определения. HO – это множество формул с переменными порядка не выше *n*. HO – это подмножество формул вида , где *Q* – квантор, а означает, что – это *n*-кортеж переменных порядка *n* с той же квантификацией. Таким образом, HO – это множество формул с чередованием кванторов порядка *n*, начинающихся с , за которым следует формула порядка *n*. Используя стандартное обозначение тетрации, и с кратностью *n*.

Нормальная форма

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

Отношение к классам сложности

HO равен классу ELEMENTARY элементарных функций. Если быть точнее, , означает башню из двоек, заканчивающуюся на , где – константа. Частным случаем этого является , что является точной формулировкой теоремы Фагина. Используя оракульные машины в полиномиальной иерархии,