В описательной сложности , ветви вычислительной сложности , FO представляет собой класс сложности структур, который можно распознать по формулам логики первого порядка , а также равен классу сложности AC 0 . В описательной сложности используется формализм логики, но не используются некоторые ключевые понятия, связанные с логикой, такие как теория доказательств или аксиоматизация.
Ограничение предикатов набором X дает меньший класс FO [ X ]. Например, FO [<] - это набор языков без звездочек . Два разных определения FO [<], с точки зрения логики и с точки зрения регулярных выражений, предполагают, что этот класс может быть математически интересен помимо своей роли в вычислительной сложности, и что методы как из логических, так и из регулярных выражений могут быть полезны изучение.
Точно так же расширения логики первого порядка, образованные добавлением операторов, порождают другие хорошо известные классы сложности. [1] Это позволяет установить сложность некоторых проблем без ссылки на алгоритмы .
Определение и примеры
Идея
Когда мы используем логический формализм для описания вычислительной задачи, входные данные представляют собой конечную структуру, а элементы этой структуры являются областью дискурса . Обычно входные данные представляют собой либо строку (битов, либо алфавит), а элементы логической структуры представляют позиции строки, либо входные данные представляют собой граф, а элементы логической структуры представляют его вершины. Длина входа будет измеряться размером соответствующей конструкции. Какой бы ни была структура, мы можем предположить, что есть отношения, которые можно проверить, например "истинно, если есть ребро от x до y "(в случае, если структура является графом), или"истинно тогда и только тогда п я буква строки равна 1.»Эти отношения являются предикатами для логики первого порядка системы. У нас также есть константы, которые являются особыми элементами соответствующей структуры, например , если мы хотим , чтобы проверить достижимость в граф, нам нужно будет выбрать две константы s (начало) и t (терминал).
В описательной теории сложности мы почти всегда предполагаем, что существует полный порядок по элементам и что мы можем проверить равенство между элементами. Это позволяет нам рассматривать элементы как числа: элемент x представляет собой число n, если естьэлементы y с. Благодаря этому у нас также может быть примитивный предикат bit, гдеистинно, если только k- й бит двоичного разложения числа n равен 1. (Мы можем заменить сложение и умножение тернарными отношениями, так что верно, если и только если а также верно, если и только если ).
Формально
Пусть X - набор предикатов на. Язык FO [ X ] определяется как замыкание конъюнкцией (), отрицание () и универсальная количественная оценка () над элементами конструкций. Экзистенциальная количественная оценка () и дизъюнкция () также часто используются, но их можно определить с помощью первых трех символов. Базовый случай - это предикаты X, примененные к некоторым переменным. Всегда неявно есть предикатдля каждой буквы a алфавита, утверждая, что буква в позиции x является a .
Семантика формул в FO проста, истинно, если и только если A ложно,истинно, если и только если A истинно, а B истинно, и верно, если и только если верно для всех значений v, которые x может принимать в базовом юниверсе. Для P в гр -ичный предиката, верно тогда и только тогда, когда интерпретируется как правда.
Имущество
Предупреждение
Затем запрос в FO будет проверять, истинна ли формула первого порядка для данной структуры, представляющей входные данные для проблемы. Не следует путать этот вид проблемы с проверкой истинности количественной логической формулы, которая является определением QBF , которое является PSPACE-полным . Разница между этими двумя проблемами заключается в том, что в QBF размер проблемы - это размер формулы, а элементы - это просто логические переменные, тогда как в FO размер проблемы - это размер структуры, а формула фиксирована.
Это похоже на параметризованную сложность, но размер формулы не является фиксированным параметром.
Нормальная форма
Не обращая внимания на пустые структуры, каждая формула эквивалентна формуле в предваренной нормальной форме (где сначала записываются все кванторы, а затем бескванторная формула).
Операторы
FO без операторов
С точки зрения сложности схемы , FO (ARB), где ARB - это набор всех предикатов, логика, в которой мы можем использовать произвольные предикаты, может быть показано равным AC 0 , первому классу в иерархии AC . Действительно, существует естественный перевод символов FO в узлы цепей, где существование а также размера n .
FO (BIT) - это ограничение семейства цепей AC 0 , которое можно построить в переменном логарифмическом времени . FO (<) - это набор языков без звездочек .
Частичная фиксированная точка - PSPACE
FO (PFP, X ) - это набор логических запросов, определяемых в FO (X), куда мы добавляем частичный оператор с фиксированной точкой.
Пусть k - целое число,- векторы k переменных, P - переменная второго порядка с арностью k , а φ - функция FO (PFP, X), использующая x и P в качестве переменных. Мы можем итеративно определить такой, что а также (имеется в виду φ сзаменена на переменную второго порядка P ). Тогда либо есть фиксированная точка, либо списокs циклический.
определяется как значение фиксированной точки на y, если есть фиксированная точка, иначе как false. Поскольку P s являются свойствами арности k , существует не более ценности для s, поэтому с помощью счетчика полиномиального пространства мы можем проверить, есть ли цикл или нет.
Доказано, что FO (PFP, BIT) равно PSPACE . Это определение эквивалентно.
Наименьшая фиксированная точка - P
FO (LFP, X) - это набор логических запросов, определяемых в FO (PFP, X), где частичная фиксированная точка ограничена монотонностью. То есть, если переменная второго порядка - P , то всегда подразумевает .
Мы можем гарантировать монотонность, ограничивая формулу φ, чтобы она содержала только положительные вхождения P (то есть вхождения, которым предшествует четное число отрицаний). В качестве альтернативы мы можем описать в виде где .
Из-за монотонности мы добавляем только векторы в таблицу истинности P , а поскольку есть только возможных векторов мы всегда найдем фиксированную точку перед итераций. Теорема Иммерман-Варди, показали независимо друг от друга Иммерман [2] и Варди , [3] показывает , что FO (LFP, БИТ) = Р . Это определение эквивалентно.
Транзитивное закрытие - NL
FO (TC, X) - это набор логических запросов, определяемых в FO (X) с помощью оператора транзитивного замыкания (TC).
TC определяется так: пусть k - натуральное число ивектор k переменных. потомверно, если существует n векторов переменных такой, что , и для всех , правда. Здесь φ формула, записанная в FO (TC) иозначает, что переменные u и v заменены на x и y .
FO (TC, BIT) равно NL .
Детерминированное транзитивное замыкание - это L
FO (DTC, X) определяется как FO (TC, X), где оператор транзитивного замыкания является детерминированным. Это означает, что когда мы применяем, мы знаем, что для всех u существует не более одного v такого, что.
Можно предположить, что является синтаксическим сахаром для где .
Было показано , что FO (DTC, БИТ), равен L .
Нормальная форма
Любая формула с оператором фиксированной точки (соответственно, транзитивным замыканием) может быть без ограничения общности записана с ровно одним применением операторов к 0 (соответственно. )
Итерация
Мы определим первый порядок с итерацией, ; здесь представляет собой (класс) функций от целых чисел к целым числам, и для различных классов функций получим разные классы сложности .
В этом разделе мы напишем значить а также значить . Сначала нам нужно определить блоки кванторов (QB), блок кванторов - это список где s являются FO -формулами без кванторов иs либо или же . Если Q является блоком квантификаторов, мы вызовемоператор итерации, который определяется как Q, записанныйвремя. Следует обратить внимание, что здесь естькванторы в списке, но используются только k переменных и каждая из этих переменных раз.
Теперь мы можем определить быть FO-формулами с итерационным оператором, экспонента которого находится в классе , и мы получаем эти равенства:
Логика без арифметических соотношений
Пусть отношение преемника succ - такое бинарное отношение, что верно тогда и только тогда, когда .
По логике первого порядка succ менее выразительно, чем <, который менее выразителен, чем +, который менее выразителен, чем бит , в то время как + и × выразительны, как бит .
Использование преемника для определения бита
Можно определить положительные, а затем битовые отношения с детерминированным транзитивным замыканием.
а также
с участием
Это просто означает, что когда мы запрашиваем бит 0, мы проверяем четность и переходим к (1,0), если a нечетное (что является принимающим состоянием), иначе мы отклоняем. Если мы немного проверим, мы делим a на 2 и проверяем бит.
Следовательно, нет смысла говорить об операторах с одним преемником без других предикатов.
Логика без преемника
FO [LFP] и FO [PFP] - это две логики без каких-либо предикатов, за исключением предикатов равенства между переменными и буквенными предикатами. Они равны соответственно реляционным-P и FO (PFP) реляционным-PSPACE , классам P и PSPACE над реляционными машинами . [4]
Теорема Абитебула-Виану утверждает, что FO (LFP) = FO (PFP) тогда и только тогда, когда FO (<, LFP) = FO (<, PFP), следовательно, тогда и только тогда, когда P = PSPACE. Этот результат был распространен на другие фиксированные точки. [4] Это показывает, что проблема первого порядка является скорее технической проблемой, чем фундаментальной.
Рекомендации
- Рональд Фэджин , Обобщенные спектры первого порядка и распознаваемые множества за полиномиальное время . Сложность вычислений / Под ред. Р. Карп, SIAM-AMS Proceedings 7, pp. 27–41. 1974 г.
- Рональд Феджин, Теория конечных моделей - личная перспектива . Теоретическая информатика 116, 1993, стр. 3–31.
- Нил Иммерман. Языки, охватывающие классы сложности . Пятнадцатый симпозиум ACM STOC , стр. 347–354. 1983 г.
- ^ Иммерман, Нил (1999). Описательная сложность . Springer. ISBN 978-0-387-98600-5.
- ^ Иммерман, Нил (1986). «Реляционные запросы, вычислимые за полиномиальное время» . Информация и контроль . 68 (1–3): 86–104. DOI : 10.1016 / s0019-9958 (86) 80029-8 .
- ^ Варди, Моше Ю. (1982). Сложность языков реляционных запросов (Расширенная аннотация) . Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений . STOC '82. Нью-Йорк, Нью-Йорк, США: ACM. С. 137–146. CiteSeerX 10.1.1.331.6045 . DOI : 10.1145 / 800070.802186 . ISBN 978-0897910705.
- ^ a b Серж Абитебул, Моше Й. Варди , Виктор Виану : логика фиксированных точек, реляционные машины и вычислительная сложность Журнал архива ACM, том 44, выпуск 1 (январь 1997 г.), страницы: 30-56, ISSN 0004-5411
Внешние ссылки
- Страница описательной сложности Нила Иммермана , включая диаграмму
- Зоопарк сложности о ФО , см. Также следующие классы