Термин алгебра

В универсальной алгебре и математической логике термальная алгебра представляет собой свободно порождаемую алгебраическую структуру по заданной сигнатуре . ^[1]^[2] Например, в сигнатуре , состоящей из одной бинарной операции , термин алгебра над набором X переменных — это в точности свободная магма порожденная X. , Другие синонимы этого понятия включают абсолютно свободную алгебру и анархическую алгебру . ^[3]

С точки зрения теории категорий , терминальная алгебра является исходным объектом для категории всех X -порожденных алгебр одной и той же сигнатуры , и этот объект, уникальный с точностью до изоморфизма , называется исходной алгеброй ; он порождает гомоморфным проектированием все алгебры в категории. ^[4]^[5]

Аналогичным понятием является вселенная Эрбрана в логике , обычно используемая под этим названием в логическом программировании . ^[6] который (абсолютно свободно) определяется, начиная с набора констант и функциональных символов в наборе предложений . То есть вселенная Эрбрана состоит из всех основных терминов : терминов, в которых нет переменных.

Атомная формула или атом обычно определяется как предикат, применяемый к кортежу терминов; тогда основной атом является предикатом, в котором появляются только основные термины. База Эрбрана — это набор всех основных атомов, которые могут быть образованы из символов-предикатов в исходном наборе предложений и терминов во вселенной Эрбрана. ^[7]^[8] Эти две концепции названы в честь Жака Эрбрана .

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

Универсальная алгебра [ править ]

Тип $\tau$ представляет собой набор функциональных символов, каждый из которых имеет соответствующую арность (т. е. количество входов). Для любого неотрицательного целого числа $n$ , позволять $\tau _{n}$ обозначают функциональные символы в $\tau$ арности $n$ . Константа — это функциональный символ арности 0.

Позволять $\tau$ быть типом, и пусть $X$ быть непустым набором символов, представляющим переменные символы. (Для простоты предположим, что $X$ и $\tau$ не пересекаются.) Тогда множество слагаемых $T(X)$ типа $\tau$ над $X$ — это набор всех правильно сформированных строк , которые можно построить с использованием переменных символов $X$ а константы и операции $\tau$ . Формально, $T(X)$ — наименьшее множество такое, что:

$X\cup \tau _{0}\subseteq T(X)$ — каждый переменный символ из $X$ это термин в $T(X)$ , как и каждый постоянный символ из $\tau _{0}$ .
Для всех $n\geq 1$ и для всех функциональных символов $f\in \tau _{n}$ и условия $t_{1},...,t_{n}\in T(X)$ , у нас есть строка $f(t_{1},...,t_{n})\in T(X)$ - данный $n$ условия $t_{1},...,t_{n}$ , применение $n$ -арный функциональный символ $f$ для них снова представляет собой термин.

Термин алгебра ${\mathcal {T}}(X)$ типа $\tau$ над $X$ Короче говоря, это алгебра типа $\tau$ который сопоставляет каждое выражение с его строковым представлением. Формально, ${\mathcal {T}}(X)$ определяется следующим образом: ^[9]

Домен ${\mathcal {T}}(X)$ является $T(X)$ .
Для каждой нулевой функции $f$ в $\tau _{0}$ , $f^{{\mathcal {T}}(X)}()$ определяется как строка $f$ .
Для всех $n\geq 1$ и для каждой n -арной функции $f$ в $\tau$ и элементы $t_{1},...,t_{n}$ в домене, $f^{{\mathcal {T}}(X)}(t_{1},...,t_{n})$ определяется как строка $f(t_{1},...,t_{n})$ .

Термовая алгебра называется абсолютно свободной , поскольку для любой алгебры ${\mathcal {A}}$ типа $\tau$ , и для любой функции $g:X\to {\mathcal {A}}$ , $g$ продолжается до единственного гомоморфизма $g^{\ast }:{\mathcal {T}}(X)\to {\mathcal {A}}$ , который просто оценивает каждый термин $t\in {\mathcal {T}}(X)$ до соответствующего значения $g^{\ast }(t)\in {\mathcal {A}}$ . Формально для каждого $t\in {\mathcal {T}}(X)$ :

Если $t\in X$ , затем $g^{\ast }(t)=g(t)$ .
Если $t=f\in \tau _{0}$ , затем $g^{\ast }(t)=f^{\mathcal {A}}()$ .
Если $t=f(t_{1},...,t_{n})$ где $f\in \tau _{n}$ и $n\geq 1$ , затем $g^{\ast }(t)=f^{\mathcal {A}}(g^{\ast }(t_{1}),...,g^{\ast }(t_{n}))$ .

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

В качестве примера тип, основанный на целочисленной арифметике, может быть определен следующим образом: $\tau _{0}=\{0,1\}$ , $\tau _{1}=\{\}$ , $\tau _{2}=\{+,*\}$ , и $\tau _{i}=\{\}$ для каждого $i>2$ .

Самая известная алгебра типа $\tau$ имеет натуральные числа в качестве области определения и интерпретирует $0$ , $1$ , $+$ , и $*$ обычным способом; мы называем это как ${\mathcal {A}}_{nat}$ .

Для примера набора переменных $X=\{x,y\}$ , мы собираемся исследовать термин алгебра ${\mathcal {T}}(X)$ типа $\tau$ над $X$ .

Во-первых, набор $T(X)$ терминов типа $\tau$ над $X$ считается.Мы используем красный цвет для обозначения его членов, которые в противном случае может быть трудно распознать из-за их необычной синтаксической формы.У нас есть, например

${\color {red}x}\in T(X)$ , с $x\in X$ — переменный символ;
${\color {red}1}\in T(X)$ , с $1\in \tau _{0}$ является постоянным символом; следовательно
${\color {red}+x1}\in T(X)$ , с $+$ — 2-арный функциональный символ; следовательно, в свою очередь,
${\color {red}*+x1x}\in T(X)$ с $*$ является 2-арным функциональным символом.

В более общем смысле каждая строка в $T(X)$ соответствует математическому выражению, построенному из допустимых символов и записанному в польской префиксной записи ;например, термин ${\color {red}*+x1x}$ соответствует выражению $(x+1)*x$ в обычной инфиксной записи . Во избежание двусмысленности в польских обозначениях скобки не нужны; например, инфиксное выражение $x+(1*x)$ соответствует термину ${\color {red}+x*1x}$ .

Чтобы привести несколько контрпримеров, мы имеем, например,

${\color {red}z}\not \in T(X)$ , с $z$ не является ни допустимым переменным символом, ни допустимым постоянным символом;
${\color {red}3}\not \in T(X)$ , по той же причине,
${\color {red}+1}\not \in T(X)$ , с $+$ является двухмерным функциональным символом, но используется здесь только с одним аргументом (а именно. ${\color {red}1}$ ).

Теперь, когда срок установлен $T(X)$ установлено, будем рассматривать термин алгебра ${\mathcal {T}}(X)$ типа $\tau$ над $X$ .В этой алгебре используется $T(X)$ как его область, в которой необходимо определить сложение и умножение.Функция сложения $+^{{\mathcal {T}}(X)}$ занимает два срока $p$ и $q$ и возвращает термин ${\color {red}+}pq$ ; аналогично функция умножения $*^{{\mathcal {T}}(X)}$ карты с учетом условий $p$ и $q$ к сроку ${\color {red}*}pq$ .Например, $*^{{\mathcal {T}}(X)}({\color {red}+x1},{\color {red}x})$ оценивается в термине ${\color {red}*+x1x}$ .Неформально операции $+^{{\mathcal {T}}(X)}$ и $*^{{\mathcal {T}}(X)}$ оба являются «ленивыми» в том смысле, что они просто записывают, какие вычисления следует выполнить, а не выполняют их.

В качестве примера однозначной расширяемости гомоморфизма рассмотрим $g:X\to {\mathcal {A}}_{nat}$ определяется $g(x)=7$ и $g(y)=3$ .Неофициально, $g$ определяет присвоение значений переменным символам, и как только это будет сделано, каждый термин из $T(X)$ можно оценить единственным способом ${\mathcal {A}}_{nat}$ .Например,

{\begin{array}{lll}&g^{*}({\color {red}+x1})\\=&g^{*}({\color {red}x})+g^{*}({\color {red}1})&{\text{ since }}g^{*}{\text{ is a homomorphism }}\\=&g({\color {red}x})+g^{*}({\color {red}1})&{\text{ since }}g^{*}{\text{ coincides on }}X{\text{ with }}g\\=&7+g^{*}({\color {red}1})&{\text{ by definition of }}g\\=&7+1&{\text{ since }}g^{*}{\text{ is a homomorphism }}\\=&8&{\text{ according to the well-known arithmetical rules in }}{\mathcal {A}}_{nat}\\\end{array}}

Аналогичным образом получают $g^{*}({\color {red}*+x1x})=...=8*g({\color {red}x})=...=56$ .

База Эрбранда

Сигнатура O σ языка — это тройка < , F , P > состоящая из алфавита констант O , функциональных символов F и предикатов P. , База Эрбран ^[10] сигнатуры σ состоит из всех основных атомов σ : всех формул вида R ( t ₁ , ..., t _n ), где t ₁ , ..., t _n — термины, не содержащие переменных (т. е. элементы сигнатуры σ). Вселенная Эрбрана), а R — это n- арный символ отношения ( т.е. предикат ). В случае логики с равенством она также содержит все уравнения вида где _, t1 и _t1 t2 не _{содержат} t2 переменных ₌ .

Разрешимость [ править ]

Алгебры термов можно показать разрешимыми с помощью исключения кванторов . Сложность проблемы решения НЕЭЛЕМЕНТАРНА, поскольку бинарные конструкторы являются инъективными и, следовательно, образуют пары. ^[11]

См. также [ править ]

Программирование набора ответов
Клон (алгебра)
Область дискурса / Вселенная (математика)
Теорема Рабина о дереве (монадическая теория бесконечного полного двоичного дерева разрешима)
Начальная алгебра
Абстрактный тип данных
Система переписывания терминов

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

^ Уилфрид Ходжес (1997). Теория более коротких моделей . Издательство Кембриджского университета . стр. 14 . ISBN 0-521-58713-1 .
^ Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета . п. 49. ИСБН 0-521-77920-0 .
^ Клаус Денеке; Шелли Л. Висмат (2009). Универсальная алгебра и коалгебра . Всемирная научная . стр. 21–23. ISBN 978-981-283-745-5 .
^ ТД Це (2010). Унифицированная структура для моделей структурного анализа и проектирования: подход, использующий исходную семантику алгебры и теорию категорий . Издательство Кембриджского университета . стр. 46–47. дои : 10.1017/CBO9780511569890 . ISBN 978-0-511-56989-0 .
^ Жан-Ив Безио (1999). «Математическая структура логического синтаксиса» . В Карниелли, Вальтер Александр; Д'Оттавиано, Итала М.Л. (ред.). Достижения в современной логике и информатике: материалы одиннадцатой бразильской конференции по математической логике, 6–10 мая 1996 г., Сальвадор, Баия, Бразилия . Американское математическое общество . п. 9. ISBN 978-0-8218-1364-5 . Проверено 18 апреля 2011 г.
^ Дирк ван Дален (2004). Логика и структура . Спрингер . п. 108. ИСБН 978-3-540-20879-2 .
^ М. Бен-Ари (2001). Математическая логика для информатики . Спрингер . стр. 148–150. ISBN 978-1-85233-319-5 .
^ Монро Ньюборн (2001). Автоматизированное доказательство теорем: теория и практика . Спрингер . п. 43. ИСБН 978-0-387-95075-4 .
^ Стэнли Беррис; HP Санкаппанавар (1981). Курс универсальной алгебры . Спрингер. стр. 68–69, 71. ISBN. 978-1-4613-8132-7 . {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )
^ Рохелио Давила. Обзор программирования набора ответов .
^ Жанна Ферранте; Чарльз В. Ракофф (1979). Вычислительная сложность логических теорий . Спрингер , глава 8, теорема 1.2.

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

Джоэл Берман (2005). «Строение свободных алгебр» . В структурной теории автоматов, полугрупп и универсальной алгебре . Спрингер . стр. 47–76. МИСТЕР 2210125 .

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

Вайсштейн, Эрик В. «Вселенная Эрбрана» . Математический мир .

[1] Уилфрид Ходжес (1997). Теория более коротких моделей . Издательство Кембриджского университета . стр. 14 . ISBN 0-521-58713-1 .

[2] Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета . п. 49. ИСБН 0-521-77920-0 .

[DeneckeWismath2009-3] Клаус Денеке; Шелли Л. Висмат (2009). Универсальная алгебра и коалгебра . Всемирная научная . стр. 21–23. ISBN 978-981-283-745-5 .

[Tse2010-4] ТД Це (2010). Унифицированная структура для моделей структурного анализа и проектирования: подход, использующий исходную семантику алгебры и теорию категорий . Издательство Кембриджского университета . стр. 46–47. дои : 10.1017/CBO9780511569890 . ISBN 978-0-511-56989-0 .

[CarnielliD'Ottaviano1999-5] Жан-Ив Безио (1999). «Математическая структура логического синтаксиса» . В Карниелли, Вальтер Александр; Д'Оттавиано, Итала М.Л. (ред.). Достижения в современной логике и информатике: материалы одиннадцатой бразильской конференции по математической логике, 6–10 мая 1996 г., Сальвадор, Баия, Бразилия . Американское математическое общество . п. 9. ISBN 978-0-8218-1364-5 . Проверено 18 апреля 2011 г.

[Dalen2004-6] Дирк ван Дален (2004). Логика и структура . Спрингер . п. 108. ИСБН 978-3-540-20879-2 .

[Ben-Ari2001-7] М. Бен-Ари (2001). Математическая логика для информатики . Спрингер . стр. 148–150. ISBN 978-1-85233-319-5 .

[Newborn2001-8] Монро Ньюборн (2001). Автоматизированное доказательство теорем: теория и практика . Спрингер . п. 43. ИСБН 978-0-387-95075-4 .

[Burris1981-9] Стэнли Беррис; HP Санкаппанавар (1981). Курс универсальной алгебры . Спрингер. стр. 68–69, 71. ISBN. 978-1-4613-8132-7 . {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )

[10] Рохелио Давила. Обзор программирования набора ответов .

[11] Жанна Ферранте; Чарльз В. Ракофф (1979). Вычислительная сложность логических теорий . Спрингер , глава 8, теорема 1.2.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]