Введение
Свободно сгенерированная алгебраическая структура над данной сигнатурой. В универсальной алгебре и математической логике, термальная алгебра – это свободно сгенерированная алгебраическая структура над данной сигнатурой. Например, для сигнатуры, состоящей из одной бинарной операции, термальная алгебра над множеством X переменных является точно свободной магмой, порожденной X. Другими синонимами этого понятия являются абсолютно свободная алгебра и анархическая алгебра. С точки зрения теории категорий, термальная алгебра является начальным объектом для категории всех X-порожденных алгебр с одинаковой сигнатурой, и этот объект, единственный с точностью до изоморфизма, называется начальной алгеброй; он порождает все алгебры в категории посредством гомоморфного проецирования. Похожим понятием является вселенная Гербранда в логике, обычно используемая под этим названием в логическом программировании, которая (абсолютно свободно) определяется, исходя из множества констант и функциональных символов в наборе клауз. То есть, вселенная Гербранда состоит из всех основных термов: термов, не содержащих переменных. Атомная формула, или атом, обычно определяется как предикат, примененный к кортежу термов; основной атом – это предикат, в котором используются только основные термы. База Гербранда – это множество всех основных атомов, которые могут быть сформированы из символов предикатов в исходном наборе клауз и термов в его вселенной Гербранда. Эти два понятия названы в честь Жака Гербранда. Термальные алгебры также играют роль в семантике абстрактных типов данных, где объявление абстрактного типа данных задает сигнатуру многосортированной алгебраической структуры, а термальная алгебра является конкретной моделью этого объявления.
In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X. Other synonyms for the notion include absolutely free algebra and anarchic algebra. From a category theory perspective, a term algebra is the initial object for the category of all X generated algebras of the same signature, and this object, unique up to isomorphism, is called an initial algebra; it generates by homomorphic projection all algebras in the category. A similar notion is that of a Herbrand universe in logic, usually used under this name in logic programming, which is (absolutely freely) defined starting from the set of constants and function symbols in a set of clauses. That is, the Herbrand universe consists of all ground terms: terms that have no variables in them. An atomic formula or atom is commonly defined as a predicate applied to a tuple of terms; a ground atom is then a predicate in which only ground terms appear. The Herbrand base is the set of all ground atoms that can be formed from predicate symbols in the original set of clauses and terms in its Herbrand universe. These two concepts are named after Jacques Herbrand. Term algebras also play a role in the semantics of abstract data types, where an abstract data type declaration provides the signature of a multi sorted algebraic structure and the term algebra is a concrete model of the abstract declaration.
Универсальная алгебра
Тип — это набор символов функций, каждый из которых имеет связанную арите (т.е. число аргументов). Для любого неотрицательного целого числа n, обозначим через символы функций в типе с арите n. Константа — это символ функции с арите 0. Пусть — тип, а — непустое множество символов, представляющих символы переменных. (Для простоты предположим, что и не пересекаются.) Тогда множество термов типа над — это множество всех правильно сформированных строк, которые могут быть построены с использованием символов переменных из и констант и операций из . Формально, — это наименьшее множество, такое что:
— каждый символ переменной из является термом в , и каждый символ константы из также является термом в ;
— для всех и для всех символов функций и термов , строка является термом;
— для заданных термов , применение n-арного символа функции к ним представляет собой терм. Термин-алгебра типа над — это, по сути, алгебра типа , которая отображает каждое выражение в его строковое представление. Формально, определяется следующим образом:
Область определения — это . Для каждой унарной функции в , определяется как строка . Для всех и для каждой n-арной функции в и элементов из области определения, определяется как строка .
Термин-алгебра называется абсолютно свободной, потому что для любой алгебры типа и для любой функции , расширяется до единственного гомоморфизма , который просто вычисляет каждый терм в соответствующее значение. Формально, для каждого :
Если , то ;
Если , то ;
Если , где и , то .
— each variable symbol from is a term in , and so is each constant symbol from For all and for all function symbols and terms , we have the string — given terms , the application of an ary function symbol to them represents again a term. The term algebra of type over is, in summary, the algebra of type that maps each expression to its string representation. Formally, is defined as follows:
The domain of is For each nullary function in , is defined as the string For all and for each n ary function in and elements in the domain, is defined as the string
A term algebra is called absolutely free because for any algebra of type , and for any function , extends to a unique homomorphism , which simply evaluates each term to its corresponding value Formally, for each :
If , then If , then If where and , then .
База Гербранд
Подпись σ языка представляет собой тройку <O, F, P>, состоящую из алфавита констант O, символов функций F и предикатов P. Основа Гербранда подписи σ состоит из всех основных атомов σ: всех формул вида R(t1, …, tn), где t1, …, tn – это термы, не содержащие переменных (т.е. элементы вселенной Гербранда), а R – символ n-арной связи (т.е. предикат). В случае логики с равенством, она также содержит все уравнения вида t1 = t2, где t1 и t2 не содержат переменных.
Решаемость
Терминовые алгебры могут быть показаны решаемыми с помощью устранения кванторов. Сложность задачи принятия решений относится к классу НЕЭЛЕМЕНТАРНЫХ, поскольку бинарные конструкторы инъективны и, следовательно, являются функциями спаривания.