Есть ли логика без индукции, которая захватывает большую часть P?

38

Теорема Иммермана-Варди утверждает, что PTIME (или P) - это именно тот класс языков, который может быть описан предложением логики первого порядка вместе с оператором с фиксированной точкой над классом упорядоченных структур. Оператор с фиксированной точкой может быть либо с наименьшей фиксированной точкой (как рассматривалось Иммерманом и Варди), либо инфляционной фиксированной точкой. (Стефан Кройцер, Выразительная эквивалентность наименьшей и инфляционной логики с фиксированной запятой , Annals of Pure и Applied Logic 130 61–78, 2004).

Юрий Гуревич предположил, что нет логики захвата PTIME (« Логика и вызов информатики» , «Современные тенденции теоретической информатики», изд. Egon Boerger, 1–57, Computer Science Press, 1988), в то время как Мартин Грох заявил, что он менее уверенный ( В поисках логического захвата PTIME , FOCS 2008).

Оператор с фиксированной точкой предназначен для захвата мощности рекурсии. Фиксированные точки являются мощными, но для меня не очевидно, что они необходимы.

Существует ли оператор X, который не основан на фиксированных точках, такой, что FOL + X захватывает (большой) фрагмент PTIME?

Редактировать: Насколько я понимаю, линейная логика может выражать только утверждения о структурах, которые имеют довольно ограничительную форму. В идеале я хотел бы видеть ссылку или набросок логики, которая может выражать свойства произвольных наборов реляционных структур, но при этом избегать фиксированных точек. Если я ошибаюсь по поводу выразительной силы линейной логики, тогда приветствуется указатель или подсказка.

Андраш Саламон
источник
2
Под «логикой» я подразумеваю то, что означает Грохе: разрешимый набор предложений над словарем и отношение «является моделью» между конечными структурами и предложениями со свойством того, что множество моделей предложения всегда замкнуто при изоморфизме ,
Андрас Саламон
См. Также cstheory.stackexchange.com/questions/174/… для вопроса о том, существует ли логика, которая захватывает PTIME.
Андрас Саламон
Линейная логика - это логика высказываний, которая содержит классическую логику высказываний. Его можно расширить, чтобы разрешить квантификаторы. Но если я правильно помню, связь между линейной логикой (пропозициональными) и классами сложности отличается от того, что Грохе имеет в виду, по крайней мере, я не понимаю, как связать линейную логику с запросами над конечными структурами.
Каве
Существуют теории множеств, построенные на линейной логике, такие как теория аффинного множества света Теруи, обладающая свойством, что функция может быть доказана в ней полной, если и только если функция вычислима за полиномиальное время. См. Citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730
Нил Кришнасвами
1
Каве, вот почему я присудил награду Слимтону. Более подробный ответ все равно был бы хорош.
Андрас Саламон

Ответы:

23

Вы хотите взглянуть на то, что некоторые люди называют теоремой Гределя. Вы можете найти его в книге Пападимитриу «Вычислительная сложность» (это теорема 8.4 на стр. 176) или в оригинальной статье Грэделя .

(R)(x)(ϕ)
RxϕRR
slimton
источник
3
Ой, теперь, когда я снова прочитал ваш вопрос, я понял, что он немного отличается от предыдущей версии. Теперь вы запрашиваете оператор X, чтобы FOL + X захватывал большой фрагмент P. В этом случае вы должны взглянуть на <a href=" logcom.oxfordjournals.org/content/5/2/…> Давара . показывает , что , если есть логика для Р, то есть одна за счет расширения ВОЛП с обобщенными кванторами.
slimton
3
Я должен добавить, что Horn-фрагмент экзистенциальной логики второго порядка на голых структурах довольно слаб: надлежащее подмножество LFP на голых структурах. Нам нужен преемник, чтобы получить теорему Гределя. Результат Давара для голых структур.
Слитон
8
Насколько я понимаю, линейная логика может выражать только утверждения о структурах, которые имеют довольно ограничительную форму. В идеале я хотел бы видеть ссылку или набросок логики, которая может выражать свойства произвольных наборов реляционных структур, но при этом избегать фиксированных точек. Если я ошибаюсь по поводу выразительной силы линейной логики, тогда приветствуется указатель или подсказка.

Это не правильно: все вычлененные коммутативные моноидальные решетки являются моделями линейной логики. Вот простой способ создать такую ​​решетку из конечных графов. Начните с набора

M={(g,n)|g is a finite graph and nnodes(g)}

(g,n)ϕnϕ():M×MM

(g,n)(g,n)={(g,nn)when g=gnn=undefinedotherwise

Это объединяет два элемента путем объединения их собственных наборов, если графики равны, а собственные наборы не пересекаются.

Теперь мы можем дать модель линейной логики следующим образом:

(g,n)In=(g,n)ϕψn1,n2.n=n1n2 and (g,n1)ϕ and (g,n2)ψ(g,n)ϕψn.if nn= and (g,n)ϕ then (g,nn)ψ(g,n)always(g,n)ϕψ(g,n)ϕ and (g,n)ψ

Эта модель фактически является вариантом моделей, используемых в логике разделения, которая широко используется при проверке программ, управляющих кучей. (Если хотите, подумайте о графике как о структуре указателя кучи, и аналогия точна!)

Однако это не совсем правильный подход к линейной логике: ее реальные интуиции являются теоретико-доказательственными, а связь со сложностью происходит через вычислительную сложность теоремы об исключении разреза. Модельная теория линейной логики является тенью, отбрасываемой ее теорией доказательств.

Нил Кришнасвами
источник
Какую роль играет структура графа в приведенной выше модели? Вышеприведенное определение, кажется, работает нормально, если мы говорим, что g лежит в пределах дискретных графов.
Чарльз Стюарт
Поскольку любой (частичный) коммутативный моноид может использоваться для создания модели BI / линейной логики, структура графа не используется для интерпретации и - она ​​имеет значение только для атомарных высказываний. Например, в логике разделения есть атомное предложение «указывает на» , которое мы используем для интерпретации структуры указателя. nn
Нил Кришнасвами
8

В последнее время появляются захватывающие результаты поиска логики захвата PTIME. Известный пример Cai, Fürer и Immerman, показывающий, что LFP + C не захватывает PTIME, был основан на, казалось бы, искусственном классе графов. Конечно, он был построен для конкретной задачи демонстрации ограничений LFP + C. Только недавно Давар показал, что класс совсем не искусственный. Скорее это можно рассматривать как пример того факта, что LFP + C не может решать системы линейных уравнений!

Следовательно, Давар, Гроэ, Хольм и Лаубнер расширили логику с помощью операторов линейной алгебры, например, с помощью оператора для определения ранга определяемой матрицы. Результирующая логика LFP + rank может выражать строго больше, чем LFP + C, фактически нет известного свойства PTIME, которое LFP + rank не может выразить.

Даже FO + rk удивительно мощен, он может выражать детерминированное и симметричное транзитивное замыкание. Пока не ясно, может ли оно выражать общее транзитивное замыкание графа.

Себастьян Сибертц
источник
1
Обратите внимание, что Андерсон / Давар / Холм недавно показал, что FP + C может выражать линейное программирование ( arxiv.org/abs/1304.6870 ). Это подрывает интерпретацию более раннего результата Давара по принципу «FP + C не может решить системы линейных уравнений»; Давар только утверждал, что некоторые «естественные проблемы, связанные с системами линейных уравнений, не поддаются определению в этой логике», с которыми он, по-видимому, имел в виду ранговые вычисления.
Андрас Саламон
7

В зависимости от того, что вы подразумеваете под «захватом», может представлять интерес мягкая линейная логика и полиномиальное время Ива Лафона. В этой логике есть доказательства соответствия 1-1 и алгоритмы PTIME, которые принимают строку в качестве входных данных и выходных 0 или 1.

Статья Википедии о линейной логике находится здесь . Это не логика с фиксированной точкой. Мне легче всего понять интуицию «классической логики над -алгебрами вместо булевых алгебр».C

Аарон Стерлинг
источник
1
Я думаю, что Андраш хочет логики в смысле описательной сложности.
Каве
7

Некоторые более старые работы по этой проблеме, опять же в духе линейной логики, - это Жан-Ив Жирар, Андре Щедров и Филипп Скотт. Линейная ограниченная логика: модульный подход к вычислимости за полиномиальное время. Теоретическая информатика, 97 (1): 1–66, 1992.

Более поздние работы включают « Ограниченную линейную логику», пересмотренную Уго Дал Лаго и Мартином Хофманном.

Дэйв Кларк
источник