Монадическая логика второго порядка

В математической логике монадическая логика второго порядка ( MSO ) — это фрагмент логики второго порядка , где квантификация второго порядка ограничена квантификацией по множествам. ^[1] Она особенно важна в логике графов из-за теоремы Курселя , которая предоставляет алгоритмы для вычисления монадических формул второго порядка по графам ограниченной древовидной ширины . Она также имеет фундаментальное значение в теории автоматов , где теорема Бюхи–Элгота–Трактенброта даёт логическую характеристику регулярных языков .

Логика второго порядка допускает квантификацию по предикатам . Однако MSO — это фрагмент , в котором квантификация второго порядка ограничена монадическими предикатами (предикатами, имеющими один аргумент). Это часто описывается как квантификация по «множествам», поскольку монадические предикаты эквивалентны по выразительной силе множествам (множеству элементов, для которых предикат истинен).

Варианты

Монадическая логика второго порядка существует в двух вариантах. В варианте, рассматриваемом над такими структурами, как графы, и в теореме Курселя формула может включать немонадические предикаты (в данном случае предикат бинарного ребра ), но квантификация ограничена только монадическими предикатами. В варианте, рассматриваемом в теории автоматов и теореме Бюхи–Элгота–Трактенброта, все предикаты, включая те, что находятся в самой формуле, должны быть монадическими, за исключением отношений равенства ( ) и упорядочения ( ). ${\displaystyle E(x,y)}$ ${\displaystyle =}$ ${\displaystyle <}$

Вычислительная сложность оценки

Экзистенциальная монадическая логика второго порядка (EMSO) — это фрагмент MSO, в котором все кванторы по множествам должны быть экзистенциальными кванторами , за пределами любой другой части формулы. Квантификаторы первого порядка не ограничены. По аналогии с теоремой Фейгина , согласно которой экзистенциальная (немонадическая) логика второго порядка точно фиксирует описательную сложность класса сложности NP , класс проблем, которые могут быть выражены в экзистенциальной монадической логике второго порядка, был назван монадической NP. Ограничение монадической логикой позволяет доказывать разделения в этой логике, которые остаются недоказанными для немонадической логики второго порядка. Например, в логике графов проверка того, является ли граф несвязным, принадлежит монадической NP, поскольку тест может быть представлен формулой, описывающей существование собственного подмножества вершин без ребер, соединяющих их с остальной частью графа; Однако дополнительная задача, проверяющая, связен ли граф, не принадлежит к монадическому NP. ^{[2] [3]} Существование аналогичной пары дополнительных задач, только одна из которых имеет экзистенциальную формулу второго порядка (без ограничения монадическими формулами), эквивалентно неравенству NP и coNP , открытому вопросу в вычислительной сложности.

Напротив, когда мы хотим проверить, удовлетворяется ли булева формула MSO входным конечным деревом , эта проблема может быть решена за линейное время в дереве, путем перевода булевой формулы MSO в автомат дерева ^[4] и оценки автомата на дереве. Однако с точки зрения запроса сложность этого процесса, как правило, неэлементарна . ^[5] Благодаря теореме Курселя , мы также можем оценить булеву формулу MSO за линейное время на входном графе, если ширина дерева графа ограничена константой.

Для формул MSO, которые имеют свободные переменные , когда входные данные представляют собой дерево или имеют ограниченную ширину дерева, существуют эффективные алгоритмы перечисления для создания набора всех решений, ^[6] гарантируя, что входные данные предварительно обрабатываются за линейное время, а затем каждое решение создается с задержкой, линейной по размеру каждого решения, т. е. с постоянной задержкой в ​​общем случае, когда все свободные переменные запроса являются переменными первого порядка (т. е. они не представляют собой наборы). Существуют также эффективные алгоритмы для подсчета количества решений формулы MSO в этом случае. ^[7]

Разрешимость и сложность выполнимости

Проблема выполнимости для монадической логики второго порядка в общем случае неразрешима, поскольку эта логика включает в себя логику первого порядка .

Монадическая теория второго порядка бесконечного полного двоичного дерева , называемая S2S , разрешима . ^[8] Как следствие этого результата, следующие теории разрешимы:

• Монадическая теория деревьев второго порядка.
• Монадическая теория второго порядка нижестоящего элемента (S1S). ${\displaystyle \mathbb {N} }$
• WS2S и WS1S, которые ограничивают квантификацию конечными подмножествами (слабая монадическая логика второго порядка). Обратите внимание, что для двоичных чисел (представленных подмножествами) сложение определимо даже в WS1S.

Для каждой из этих теорий (S2S, S1S, WS2S, WS1S) сложность проблемы принятия решения неэлементарна . ^{[5] [9]}

Использование выполнимости MSO на деревьях при проверке

Монадическая логика второго порядка деревьев имеет приложения в формальной верификации . Процедуры принятия решений для выполнимости MSO ^{[10] [11] [12]} использовались для доказательства свойств программ, манипулирующих связанными структурами данных , ^[13] как форма анализа формы , и для символических рассуждений в верификации оборудования . ^[14]

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

• Описательная теория сложности
• Монадическое исчисление предикатов
• Логика второго порядка

Ссылки

1. Курсель, Бруно ; Энгельфрит, Йост (2012-01-01). Структура графа и монадическая логика второго порядка: подход к теории языка. Cambridge University Press. ISBN 978-0521898331. Получено 15.09.2016 .
2. Феджин, Рональд (1975), «Монадические обобщенные спектры», Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , 21 : 89–96, doi : 10.1002/malq.19750210112, MR  0371623.
3. Фейгин, Р.; Стокмейер , Л .; Варди, М.Ю. (1993), «О монадических NP против монадических co-NP», Труды Восьмой ежегодной конференции по теории структур сложности , Институт инженеров по электротехнике и электронике, doi :10.1109/sct.1993.336544, S2CID  32740047.
4. Thatcher, JW; Wright, JB (1968-03-01). «Обобщенная теория конечных автоматов с приложением к проблеме принятия решений логики второго порядка». Математическая теория систем . 2 (1): 57–81. doi :10.1007/BF01691346. ISSN  1433-0490. S2CID  31513761.
5. Meyer, Albert R. (1975). Parikh, Rohit (ред.). "Слабая монадическая теория второго порядка преемника не является элементарно-рекурсивной". Logic Colloquium . Lecture Notes in Mathematics. Springer Berlin Heidelberg: 132–154. doi :10.1007/bfb0064872. ISBN 9783540374831.
6. Баган, Гийом (2006). Эсик, Золтан (ред.). «MSO-запросы на древовидных разложимых структурах вычислимы с линейной задержкой». Computer Science Logic . Lecture Notes in Computer Science. 4207. Springer Berlin Heidelberg: 167–181. doi :10.1007/11874683_11. ISBN 9783540454595.
7. Арнборг, Стефан; Лагергрен, Йенс; Сизе, Детлеф (1 июня 1991 г.). «Простые задачи для древовидных графов». Журнал алгоритмов . 12 (2): 308–340. дои : 10.1016/0196-6774(91)90006-К. ISSN  0196-6774.
8. Рабин, Майкл О. (1969). «Разрешимость теорий второго порядка и автоматов на бесконечных деревьях». Труды Американского математического общества . 141 : 1–35. doi :10.2307/1995086. ISSN  0002-9947. JSTOR  1995086.
9. Стокмейер, Ларри; Мейер, Альберт Р. (2002-11-01). «Космологическая нижняя граница сложности схемы небольшой задачи в логике». Журнал ACM . 49 (6): 753–784. doi :10.1145/602220.602223. ISSN  0004-5411. S2CID  15515064.
10. Хенриксен, Йеспер Г.; Дженсен, Якоб; Йоргенсен, Майкл; Кларлунд, Нильс; Пейдж, Роберт; Рауэ, Тайс; Сэндхольм, Андерс (1995). Бринксма, Э.; Кливленд, WR; Ларсен, КГ; Маргария, Т. ; Стеффен, Б. (ред.). «Мона: Монадическая логика второго порядка на практике». Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. 1019 . Берлин, Гейдельберг: Springer: 89–110. дои : 10.1007/3-540-60630-0_5 . ISBN 978-3-540-48509-4.
11. Федор, Томаш; Голик, Лукаш; Ленгал, Ондржей; Войнар, Томаш (01 апреля 2019 г.). «Вложенные антицепи для WS1S». Акта Информатика . 56 (3): 205–228. doi : 10.1007/s00236-018-0331-z. ISSN  1432-0525. S2CID  57189727.
12. Traytel, Дмитрий; Nipkow, Тобиас (2013-09-25). «Проверенные процедуры принятия решений для MSO на основе слов на основе производных регулярных выражений». ACM SIGPLAN Notices . 48 (9): 3–f12. doi :10.1145/2544174.2500612. hdl : 20.500.11850/106053 . ISSN  0362-1340.
13. Мёллер, Андерс; Шварцбах, Майкл И. (2001-05-01). "Логическая машина утверждений указателей". Труды конференции ACM SIGPLAN 2001 по проектированию и реализации языков программирования . PLDI '01. Сноуберд, Юта, США: Ассоциация вычислительной техники. стр. 221–231. doi :10.1145/378795.378851. ISBN 978-1-58113-414-8. S2CID  11476928.
14. Basin, David; Klarlund, Nils (1998-11-01). "Автоматизированное символическое рассуждение при проверке оборудования". Formal Methods in System Design . 13 (3): 255–288. doi :10.1023/A:1008644009416. ISSN  0925-9856.