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

Свободно сгенерированная алгебраическая структура по заданной сигнатуре.

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

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

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

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

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

Универсальная алгебра

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

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

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

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

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

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

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

Пример

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

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

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

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

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

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

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

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

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

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

${\displaystyle {\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}}}$

Аналогичным образом получают . ${\displaystyle 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 -арным символом отношения ( т.е. предикатом ). В случае логики с равенством она также содержит все уравнения вида t ₁  =  t ₂ , где t ₁ и t ₂ не содержат переменных.

Разрешимость

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

Смотрите также

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

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

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

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

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

Внешние ссылки

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