Теорема Феджина - Fagin's theorem

Теорема Феджина - старейший результат описательной теории сложности , раздела теории вычислительной сложности, который характеризует классы сложности с точки зрения логического описания их проблем, а не поведения алгоритмов для решения этих проблем. Теорема утверждает, что набор всех свойств, выражаемых в экзистенциальной логике второго порядка, в точности является классом сложности NP .

Это было доказано Рональдом Феджином в 1973 году в его докторской диссертации и опубликовано в его статье 1974 года. Арность требуется по формуле второго порядка была улучшена (в одном направлении) в теореме Линч , и несколько результатов Гранджинов обеспечили более жесткие ограничения на недетерминированных произвольный доступ машинах.

Доказательство

В дополнение к статье Феджина 1974 г., Иммерман 1999 предоставляет подробное доказательство теоремы. Несложно показать, что каждая экзистенциальная формула второго порядка может быть распознана в NP путем недетерминированного выбора значения всех экзистенциально квалифицированных переменных, поэтому основная часть доказательства состоит в том, чтобы показать, что каждый язык в NP может быть описан экзистенциальная формула второго порядка. Для этого можно использовать кванторы существования второго порядка для произвольного выбора таблицы вычислений. Более подробно, для каждого временного шага трассы выполнения недетерминированной машины Тьюринга эта таблица кодирует состояние машины Тьюринга, ее положение на ленте, содержимое каждой ячейки ленты и какой недетерминированный выбор машина делает на этот шаг. Ограничение этой закодированной информации таким образом, чтобы она описывала действительную трассу выполнения, в которой содержимое ленты, а также состояние и положение машины Тьюринга на каждом временном шаге следуют из предыдущего временного шага, затем можно выполнить с помощью формулы первого порядка .

Лемма ключа , используемая в доказательстве является то , что можно кодировать линейный порядок длины п к (например, линейным порядкам и временных шагов содержимого ленты в любом временном шаге) в виде 2 K -ичных отношений R на вселенную A размера  п . Одним из способов достижения этой цели является выбор линейного упорядочения L из A , а затем определить R быть лексикографическое упорядочение из K -кортежей от A относительно  L .

Смотрите также

Ссылки

  • Иммерман, Нил (1999). Описательная сложность . Нью-Йорк: Springer-Verlag. С. 113–119. ISBN 0-387-98600-6.

дальнейшее чтение