Логика фиксированной точки

В математической логике логика с фиксированной точкой является расширением классической логики предикатов, которая была введена для выражения рекурсии. Их развитие было мотивировано описательной теорией сложности и их связью с языками запросов к базам данных , в частности с Datalog .

Логика наименьшей фиксированной точки впервые систематически изучалась Яннисом Н. Мошовакисом в 1974 году: ^[1] и он был представлен ученым-компьютерщикам в 1979 году, когда Альфред Ахо и Джеффри Уллман предложили логику с фиксированной запятой в качестве выразительного языка запросов к базе данных. ^[2]

Частичная логика с фиксированной точкой

Для реляционной подписи X FO[PFP]( X ) представляет собой набор формул, сформированных из X с использованием связок и предикатов первого порядка , переменных второго порядка , а также частичного оператора с фиксированной точкой. $\operatorname {PFP}$ используется для составления формул вида $[\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}$ , где $P$ является переменной второго порядка, ${\vec {x}}$ кортеж переменных первого порядка, ${\vec {t}}$ кортеж терминов и длины ${\vec {x}}$ и ${\vec {t}}$ совпадают с арностью $P$ .

Пусть $k$ — целое число, $x,y$ — векторы $k$ переменных, $P$ — переменная второго порядка арности $k$ , и пусть $φ$ — функция FO(PFP,X), использующая $x$ и $P$ в качестве переменных. Мы можем итеративно определить $(P_{i})_{i\in N}$ такой, что $P_{0}(x)=false$ и $P_{i}(x)=\varphi (P_{i-1},x)$ (имеется в виду $φ$ с $P_{i-1}$ заменена на переменную второго порядка $P$ ). Тогда либо существует фиксированная точка, либо список $(P_{i})$ s является циклическим. ^[3]

$[\operatorname {PFP} _{P,x}\varphi (y)]$ определяется как значение фиксированной точки $(P_{i})$ по $y,$ если есть фиксированная точка, иначе как ложь. ^[4] Поскольку $P$ s являются свойствами арности $k$ , существует не более $2^{n^{k}}$ ценности для $P_{i}$ s, поэтому с помощью счетчика полиномиального пространства мы можем проверить, есть ли цикл или нет. ^[5]

Доказано, что на упорядоченных конечных структурах свойство выражается в FO(PFP, X ) тогда и только тогда, когда оно лежит в PSPACE . ^[6]

Наименьшая логика с фиксированной точкой

Поскольку повторяющиеся предикаты, участвующие в вычислении частичной фиксированной точки, в целом не являются монотонными, фиксированная точка не всегда может существовать. FO(LFP,X), логика наименьшей фиксированной точки , представляет собой набор формул в FO(PFP,X), где частичная фиксированная точка берется только над такими формулами $φ$ , которые содержат только положительные вхождения $P$ (то есть вхождения, предшествовавшие четным числом отрицаний). Это гарантирует монотонность конструкции с фиксированной точкой (то есть, если переменная второго порядка равна $P$ , то $P_{i}(x)$ всегда подразумевает $P_{i+1}(x)$ ).

Из-за монотонности мы добавляем в таблицу истинности $P$ только векторы , и поскольку существуют только $n^{k}$ возможных векторов, мы всегда найдем фиксированную точку раньше $n^{k}$ итерации. Теорема Иммермана-Варди, независимо показанная Иммерманом. ^[7] и Варди , ^[8] показывает, что FO(LFP, X ) характеризует P во всех упорядоченных структурах.

Выразительность логики наименьшей фиксированной точки точно совпадает с выразительностью языка запросов к базе данных Datalog , показывая, что в упорядоченных структурах Datalog может выражать именно те запросы, которые выполняются за полиномиальное время. ^[9]

Инфляционная логика фиксированной точки

Другой способ обеспечить монотонность конструкции с фиксированной точкой — добавлять только новые кортежи к $P$ на каждом этапе итерации, не удаляя кортежи, для которых $P$ больше не держится. Формально мы определяем $\operatorname {IFP} (\phi _{P,x})$ как $\operatorname {PFP} (\psi _{P,x})$ где $\psi (P,x)=\phi (P,x)\vee P(x)$ .

Эта инфляционная фиксированная точка согласуется с наименее фиксированной точкой, в которой определена последняя. Хотя на первый взгляд кажется, что инфляционная логика с фиксированной точкой должна быть более выразительной, чем логика с наименьшей фиксированной точкой, поскольку она поддерживает более широкий диапазон аргументов с фиксированной точкой, на самом деле каждая FO[IFP]( X )-формула эквивалентна к FO[LFP]( X )-формуле. ^[10]

Одновременная индукция

Хотя все введенные до сих пор операторы с фиксированной точкой выполняли итерацию только при определении одного предиката, многие компьютерные программы более естественно рассматривать как перебирающие несколько предикатов одновременно. Либо увеличивая арность операторов с фиксированной точкой, либо путем их вложения, каждая одновременная наименьшая, инфляционная или частичная фиксированная точка может фактически быть выражена с использованием соответствующих одноитерационных конструкций, обсуждавшихся выше. ^[11]

Логика транзитивного замыкания

Вместо того, чтобы допускать индукцию по произвольным предикатам, логика транзитивного замыкания позволяет только транзитивные замыкания напрямую выражать .

FO[TC]( X ) — это набор формул, образованных из X с использованием связок и предикатов первого порядка, переменных второго порядка, а также оператора транзитивного замыкания. $\operatorname {TC}$ используется для составления формул вида $[\operatorname {TC} _{{\vec {x}},{\vec {y}}}\varphi ]{\vec {s}}{\vec {t}}$ , где ${\vec {x}}$ и ${\vec {y}}$ представляют собой кортежи попарно различных переменных первого порядка, ${\vec {t}}$ и ${\vec {s}}$ кортежи термов и длины ${\vec {x}}$ , ${\vec {y}}$ , ${\vec {s}}$ и ${\vec {t}}$ совпадают.

TC определяется следующим образом: пусть $k$ — целое положительное число и $u,v,x,y$ — векторы $k$ переменных. Затем ${\mathsf {TC}}(\phi _{u,v})(x,y)$ верно, если существует $n$ векторов переменных $(z_{i})$ такой, что $z_{1}=x,z_{n}=y$ , и для всех $i<n$ , $\phi (z_{i},z_{i+1})$ это правда. Здесь $φ$ — формула, записанная на FO(TC), а $\phi (x,y)$ означает, что переменные $u$ и $v$ заменяются на $x$ и $y$ .

Для упорядоченных структур FO[TC] характеризует класс сложности NL . ^[12] Эта характеристика является важной частью доказательства Иммермана, что NL замкнуто относительно дополнения (NL = co-NL). ^[13]

Детерминированная логика транзитивного замыкания

FO[DTC]( X ) определяется как FO(TC,X), где оператор транзитивного замыкания является детерминированным. Это означает, что когда мы применяем $\operatorname {DTC} (\phi _{u,v})$ , мы знаем, что для всех $u$ существует не более одного $v$ такого, что $\phi (u,v)$ .

Мы можем предположить, что $\operatorname {DTC} (\phi _{u,v})$ это синтаксический сахар для $\operatorname {TC} (\psi _{u,v})$ где $\psi (u,v)=\phi (u,v)\wedge \forall x(x=v\vee \neg \phi (u,x))$ .

характеризует класс сложности L. Для упорядоченных структур FO[DTC ] ^[12]

Итерации

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

Мы определим первый порядок с помощью итерации, ${\mathsf {FO}}[t(n)]$ ; здесь $t(n)$ - это (класс) функций от целых чисел до целых чисел и для разных классов функций $t(n)$ мы получим разные классы сложности ${\mathsf {FO}}[t(n)]$ .

В этом разделе мы напишем $(\forall xP)Q$ означать $(\forall x(P\Rightarrow Q))$ и $(\exists xP)Q$ означать $(\exists x(P\wedge Q))$ . Сначала нам нужно определить блоки кванторов (QB). Блок кванторов представляет собой список. $(Q_{1}x_{1},\phi _{1})...(Q_{k}x_{k},\phi _{k})$ где $\phi _{i}$ s — бескванторные FO-формулы и $Q_{i}$ либо $\forall$ или $\exists$ . Если $Q$ — блок кванторов, мы вызовем $[Q]^{t(n)}$ оператор итерации, который определяется как $Q,$ записанный $t(n)$ время. Следует обратить внимание, что здесь есть $k*t(n)$ кванторы в списке, но $только k переменных и каждая из этих переменных$ используются $t(n)$ раз. ^[14]

Теперь мы можем определить ${\mathsf {FO}}[t(n)]$ быть FO-формулами с итерационным оператором, показатель степени которого находится в классе $t(n)$ , и получаем следующие равенства:

${\mathsf {FO}}[(\log n)^{i}]$ равен FO-равномерному AC ^я, и на самом деле ${\mathsf {FO}}[t(n)]$ является FO-равномерным АС глубины $t(n)$ . ^[15]
${\mathsf {FO}}[(\log n)^{O(1)}]$ равен НК. ^[16]
${\mathsf {FO}}[n^{O(1)}]$ равен PTIME . Это еще один способ записи FO(IFP). ^[17]
${\mathsf {FO}}[2^{n^{O(1)}}]$ равен PSPACE . Это еще один способ записи FO(PFP). ^[18]

Примечания

^ Мошовакис, Яннис Н. (1974). «Элементарная индукция по абстрактным структурам» . Исследования по логике и основам математики . 77 . дои : 10.1016/s0049-237x(08)x7092-2 . ISBN 9780444105370 . ISSN 0049-237X .
^ Ахо, Альфред В.; Уллман, Джеффри Д. (1979). «Универсальность языков поиска данных» . Материалы 6-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '79 . Нью-Йорк, Нью-Йорк, США: ACM Press: 110–119. дои : 10.1145/567752.567763 . S2CID 3242505 .
^ Эббингауз и Флум, с. 121
^ Эббингауз и Флум, с. 121
^ Иммерман 1999, с. 161
^ Абитбул, С.; Виану, В. (1989). «Расширения Fixpoint логики первого порядка и языков, подобных журналам данных» . [1989] Труды. Четвертый ежегодный симпозиум по логике в информатике . IEEE-компьютер. Соц. Нажимать. стр. 71–79. дои : 10.1109/lics.1989.39160 . ISBN 0-8186-1954-6 . S2CID 206437693 .
^ Иммерман, Нил (1986). «Реляционные запросы, вычисляемые за полиномиальное время» . Информация и контроль . 68 (1–3): 86–104. дои : 10.1016/s0019-9958(86)80029-8 .
^ Варди, Моше Ю. (1982). «Сложность реляционных языков запросов (расширенное резюме)». Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений - STOC '82 . Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 137–146. CiteSeerX 10.1.1.331.6045 . дои : 10.1145/800070.802186 . ISBN 978-0897910705 . S2CID 7869248 .
^ Эббингауз и Флум, с. 242
^ Юрий Гуревич и Сахарон Шелах, Расширение логики первого порядка с фиксированной точкой, Анналы чистой и прикладной логики 32 (1986) 265–280.
^ Эббингауз и Флум, стр. 179, 193.
^ Jump up to: ^а ^б Иммерман, Нил (1983). «Языки, охватывающие классы сложности» . Материалы пятнадцатого ежегодного симпозиума ACM по теории вычислений - STOC '83 . Нью-Йорк, Нью-Йорк, США: ACM Press. стр. 347–354. дои : 10.1145/800061.808765 . ISBN 0897910990 . S2CID 7503265 .
^ Иммерман, Нил (1988). «Недетерминированное пространство закрыто при дополнении» . SIAM Journal по вычислительной технике . 17 (5): 935–938. дои : 10.1137/0217058 . ISSN 0097-5397 .
^ Иммерман 1999, с. 63
^ Иммерман 1999, с. 82
^ Иммерман 1999, с. 84
^ Иммерман 1999, с. 58
^ Иммерман 1999, с. 161

Ссылки

Эббингауз, Хайнц-Дитер; Флум, Йорг (1999). Теория конечных моделей . Перспективы математической логики (2-е изд.). Спрингер. дои : 10.1007/978-3-662-03182-7 . ISBN 978-3-662-03184-1 .
Нил, Иммерман (1999). Описательная сложность . Спрингер. ISBN 0-387-98600-6 . OCLC 901297152 .

[1] Мошовакис, Яннис Н. (1974). «Элементарная индукция по абстрактным структурам» . Исследования по логике и основам математики . 77 . дои : 10.1016/s0049-237x(08)x7092-2 . ISBN 9780444105370 . ISSN 0049-237X .

[2] Ахо, Альфред В.; Уллман, Джеффри Д. (1979). «Универсальность языков поиска данных» . Материалы 6-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '79 . Нью-Йорк, Нью-Йорк, США: ACM Press: 110–119. дои : 10.1145/567752.567763 . S2CID 3242505 .

[3] Эббингауз и Флум, с. 121

[4] Эббингауз и Флум, с. 121

[5] Иммерман 1999, с. 161

[6] Абитбул, С.; Виану, В. (1989). «Расширения Fixpoint логики первого порядка и языков, подобных журналам данных» . [1989] Труды. Четвертый ежегодный симпозиум по логике в информатике . IEEE-компьютер. Соц. Нажимать. стр. 71–79. дои : 10.1109/lics.1989.39160 . ISBN 0-8186-1954-6 . S2CID 206437693 .

[7] Иммерман, Нил (1986). «Реляционные запросы, вычисляемые за полиномиальное время» . Информация и контроль . 68 (1–3): 86–104. дои : 10.1016/s0019-9958(86)80029-8 .

[8] Варди, Моше Ю. (1982). «Сложность реляционных языков запросов (расширенное резюме)». Материалы четырнадцатого ежегодного симпозиума ACM по теории вычислений - STOC '82 . Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 137–146. CiteSeerX 10.1.1.331.6045 . дои : 10.1145/800070.802186 . ISBN 978-0897910705 . S2CID 7869248 .

[9] Эббингауз и Флум, с. 242

[10] Юрий Гуревич и Сахарон Шелах, Расширение логики первого порядка с фиксированной точкой, Анналы чистой и прикладной логики 32 (1986) 265–280.

[11] Эббингауз и Флум, стр. 179, 193.

[:0-12] Jump up to: ^а ^б Иммерман, Нил (1983). «Языки, охватывающие классы сложности» . Материалы пятнадцатого ежегодного симпозиума ACM по теории вычислений - STOC '83 . Нью-Йорк, Нью-Йорк, США: ACM Press. стр. 347–354. дои : 10.1145/800061.808765 . ISBN 0897910990 . S2CID 7503265 .

[13] Иммерман, Нил (1988). «Недетерминированное пространство закрыто при дополнении» . SIAM Journal по вычислительной технике . 17 (5): 935–938. дои : 10.1137/0217058 . ISSN 0097-5397 .

[14] Иммерман 1999, с. 63

[15] Иммерман 1999, с. 82

[16] Иммерман 1999, с. 84

[17] Иммерман 1999, с. 58

[18] Иммерман 1999, с. 161

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]