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

Понятие в математической логике

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Итерации

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

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

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

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

• ${\displaystyle {\mathsf {FO}}[(\log n)^{i}]}$равно FO-равномерному AC i , и фактически является FO-равномерным AC глубины . ^[15] ${\displaystyle {\mathsf {FO}}[t(n)]}$ ${\displaystyle t(n)}$
• ${\displaystyle {\mathsf {FO}}[(\log n)^{O(1)}]}$равно NC. ^[16]
• ${\displaystyle {\mathsf {FO}}[n^{O(1)}]}$равно PTIME . Это также другой способ записать FO(IFP). ^[17]
• ${\displaystyle {\mathsf {FO}}[2^{n^{O(1)}}]}$равно PSPACE . Это также другой способ записи FO(PFP). ^[18]

Примечания

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

Ссылки

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