Монадическая логика второго порядка
В математической логике монадическая логика второго порядка ( MSO ) — это фрагмент логики второго порядка , где количественная оценка второго порядка ограничена количественной оценкой по множествам. [1] Это особенно важно в логике графов из-за теоремы Курселя , которая предоставляет алгоритмы для вычисления монадических формул второго порядка над графами ограниченной ширины дерева . Это также имеет фундаментальное значение в теории автоматов , где теорема Бючи-Эльгота-Трахтенброта дает логическую характеристику регулярных языков .
Логика второго порядка позволяет проводить количественную оценку предикатов . Однако MSO — это фрагмент , в котором количественная оценка второго порядка ограничена монадическими предикатами (предикатами, имеющими один аргумент). Это часто описывается как количественная оценка «наборов», поскольку монадические предикаты эквивалентны по выразительной силе множествам (набору элементов, для которых предикат истинен).
Варианты [ править ]
Монадическая логика второго порядка существует в двух вариантах. В варианте, рассматриваемом для таких структур, как графы, и в теореме Курселя, формула может включать немонадические предикаты (в данном случае предикат бинарного ребра ), но количественная оценка ограничивается только монадическими предикатами. В варианте, рассматриваемом в теории автоматов и теореме Бючи–Эльгота–Трахтенброта, все предикаты, в том числе и в самой формуле, должны быть монадическими, за исключением равенства ( ) и заказ ( ) связи.
Вычислительная сложность оценки [ править ]
Экзистенциальная монадическая логика второго порядка (EMSO) — это фрагмент MSO, в котором все кванторы над множествами должны быть кванторами существования вне любой другой части формулы. Кванторы первого порядка не ограничены. По аналогии с теоремой Феджина , согласно которой экзистенциальная (негонадическая) логика второго порядка точно отражает дескриптивную сложность класса сложности NP , класс проблем, которые могут быть выражены в экзистенциальной монадической логике второго порядка, получил название монадической NP. . Ограничение на монадическую логику позволяет доказать в этой логике разделения, которые остаются недоказанными для немонадической логики второго порядка. Например, в логике графов проверка того, является ли граф несвязным, принадлежит монадическому NP, поскольку тест может быть представлен формулой, описывающей существование правильного подмножества вершин без ребер, соединяющих их с остальной частью графа. ; однако дополнительная задача проверки связности графа не принадлежит монадической NP. [2] [3] Существование аналогичной пары дополнительных задач, только одна из которых имеет экзистенциальную формулу второго порядка (без ограничения на монадические формулы), эквивалентно неравенству NP и coNP , открытому вопросу вычислительной сложности.
Напротив, когда мы хотим проверить, удовлетворяется ли логическая формула MSO входным конечным деревом , эту проблему можно решить за линейное время в дереве, переведя булеву формулу MSO в древесный автомат. [4] и оцениваем автомат на дереве. Однако с точки зрения запроса сложность этого процесса обычно не является элементарной . [5] Благодаря теореме Курселя мы также можем вычислить логическую формулу MSO за линейное время на входном графе, если ширина дерева графа ограничена константой.
Для формул MSO, которые имеют свободные переменные , когда входные данные представляют собой дерево или имеют ограниченную ширину дерева, существуют эффективные алгоритмы перечисления для создания набора всех решений: [6] гарантируя, что входные данные предварительно обрабатываются за линейное время и что каждое решение затем создается с задержкой, линейной по размеру каждого решения, т. е. с постоянной задержкой в общем случае, когда все свободные переменные запроса являются переменными первого порядка ( т. е. они не представляют множества). В этом случае также существуют эффективные алгоритмы подсчета количества решений формулы MSO. [7]
Разрешимость и сложность выполнимости [ править ]
Проблема выполнимости монадической логики второго порядка, вообще говоря, неразрешима, поскольку эта логика включает в себя логику первого порядка .
Монадическая теория второго порядка бесконечного полного двоичного дерева , называемая S2S , разрешима . [8] Вследствие этого результата разрешимы следующие теории:
- Монадическая теория деревьев второго порядка.
- Монадическая теория второго порядка под преемником (S1S).
- WS2S и WS1S, которые ограничивают количественную оценку конечными подмножествами (слабая монадическая логика второго порядка). Обратите внимание, что для двоичных чисел (представленных подмножествами) сложение можно определить даже в WS1S.
Для каждой из этих теорий (S2S, S1S, WS2S, WS1S) сложность проблемы решения неэлементарна . [5] [9]
Использование выполнимости MSO на деревьях при проверке [ править ]
Монадическая логика деревьев второго порядка имеет приложения в формальной верификации . Процедуры принятия решения о выполнимости MSO [10] [11] [12] использовались для доказательства свойств программ, манипулирующих связанными структурами данных , [13] как форма анализа формы и для символических рассуждений при проверке оборудования . [14]
См. также [ править ]
Ссылки [ править ]
- ^ Курсель, Бруно ; Энгельфриет, Йост (01 января 2012 г.). Структура графа и монадическая логика второго порядка: теоретико-языковой подход . Издательство Кембриджского университета. ISBN 978-0521898331 . Проверено 15 сентября 2016 г.
- ^ Феджин, Рональд (1975), «Монадические обобщенные спектры», Журнал математической логики и основ математики , 21 : 89–96, doi : 10.1002/malq.19750210112 , MR 0371623 .
- ^ Феджин, Р .; Стокмейер, Л .; Варди, МЮ (1993), «О монадическом NP против монадического со-NP», Материалы восьмой ежегодной конференции по теории структуры сложности , Институт инженеров по электротехнике и электронике, номер документа : 10.1109/sct.1993.336544 , S2CID 32740047 .
- ^ Тэтчер, Дж.В.; Райт, Дж. Б. (1 марта 1968 г.). «Обобщенная теория конечных автоматов с приложением к задаче решения логики второго порядка». Теория математических систем . 2 (1): 57–81. дои : 10.1007/BF01691346 . ISSN 1433-0490 . S2CID 31513761 .
- ^ Перейти обратно: а б Мейер, Альберт Р. (1975). Парих, Рохит (ред.). «Слабая монадическая теория наследника второго порядка не является элементарно-рекурсивной». Логический коллоквиум . Конспект лекций по математике. Шпрингер Берлин Гейдельберг: 132–154. дои : 10.1007/bfb0064872 . ISBN 9783540374831 .
- ^ Баган, Гийом (2006). Эсик, Золтан (ред.). «Запросы MSO к древовидным разложимым структурам вычисляются с линейной задержкой». Информатика Логика . Конспекты лекций по информатике. 4207 . Шпрингер Берлин Гейдельберг: 167–181. дои : 10.1007/11874683_11 . ISBN 9783540454595 .
- ^ Арнборг, Стефан; Лагергрен, Йенс; Сизе, Детлеф (1 июня 1991 г.). «Простые задачи для древовидных графов». Журнал алгоритмов . 12 (2): 308–340. дои : 10.1016/0196-6774(91)90006-К . ISSN 0196-6774 .
- ^ Рабин, Майкл О. (1969). «Разрешимость теорий второго порядка и автоматов на бесконечных деревьях» . Труды Американского математического общества . 141 : 1–35. дои : 10.2307/1995086 . ISSN 0002-9947 . JSTOR 1995086 .
- ^ Стокмейер, Ларри; Мейер, Альберт Р. (1 ноября 2002 г.). «Космологическая нижняя граница схемной сложности небольшой задачи логики» . Журнал АКМ . 49 (6): 753–784. дои : 10.1145/602220.602223 . ISSN 0004-5411 . S2CID 15515064 .
- ^ Хенриксен, Йеспер Г.; Дженсен, Джейкоб; Йоргенсен, Майкл; Кларлунд, Нильс; Пейдж, Роберт; Рауэ, Тайс; Сэндхольм, Андерс (1995). Бринксма, Э.; Кливленд, WR; Ларсен, КГ; Маргария, Т. ; Стеффен, Б. (ред.). «Мона: Монадическая логика второго порядка на практике» . Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. 1019 . Берлин, Гейдельберг: Springer: 89–110. дои : 10.1007/3-540-60630-0_5 . ISBN 978-3-540-48509-4 .
- ^ Федор, Томас; Голик, Лукаш; Ленгал, Ондржей; Войнар, Томаш (01.04.2019). «Вложенные антицепи для WS1S» . Акта Информатика . 56 (3): 205–228. дои : 10.1007/s00236-018-0331-z . ISSN 1432-0525 . S2CID 57189727 .
- ^ Трайтель, Дмитрий; Нипков, Тобиас (25 сентября 2013 г.). «Проверенные процедуры принятия решений для MSO по словам на основе производных регулярных выражений» . Уведомления ACM SIGPLAN . 48 (9): 3–f12. дои : 10.1145/2544174.2500612 . hdl : 20.500.11850/106053 . ISSN 0362-1340 .
- ^ Мёллер, Андерс; Шварцбах, Майкл И. (1 мая 2001 г.). «Логический механизм утверждения указателя» . Материалы конференции ACM SIGPLAN 2001 по проектированию и реализации языков программирования . ПЛДИ '01. Сноуберд, Юта, США: Ассоциация вычислительной техники. стр. 221–231. дои : 10.1145/378795.378851 . ISBN 978-1-58113-414-8 . S2CID 11476928 .
- ^ Басин, Дэвид; Кларлунд, Нильс (1 ноября 1998 г.). «Символические рассуждения на основе автоматов при проверке оборудования» . Формальные методы проектирования систем . 13 (3): 255–288. дои : 10.1023/А:1008644009416 . ISSN 0925-9856 .
