Теория конечных моделей

Теория конечных моделей — это раздел теории моделей . Теория моделей — это раздел логики , который занимается отношениями между формальным языком (синтаксисом) и его интерпретациями (семантикой). Теория конечных моделей — это ограничение теории моделей интерпретациями конечных структур , которые имеют конечную вселенную.

Поскольку многие центральные теоремы теории моделей не выполняются, если ограничиться конечными структурами, теория конечных моделей сильно отличается от теории моделей в своих методах доказательства. Центральные результаты классической теории моделей, которые не работают для конечных структур в рамках теории конечных моделей, включают теорему о компактности , теорему Гёделя о полноте и метод ультрапроизведений для логики первого порядка (FO). Хотя теория моделей имеет множество приложений к математической алгебре , теория конечных моделей стала «необычайно эффективной» ^[1]инструмент в информатике. Другими словами: «В истории математической логики наибольший интерес сосредоточился на бесконечных структурах. [...] Тем не менее, объекты, которые есть и хранятся в компьютерах, всегда конечны. Для изучения вычислений нам нужна теория конечных структур». ^[2] Таким образом, основными областями применения теории конечных моделей являются: теория описательной сложности , теория баз данных и теория формального языка .

Аксиоматичность [ править ]

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

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

Характеристика единой структуры [ править ]

Является ли язык L достаточно выразительным, чтобы аксиоматизировать одну конечную структуру S ?

Проблема [ править ]

Структура, подобная (1) на рисунке, может быть описана предложениями FO в логике графов типа

Каждый узел имеет ребро к другому узлу: $\forall _{x}\exists _{y}G(x,y).$
Ни один узел не имеет ребра сам по себе: $\forall _{x,y}(G(x,y)\Rightarrow x\neq y).$
Существует хотя бы один узел, связанный со всеми остальными : $\exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).$

Однако эти свойства не аксиоматизируют структуру, поскольку для структуры (1') указанные выше свойства также выполняются, однако структуры (1) и (1') не изоморфны.

Неформально вопрос заключается в том, будут ли при добавлении достаточного количества свойств эти свойства вместе точно описывать (1) и не будут действительны (все вместе) ни для какой другой структуры (с точностью до изоморфизма).

Подход [ править ]

Для одной конечной структуры всегда можно точно описать структуру одним предложением FO. Здесь принцип проиллюстрирован для структуры с одним бинарным отношением. $R$ и без констант:

сказать, что есть по крайней мере $n$ элементы: $\varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})$
сказать, что существует максимум $n$ элементы: $\varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)$
указать каждый элемент отношения $R$ : $\varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})$
указать каждый неэлемент отношения $R$ : $\varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})$

все для одного и того же кортежа $x_{1}..x_{n}$ , что дает предложение FO $\exists _{x_{1}}\dots \exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})$ .

Расширение на фиксированное количество структур [ править ]

Метод описания одной структуры с помощью предложения первого порядка легко распространить на любое фиксированное число структур. Уникальное описание можно получить дизъюнкцией описаний для каждой структуры. Например, для двух структур $A$ и $B$ с определительными предложениями $\varphi _{A}$ и $\varphi _{B}$ это было бы

\varphi _{A}\lor \varphi _{B}.

Расширение до бесконечной структуры [ править ]

По определению, множество, содержащее бесконечную структуру, выходит за рамки области, с которой имеет дело FMT. Обратите внимание, что бесконечные структуры никогда не могут быть дискриминированы в FO из-за теоремы Левенхайма-Скулема , которая подразумевает, что ни одна теория первого порядка с бесконечной моделью не может иметь уникальную модель с точностью до изоморфизма.

Самым известным примером, вероятно, является теорема Скулема о том, что существует счетная нестандартная модель арифметики.

Характеристика класса структур [ править ]

Является ли язык L достаточно выразительным, чтобы точно (с точностью до изоморфизма) описать те конечные структуры, которые обладают определенным свойством P ?

Проблема [ править ]

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

Подход [ править ]

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

Основная идея заключается в том, что всякий раз, когда кто-то хочет увидеть, может ли свойство P быть выражено в FO, он выбирает структуры A и B , где A имеет P , а B - нет. Если для A и B справедливы одни и те же предложения FO, то P не может быть выражено в FO. Суммируя:
$A\in P,B\not \in P$ и $A\equiv B,$
где $A\equiv B$ это сокращение от $A\models \alpha \Leftrightarrow B\models \alpha$ для всех FO-предложений α, а P представляет класс структур со свойством P .
Методика рассматривает счетное множество подмножеств языка, объединение которых образует сам язык. Например, для FO рассмотрим классы FO[ m ] для каждого m . Затем для каждого m необходимо продемонстрировать приведенную выше основную идею. То есть:
$A\in P,B\not \in P$ и $A\equiv _{m}B$
с парой $A,B$ для каждого $m$ и α (в ≡) из FO[ m ]. Может оказаться целесообразным выбрать классы FO[ m ] для формирования раздела языка.
Одним из распространенных способов определения FO[ m ] является использование ранга квантора qr(α) формулы FO α, который выражает глубину вложенности кванторов . Например, для формулы в пренексной нормальной форме qr — это просто общее количество ее кванторов. Тогда FO[ m ] можно определить как все формулы FO α с qr(α) ≤ m (или, если требуется разбиение, как формулы FO с кванторным рангом, равным m ).
Таким образом, все сводится к тому, чтобы показать $A\models \alpha \Leftrightarrow B\models \alpha$ на подмножествах FO[ m ]. Основной подход здесь заключается в использовании алгебраической характеристики, обеспечиваемой играми Эренфойхта – Фрессе . Неформально они берут один частичный изоморфизм на A и B и расширяют его m раз, чтобы либо доказать, либо опровергнуть. $A\equiv _{m}B$ , в зависимости от того, кто выиграет игру.

Пример [ править ]

размера упорядоченной структуры A Мы хотим показать, что свойство четности = (A, ≤) не может быть выражено в FO.

Идея состоит в том, чтобы выбрать $A \in EVEN$ и $B \notin EVEN$ , где EVEN — класс всех структур четного размера.
Начнем с двух упорядоченных структур A ₂ и B ₂ с вселенными A ₂ = {1, 2, 3, 4} и B ₂ = {1, 2, 3}. Очевидно, $\in A2 EVEN$ и $B2 \notin EVEN$ .
Для m = 2 мы теперь можем показать*, что в двухходовой игре Эренфойхта–Фрэссе на A ₂ и B ₂ всегда выигрывает дубликатор, и, следовательно, A ₂ и B ₂ не могут быть различимы в FO[2], т.е. $\mathbf {A} _{2}\models \alpha \iff \mathbf {B} _{2}\models \alpha$ для любого $α \in FO[2]$ .
Далее нам нужно масштабировать структуры, увеличивая m . Например, для m = 3 мы должны найти A ₃ и B ₃ такие, чтобы дубликатор всегда выигрывал игру в 3 хода. Этого можно добиться с помощью A ₃ = {1, ..., 8} и B ₃ = {1, ..., 7}. В более общем смысле мы можем выбрать A _m = {1, ..., 2 ^м} и B _m = {1, ..., 2 ^м−1}; для любого m дубликатор всегда выигрывает игру с m -ходами для этой пары структур*.
Таким образом, EVEN на конечных упорядоченных структурах не может быть выражено в FO.

(*) Обратите внимание, что доказательство результата игры Эренфойхта–Фрэссе опущено, поскольку оно не является здесь основной задачей.

нуля и единицы Законы

Глебский и др. (1969) и независимо Феджин (1976) доказал закон нуля и единицы для предложений первого порядка в конечных моделях; В доказательстве Феджина использовалась теорема о компактности . Согласно этому результату, каждое предложение первого порядка в реляционной сигнатуре $\sigma$ либо почти всегда истинно, либо почти всегда ложно в конечных $\sigma$ -структуры. То есть, пусть $S$ — фиксированное предложение первого порядка и выбираем случайное $\sigma$ -состав $G_{n}$ с доменом $\{1,\dots ,n\}$ , равномерно среди всех $\sigma$ -структуры с доменом $\{1,\dots ,n\}$ . Тогда в пределе, когда $n$ стремится к бесконечности, вероятность того, что $G n$ моделирует $S$ , будет стремиться либо к нулю, либо к единице:

\lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.

Проблема определения того, имеет ли данное предложение вероятность, стремящуюся к нулю или к единице, является PSPACE-полной . ^[3]

Аналогичный анализ был проведен для более выразительных логик, чем логика первого порядка. Было показано, что закон 0-1 справедлив для предложений в FO(LFP) , логике первого порядка, дополненной оператором наименьшей фиксированной точки, и, в более общем плане, для предложений в бесконечной логике. $L_{\infty \omega }^{\omega }$ , что допускает потенциально сколь угодно длинные соединения и дизъюнкции. Другим важным вариантом является немаркированный закон 0-1, в котором вместо учета доли структур с доменом $\{1,\dots ,n\}$ , рассматривается доля классов изоморфизма структур с $n$ элементами. Эта дробь четко определена, поскольку любые две изоморфные структуры удовлетворяют одним и тем же предложениям. Немаркированный закон 0-1 справедлив и для $L_{\infty \omega }^{\omega }$ и, следовательно, в частности для FO(LFP) и логики первого порядка. ^[4]

сложности Описательная теория

Важной целью теории конечных моделей является характеристика классов сложности по типу логики , необходимой для выражения языков в них. Например, PH , объединение всех классов сложности в полиномиальной иерархии, представляет собой именно класс языков, выражаемых утверждениями логики второго порядка . Эта связь между сложностью и логикой конечных структур позволяет легко переносить результаты из одной области в другую, облегчая использование новых методов доказательства и предоставляя дополнительные доказательства того, что основные классы сложности каким-то образом «естественны» и не привязаны к конкретным абстрактным машинам. используемым чтобы определить их.

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

Некоторые известные классы сложности фиксируются логическими языками следующим образом:

При наличии линейного порядка логика первого порядка с добавленным коммутативным транзитивным оператором замыкания дает L , проблемы, разрешимые в логарифмическом пространстве.
При наличии линейного порядка логика первого порядка с транзитивным оператором замыкания дает NL , проблемы, решаемые в недетерминированном логарифмическом пространстве.
При наличии линейного порядка логика первого порядка с оператором наименьшей неподвижной точки дает P , проблемы, решаемые за детерминированное полиномиальное время.
На всех конечных структурах (независимо от того, упорядочены ли они) экзистенциальная логика второго порядка дает NP ( теорема Феджина ). ^[5]

Приложения [ править ]

Теория баз данных [ править ]

Существенный фрагмент SQL (а именно тот, который фактически представляет собой реляционную алгебру ) основан на логике первого порядка (более точно может быть переведен в реляционное исчисление предметной области с помощью теоремы Кодда ), как иллюстрирует следующий пример: Подумайте о таблице базы данных. ДЕВУШКИ" с столбцами "FIRST_NAME" и "LAST_NAME". Это соответствует бинарному отношению, скажем, G(f, l) для FIRST_NAME × LAST_NAME. ФО-запрос ${l:G({\text{'Judy'}},l)}$ , который возвращает все фамилии, где первое имя — «Джуди», в SQL будет выглядеть следующим образом:

выберите   LAST_NAME  
 из   GIRLS, 
 где   FIRST_NAME   =   'Джуди'

Обратите внимание: здесь мы предполагаем, что все фамилии встречаются только один раз (или нам следует использовать SELECT DISTINCT, поскольку мы предполагаем, что отношения и ответы представляют собой наборы, а не пакеты).

Далее мы хотим сделать более сложное утверждение. Поэтому помимо таблицы "ДЕВОЧКИ" у нас есть таблица "МАЛЬЧИКИ" еще и со столбцами "FIRST_NAME" и "LAST_NAME". Теперь мы хотим запросить фамилии всех девочек, у которых такая же фамилия, как хотя бы у одного мальчика. Запрос FO ${(f,l):\exists h(G(f,l)\land B(h,l))}$ и соответствующий оператор SQL:

выберите   FIRST_NAME  ,   LAST_NAME  
 из   GIRLS 
 , где   LAST_NAME   IN   (   выберите   LAST_NAME   из   BOYS   );

Обратите внимание, что для выражения «∧» мы ввели новый языковой элемент «IN» с последующим оператором выбора. Это делает язык более выразительным за счет более высокой сложности изучения и реализации. Это обычный компромисс при проектировании формального языка. Показанный выше способ («IN») далеко не единственный способ расширения языка. Альтернативный способ – это, например, ввести оператор «JOIN», то есть:

выберите   отдельный   g  .   FIRST_NAME  ,   г.    ФАМИЛИЯ  
 из   ДЕВОЧКИ   г  ,   МАЛЬЧИКИ   б 
 где   г  .   LAST_NAME  =  б  .   ФАМИЛИЯ  ;

Логика первого порядка слишком ограничительна для некоторых приложений баз данных, например, из-за ее неспособности выразить транзитивное замыкание . Это привело к добавлению в языки запросов к базе данных более мощных конструкций, таких как рекурсивное With в SQL:1999 . Поэтому более выразительные логики, такие как логики с фиксированной точкой , изучаются в теории конечных моделей из-за их актуальности для теории баз данных и приложений.

Запрос и поиск [ править ]

Нарративные данные не содержат определенных отношений. Таким образом, логическая структура текстовых поисковых запросов может быть выражена в логике высказываний , например:

(«Java» И НЕ «остров») ИЛИ («C#» И НЕ «музыка»)

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

История [ править ]

Трахтенброт 1950 : несостоятельность теоремы о полноте в логике первого порядка
Шольц 1952: характеристика спектров в логике первого порядка
Феджин 1974 : набор всех свойств, выражаемых в экзистенциальной логике второго порядка, представляет собой именно класс сложности NP.
Чандра, Харель 1979/80: расширение логики первого порядка с фиксированной точкой для языков запросов к базе данных, способное выражать транзитивное замыкание -> запросы как центральные объекты FMT.
Иммерман , Варди 1982: логика фиксированной точки над упорядоченными структурами захватывает PTIME -> описательную сложность ( теорема Иммермана-Селепшени )
Эббингауз , Флюм 1995: первая всеобъемлющая книга «Теория конечных моделей».
Абитебул , Халл, Виану 1995: книга «Основы баз данных».
Иммерман 1999: книга « Описательная сложность ».
Купер, Либкин, Пареденс 2000: книга «Базы данных с ограничениями».
Дармштадт, 2005 г./ Аахен, 2006 г.: первые международные семинары по «Теории алгоритмических моделей».

Цитаты [ править ]

^ Феджин, Рональд (1993). «Теория конечных моделей – личный взгляд» (PDF) . Теоретическая информатика . 116 : 3–31. дои : 10.1016/0304-3975(93)90218-I . Архивировано из оригинала 23 июня 2021 г. Проверено 20 июля 2023 г. {{cite journal}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
^ Иммерман, Нил (1999). Описательная сложность . Нью-Йорк: Springer-Verlag. п. 6 . ISBN 0-387-98600-6 .
^ Гранжан, Этьен (1983). «Сложность теории первого порядка почти всех конечных структур» . Информация и контроль . 57 (2–3): 180–204. дои : 10.1016/S0019-9958(83)80043-6 .
^ Эббингауз, Хайнц-Дитер; Флум, Йорг (1995). «4». Теория конечных моделей . Перспективы математической логики. дои : 10.1007/978-3-662-03182-7 . ISBN 978-3-662-03184-1 .
^ Эббингауз, Хайнц-Дитер; Флум, Йорг (1995). «7». Теория конечных моделей . Перспективы математической логики. дои : 10.1007/978-3-662-03182-7 .

Ссылки [ править ]

Эббингауз, Хайнц-Дитер ; Флум, Йорг (1995). Теория конечных моделей . Спрингер . ISBN 978-3-540-60149-4 .

Феджин, Рональд (1976). «Вероятности в конечных моделях». Журнал символической логики . 41 (1): 50–58. дои : 10.2307/2272945 . JSTOR 2272945 .
Glebskiĭ, Yu V.; Kogan, D. I.; Liogon'kiĭ, M. I.; Talanov, V. A. (1969). "Объем и доля выполнимости формул узкого исчисления предикатов" [Volume and fraction of satisfiability of formulae of the first-order predicate calculus]. Kibernetika . 5 (2): 17–27. Also available as; «Область и степень реализуемости формул ограниченного исчисления предикатов». Кибернетика . 5 (2): 142–154. 1972. doi : 10.1007/BF01071084 .
Либкин, Леонид (2004). Элементы теории конечных моделей . Спрингер . ISBN 3-540-21202-7 .

Абитбул, Серж ; Халл, Ричард; Виану, Виктор (1995). Основы баз данных . Аддисон-Уэсли . ISBN 0-201-53771-0 .

Иммерман, Нил (1999). Описательная сложность . Нью-Йорк: Спрингер . ISBN 0-387-98600-6 .

Дальнейшее чтение [ править ]

Градель, Эрих; Колайтис, Фокион Г.; Либкин Леонид ; Мартин, Маркс; Спенсер, Джоэл ; Варди, Моисей Ю .; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения . Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag . ISBN 978-3-540-00428-8 . Збл 1133.03001 .

Внешние ссылки [ править ]

Либкин, Леонид (2009). «Набор инструментов теории конечных моделей теоретика баз данных». PODS 2009: Материалы двадцать восьмого симпозиума ACM SIGACT-SIGMOD по принципам систем баз данных . стр. 65–76. дои : 10.1145/1559795.1559807 . Также подходит в качестве общего введения и обзора.
Леонид Либкин. Вводная глава «Элементы теории конечных моделей». Архивировано 24 сентября 2015 г. в Wayback Machine . Мотивирует три основные области применения: базы данных, сложность и формальные языки.
Йоуко Вяэнянен. Краткий курс теории конечных моделей . Кафедра математики Хельсинкского университета. На основе лекций 1993-1994 гг.
Анудж Давар. Теория бесконечных и конечных моделей , слайды, Кембриджский университет, 2002.
«Теория алгоритмических моделей» . RWTH Ахен. Архивировано из оригинала 17 июля 2012 года . Проверено 7 ноября 2013 г. Включает список открытых проблем FMT.

[Fagin_history-1] Феджин, Рональд (1993). «Теория конечных моделей – личный взгляд» (PDF) . Теоретическая информатика . 116 : 3–31. дои : 10.1016/0304-3975(93)90218-I . Архивировано из оригинала 23 июня 2021 г. Проверено 20 июля 2023 г. {{cite journal}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )

[Immerman_history-2] Иммерман, Нил (1999). Описательная сложность . Нью-Йорк: Springer-Verlag. п. 6 . ISBN 0-387-98600-6 .

[3] Гранжан, Этьен (1983). «Сложность теории первого порядка почти всех конечных структур» . Информация и контроль . 57 (2–3): 180–204. дои : 10.1016/S0019-9958(83)80043-6 .

[4] Эббингауз, Хайнц-Дитер; Флум, Йорг (1995). «4». Теория конечных моделей . Перспективы математической логики. дои : 10.1007/978-3-662-03182-7 . ISBN 978-3-662-03184-1 .

[5] Эббингауз, Хайнц-Дитер; Флум, Йорг (1995). «7». Теория конечных моделей . Перспективы математической логики. дои : 10.1007/978-3-662-03182-7 .

[1]

[2]

[3]

[4]

[5]

Аксиоматичность [ править ]

Характеристика единой структуры [ править ]

Проблема [ править ]

Подход [ править ]

Расширение на фиксированное количество структур [ править ]

Расширение до бесконечной структуры [ править ]

Характеристика класса структур [ править ]

Проблема [ править ]

Подход [ править ]

Пример [ править ]

нуля и единицы Законы

сложности Описательная теория ​

Приложения [ править ]

Теория баз данных [ править ]

Запрос и поиск [ править ]

История [ править ]

Цитаты [ править ]

Ссылки [ править ]

Дальнейшее чтение [ править ]

Внешние ссылки [ править ]

сложности Описательная теория