Формальные языки
Дескриптивная сложность
Если P ≠ NP нельзя доказать 'в лоб' - может логика поможет? Теорема Фагина (1974) дала первую точную логическую характеристику NP: это ровно те задачи, выразимые в экзистенциальном SO. Это связывает два разных мира - математическую логику и теорию вычислений.
- Datalog - логический язык запросов, соответствует FO + LFP - используется в Souffle (статический анализ LLVM)
- GraphQL и Cypher (Neo4j): выразительность запросов определяется логической сложностью
- Prolog: резолюция в Horn clauses - фрагмент FO, полиномиальная сложность для datalog
- SPARQL (W3C RDF запросы): выразительность соответствует FO с рекурсией (SPARQL 1.1)
Логика и вычислительная сложность
Дескриптивная сложность (Immerman, Fagin) связывает классы сложности с фрагментами логики. Центральный вопрос: какие задачи можно выразить формулой данной логики над конечными структурами?
FO (первый порядок) выражает свойства с ограниченным числом квантификаторов - это AC0. Сложение и умножение натуральных чисел не выразимы в FO (теорема Furst-Saxe-Sipser). Для полиномиального времени нужен LFP - итерация до фиксированной точки.
Почему FO соответствует AC0, а не P?
Теорема Фагина и NP
Теорема Фагина (1974): класс NP точно соответствует экзистенциальному второму порядку (∃SO) над конечными структурами. Это первая точная логическая характеристика класса сложности - до теорем о вычислительной сложности.
- ∃SO = NP: экзистенциальная квантификация по отношениям = недетерминизм
- ∀SO = co-NP: универсальная квантификация по отношениям
- ∃∀SO = Sigma_2^P, ∀∃SO = Pi_2^P - первый и второй уровень PH
- SO = PH: всё второй порядок = вся иерархия полинома
Почему экзистенциальная квантификация второго порядка соответствует недетерминизму?
Дескриптивная характеризация PTIME
FO + LFP (least fixed point) = PTIME на упорядоченных структурах (Immerman-Vardi теорема, 1982). Оговорка 'упорядоченных' существенна: без упорядочения FO + LFP не захватывает весь PTIME.
Почему без упорядочения FO + LFP не захватывает весь PTIME?
Теория конечных моделей
Теория конечных моделей отличается от классической теории моделей: теорема Гёделя о полноте и теорема компактности не работают для конечных структур. Игры Эренфейхта-Фраиссе - основной инструмент разделения классов.
Как игра Эренфейхта-Фраиссе доказывает, что задача не выразима в FO?
Итоги
- FO = AC0: ограниченное число кванторов = схемы постоянной глубины
- FO + LFP = PTIME (на упорядоченных): итерация до фиксированной точки добавляет P
- ∃SO = NP (теорема Фагина): угадать предикат + проверить FO формулой
- EF-игры: основной инструмент доказательства невыразимости в FO
Связанные темы
Дескриптивная сложность соединяет математическую логику с теорией вычислений:
- P vs NP — ∃SO = NP: логическая характеризация дала новые барьеры (relativization в логических терминах)
- Темпоральная логика — CTL = mu-calculus = LFP над кripke-структурами: model checking как FO + LFP
- Базы данных — Datalog = FO + LFP: запросы с рекурсией, используются в Souffle, Datomic
- Коммуникационная сложность — Ehrenfeucht-Fraisse связана с коммуникационной сложностью через игровые характеризации
Вопросы для размышления
- Если ∃SO = NP, то можно ли через ∃SO доказать P ≠ NP, показав что CLIQUE не в FO+LFP?
- Почему теорема компактности не работает для конечных структур и что это означает для дескриптивной сложности?
- Как Datalog (FO + LFP) используется в Souffle для статического анализа программ?