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

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

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

Аксиоматичность

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

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

Характеристика единой структуры

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

Отдельные графы (1) и (1'), обладающие общими свойствами.

Проблема

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

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

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

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

Подход

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

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

Набор до n структур.

Проблема

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

Подход

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

1. Основная идея заключается в том, что всякий раз, когда кто-то хочет увидеть, может ли свойство 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 .
2. Методика рассматривает счетное множество подмножеств языка, объединение которых образует сам язык. Например, для FO рассмотрим классы FO[ m ] для каждого m . Затем для каждого m необходимо продемонстрировать приведенную выше основную идею. То есть:

   $A\in P,B\not \in P$ и $A\equiv _{m}B$

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

Пример

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

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

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

сложности

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

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

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

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

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

Приложения

Теория баз данных

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

select LAST_NAME 
from GIRLS
where FIRST_NAME = 'Judy'

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

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

select FIRST_NAME, LAST_NAME 
from GIRLS
where LAST_NAME IN ( select LAST_NAME from BOYS );

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

select distinct g.FIRST_NAME, g.LAST_NAME 
from GIRLS g, BOYS b
where g.LAST_NAME=b.LAST_NAME;

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

Запрос и поиск

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

("Java" AND NOT "island") OR ("C#" AND NOT "music")

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

История

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

Ссылки

• Эббингауз, Хайнц-Дитер ; Флум, Йорг (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.