Теорема Феджинса - Fagins theorem
Теорема Феджина это самый старый результат описательная теория сложности, филиал теория сложности вычислений который характеризует классы сложности с точки зрения логического описания их проблем, а не поведения алгоритмов для решения этих проблем. Теорема утверждает, что набор всех свойств, выражаемых в экзистенциальной логика второго порядка это в точности класс сложности НП.
Это было доказано Рональд Феджин в 1973 г. в его докторской диссертации и появляется в его статье 1974 г. В арность требуемая формулой второго порядка была улучшена (в одну сторону) в Теорема Линча, и несколько результатов Гранджан предоставили более жесткие границы недетерминированных произвольный доступ машины.
Доказательство
В дополнение к статье Феджина 1974 г., Иммерман 1999 предоставляет подробное доказательство теоремы. Несложно показать, что каждая экзистенциальная формула второго порядка может быть распознана в NP, недетерминированно выбирая значение всех экзистенциально квалифицированных переменных, поэтому основная часть доказательства состоит в том, чтобы показать, что каждый язык в NP может быть описан экзистенциальная формула второго порядка. Для этого можно использовать кванторы существования второго порядка для произвольного выбора таблицы вычислений. Более подробно, для каждого временного шага трассировки выполнения недетерминированная машина Тьюринга эта таблица кодирует состояние машины Тьюринга, ее положение на ленте, содержимое каждой ячейки ленты и какой недетерминированный выбор машина делает на этом этапе. Ограничение этой закодированной информации так, чтобы она описывала действительную трассировку выполнения, в которой содержимое ленты, состояние и положение машины Тьюринга на каждом временном шаге следуют из предыдущего временного шага, затем можно выполнить с помощью формула первого порядка.
Ключевая лемма, использованная в доказательстве, заключается в том, что можно закодировать линейный порядок длины пk (например, линейный порядок временных шагов и содержимого ленты на любом временном шаге) как 2k-арное отношение р во вселенной А размерап. Один из способов добиться этого - выбрать линейное упорядочение. L из А а затем определить р быть лексикографический порядок из k- пары из А относительноL.
Смотрите также
Рекомендации
- Феджин, Рональд. "Обобщенные спектры первого порядка и распознаваемые за полиномиальное время множества ". Сложность вычислений, изд. Р. Карп, SIAM-AMS Proceedings, Vol. 7 (1974): 43-73.
- Иммерман, Нил (1999). Описательная сложность. Нью-Йорк: Springer-Verlag. С. 113–119. ISBN 0-387-98600-6.
дальнейшее чтение
- Грэдель, Эрих; Колайтис, Phokion G .; Либкин Леонид; Маркс, Маартен; Спенсер, Джоэл; Варди, Моше Ю.; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения. Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag. ISBN 978-3-540-00428-8. Zbl 1133.03001.