Логика второго порядка является продолжением первых порядка с вторым порядком кванторами, поэтому читатель должен сначала прочитать FO (сложность) , чтобы быть в состоянии понять эту статью. По описательной сложности мы можем видеть, что языки, распознаваемые формулами SO, в точности равны языкам, определенным машинами Тьюринга в полиномиальной иерархии . Расширения SO с некоторыми операторами также дают нам ту же выразительность дала некоторой хорошо известного классу сложности , [1] , так что это способ сделать доказательство о сложности некоторых задач без необходимости идти на алгоритмическую уровне.
Определение и примеры
Мы определяем переменную второго порядка, переменная SO имеет арность и представляют любое предложение арности , т.е. подмножество -конечности Вселенной. Обычно они пишутся заглавными буквами. Логика второго порядка - это набор формул FO, куда мы добавляем количественную оценку по переменным второго порядка, поэтому мы будем использовать термины, определенные в статье FO, без их повторного определения.
Имущество
Нормальная форма
Каждая формула эквивалентна формуле в предваренной нормальной форме, где мы сначала записываем количественную оценку переменной второго порядка, а затем формулу FO в преднексированной нормальной форме.
Отношение к классам сложности
SO равно полиномиальной иерархии , точнее, у нас есть эта формула в пренексной нормальной форме, где экзистенциальные и универсальные альтернативы второго порядка k раз являются k- м уровнем полиномиальной иерархии.
Это означает, что СО только с экзистенциальной квантификацией второго порядка равно который является NP , и только с универсальной квантификацией равенкоторый является Co-NP .
Добавление ограничений
Формулы Рога равны P
SO (рог) - это набор логических запросов, определяемых формулами SO в дизъюнктивной нормальной форме , так что кванторы первого порядка являются универсальными, а некванторная часть формулы находится в форме Хорна , что означает, что это большое И для ИЛИ, и в каждом «ИЛИ» все переменные, кроме, возможно, одной, инвертируются.
Этот класс равен P .
Эти формулы могут быть составлены в предварительной форме, где второй порядок является экзистенциальным, а первый - универсальным без потери общности.
Формулы Крома равны NL
SO (Krom) - это набор логических запросов, определяемых формулами второго порядка в конъюнктивной нормальной форме, так что кванторы первого порядка являются универсальными, а бескванторная часть формулы находится в форме Крома , что означает, что формула первого порядка является большое И или ИЛИ, и в каждом «ИЛИ» есть не более двух переменных.
Этот класс равен NL .
Эти формулы могут быть составлены в предварительной форме, где второй порядок является экзистенциальным, а первый - универсальным без потери общности.
Переходное закрытие - PSPACE
SO (TC) для SO - это то же самое, что FO (TC) для FO . Оператор TC теперь также может принимать в качестве аргумента переменную второго порядка. SO (TC) невероятно похож на PSPACE .
Наименьшая фиксированная точка - EXPTIME
SO (LFP) для SO - это то же самое, что FO (LFP) для FO . Оператор LFP теперь также может принимать в качестве аргумента переменную второго порядка. SO (LFP) невероятно похож на EXPTIME .
Итерация
SO ( t ( n )) для SO то же, что FO [ t ( n )] для FO . Но теперь у нас также есть квантификатор второго порядка в блоке квантификатора. Известно, что:
Смотрите также
Рекомендации
- ^ Н. Иммерман « Описательная сложность» (1999 Springer). Всю информацию в этой статье можно проверить в этой книге.
Внешние ссылки
- Зоопарк сложности о SO , см. Также класс под ним.