Теория конечных моделей - Finite model theory

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

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

Основные задачи

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

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

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

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

Проблема

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

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

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

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

Подход

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

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

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

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

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

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

Расширение до бесконечной структуры

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

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

Характеристика класса структур

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

Набор до п конструкции.

Проблема

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

Подход

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

1. Основная идея заключается в том, что всякий раз, когда кто-то хочет узнать, п можно выразить в FO, выбираются структуры А и B, куда А имеет п и B нет. Если для А и B те же предложения FO верны, тогда п не может быть выражено в FO. Короче:

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

куда ${\displaystyle A\equiv B}$ сокращение для ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$ для всех FO-предложений α, и п представляет собой класс конструкций со свойством п.

2. Методология рассматривает счетное множество подмножеств языка, объединение которых образует сам язык. Например, для FO рассмотрим классы FO [м] для каждого м. Для каждого м Затем необходимо показать вышеупомянутую основную идею. То есть:

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

с парой ${\displaystyle A,B}$ для каждого ${\displaystyle m}$ и α (в) из FO [м]. Возможно, будет уместным выбрать классы FO [м], чтобы сформировать раздел языка.

3. Один из распространенных способов определения FO [м] с помощью ранг квантора qr (α) формулы ФО α, которая выражает глубину квантификатор гнездование. Например, для формулы в пренекс нормальная форма, qr - это просто общее количество его кванторов. Тогда FO [м] можно определить как все формулы ФО α с qr (α) ≤ м (или, если требуется разделение, как те формулы FO с кванторным рангом, равным м).

4. Таким образом, все сводится к показу ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$ на подмножествах FO [м]. Основной подход здесь заключается в использовании алгебраической характеризации, предоставляемой Игры Эренфойхта – Фраиссе. Неформально они принимают единственный частичный изоморфизм на А и B и продлить его м раз, чтобы доказать или опровергнуть ${\displaystyle A\equiv _{m}B}$, в зависимости от того, кто выиграет игру.

Пример

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

1. Идея состоит в том, чтобы выбрать А ∈ EVEN и B ∉ ЧЕТЫЕ, где ЧЕТЫЕ - это класс всех конструкций четного размера.

2. Начнем с двух упорядоченных структур А₂ и B₂ с вселенными A₂ = {1, 2, 3, 4} и B₂ = {1, 2, 3}. Очевидно А₂ ∈ EVEN и B₂ ∉ ДАЖЕ.

3. За м = 2, теперь мы можем показать *, что за 2 хода Игра Эренфойхта – Фраиссе на А₂ и B₂ дупликатор всегда выигрывает, и поэтому А₂ и B₂ не могут быть выделены в FO [2], т.е. А₂ ${\displaystyle \models }$ α ⇔ B₂ ${\displaystyle \models }$ α для любого α ∈ FO [2].

4. Затем нам нужно увеличить структуру, увеличив м. Например, для м = 3 мы должны найти А₃ и B₃ таким образом, что дубликатор всегда побеждает в игре с 3 ходами. Этого можно добиться с помощью A₃ = {1, ..., 8} и B₃ = {1, ..., 7}. В более общем плане мы можем выбрать A_м = {1, ..., 2^м} и B_м = {1, ..., 2^м-1}; для любого м дубликатор всегда выигрывает м-двигайте игру для этой пары структур *.

5. Таким образом, EVEN на конечных упорядоченных структурах не может быть выражено в FO.

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

Приложения

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

Существенный фрагмент SQL (а именно то, что эффективно реляционная алгебра ) основан на логике первого порядка (точнее можно перевести в реляционное исчисление предметной области посредством Теорема Кодда ), как показано в следующем примере: Представьте себе таблицу базы данных «GIRLS» со столбцами «FIRST_NAME» и «LAST_NAME». Это соответствует бинарному отношению, скажем, G (f, l) на FIRST_NAME X LAST_NAME. Запрос FO {l: G ('Джуди', l)}, который возвращает все фамилии, в которых имя - "Джуди", в SQL будет выглядеть так:

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

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

Далее мы хотим сделать более сложное утверждение. Следовательно, в дополнение к таблице «ДЕВУШКИ» у нас есть таблица «МАЛЬЧИКИ» также со столбцами «FIRST_NAME» и «LAST_NAME». Теперь мы хотим запросить фамилии всех девочек, у которых такая же фамилия, как у хотя бы одного из мальчиков. Запрос FO {(f, l): ∃h (G (f, l) ∧ B (h, l))}, и соответствующий оператор SQL:

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

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

выберите отдельный g.FIRST_NAME, g.LAST_NAME из GIRLS g, BOYS b, где g.LAST_NAME = b.LAST_NAME;

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

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

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

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

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

История

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

Цитаты

1. Феджин, Рональд (1993). «Теория конечных моделей - личная перспектива» (PDF). Теоретическая информатика. 116: 3–31. Дои:10.1016 / 0304-3975 (93) 90218-И.
2. Иммерман, Нил (1999). Описательная сложность. Нью-Йорк: Springer-Verlag. п.6. ISBN  0-387-98600-6.

Рекомендации

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

• Либкин Леонид (2004). Элементы теории конечных моделей. Springer. ISBN  3-540-21202-7.

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

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

дальнейшее чтение

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

внешняя ссылка

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