In
universal algebra
Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples ("models") of algebraic structures.
For instance, rather than take particular groups as the object of study ...
and
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
, a term algebra is a freely generated
algebraic structure
In mathematics, an algebraic structure consists of a nonempty set ''A'' (called the underlying set, carrier set or domain), a collection of operations on ''A'' (typically binary operations such as addition and multiplication), and a finite set o ...
over a given
signature
A signature (; from la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and ...
. For example, in a
signature
A signature (; from la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and ...
consisting of a single
binary operation
In mathematics, a binary operation or dyadic operation is a rule for combining two elements (called operands) to produce another element. More formally, a binary operation is an operation of arity two.
More specifically, an internal binary op ...
, the term algebra over a set ''X'' of variables is exactly the
free magma
In abstract algebra, a magma, binar, or, rarely, groupoid is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation that must be closed by definition. No other properties are imposed.
...
generated by ''X''. Other synonyms for the notion include absolutely free algebra and anarchic algebra.
From a
category theory
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, ca ...
perspective, a term algebra is the
initial object
In category theory, a branch of mathematics, an initial object of a category is an object in such that for every object in , there exists precisely one morphism .
The dual notion is that of a terminal object (also called terminal element): ...
for the
category of all ''X''-generated algebras of the same signature, and this object, unique up to
isomorphism
In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word i ...
, is called an
initial algebra
In mathematics, an initial algebra is an initial object in the category of -algebras for a given endofunctor . This initiality provides a general framework for induction and recursion.
Examples
Functor
Consider the endofunctor sending ...
; it generates by
homomorphic projection all algebras in the category.
A similar notion is that of a Herbrand universe in
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from prem ...
, usually used under this name in
logic programming
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
,
which is (absolutely freely) defined starting from the set of constants and function symbols in a set of
clauses
In language, a clause is a constituent that comprises a semantic predicand (expressed or not) and a semantic predicate. A typical clause consists of a subject and a syntactic predicate, the latter typically a verb phrase composed of a verb with ...
. That is, the Herbrand universe consists of all
ground term
In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables.
In first-order logic with identity, the sentence Q(a) \lor P(b ...
s: terms that have no variables in them.
An
atomic formula
In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
or atom is commonly defined as a
predicate
Predicate or predication may refer to:
* Predicate (grammar), in linguistics
* Predication (philosophy)
* several closely related uses in mathematics and formal logic:
**Predicate (mathematical logic)
**Propositional function
**Finitary relation, o ...
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
Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Coura ...
.
Term algebras also play a role in the
semantics
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...
of
abstract data type
In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a ''user'', of the data, specifically in terms of possible values, pos ...
s, 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.
Universal algebra
A type
is a set of function symbols, with each having an associated
arity
Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. ...
(i.e. number of inputs). For any non-negative integer
, let
denote the function symbols in
of arity
. A constant is a function symbol of arity 0.
Let
be a type, and let
be a non-empty set of symbols, representing the variable symbols. (For simplicity, assume
and
are disjoint.) Then the set of
terms of type
over
is the set of all well-formed
strings that can be constructed using the variable symbols of
and the constants and operations of
. Formally,
is the smallest set such that:
*
— 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
.
Example
As an example type inspired from integer arithmetic can be defined by
,
,
, and
for each
.
The best-known algebra of type
has the
natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called '' cardinal ...
as its domain and interprets
,
,
, and
in the usual way; we refer to it as
.
For the example variable set
, we are going to investigate the term algebra
of type
over
.
First, the set
of terms of type
over
is considered.
We use to flag its members, which maybe otherwise hard to recognize due to their uncommon syntactic form.
We have e.g.
*
, since
is a variable symbol;
*
, since
is a constant symbol; hence
*
, since
is a 2-ary function symbol; hence, in turn,
*
since
is a 2-ary function symbol.
More generally, each string in
corresponds to a
mathematical expression
In mathematics, an expression or mathematical expression is a finite combination of symbols that is well-formed according to rules that depend on the context. Mathematical symbols can designate numbers ( constants), variables, operations, f ...
built from the admitted symbols and written in
Polish prefix notation;
for example, the term
corresponds to the expression
in usual
infix notation
Infix notation is the notation commonly used in arithmetical and logical formulae and statements. It is characterized by the placement of operators between operands—" infixed operators"—such as the plus sign in .
Usage
Binary relations are ...
. No parentheses are needed to avoid ambiguities in Polish notation; e.g. the infix expression
corresponds to the term
.
To give some counter-examples, we have e.g.
*
, since
is neither an admitted variable symbol nor an admitted constant symbol;
*
, for the same reason,
*
, since
is a 2-ary function symbol, but is used here with only one argument term (viz.
).
Now that the term set
is established, we consider the term algebra
of type
over
.
This algebra uses
as its domain, on which addition and multiplication need to be defined.
The addition function
takes two terms
and
and returns the term
; similarly, the multiplication function
maps given terms
and
to the term
.
For example,
evaluates to the term
.
As an example for unique extendability of a homomorphism consider
defined by
and
.
Informally,
defines an assignment of values to variable symbols, and once this is done, every term from
can be evaulated in a unique way in
.
For example,
:
In a similar way, one obtains
.
Herbrand base
The signature ''σ'' of a language is a triple <''O'', ''F'', ''P''> consisting of the alphabet of constants ''O'', function symbols ''F'', and predicates ''P''. The Herbrand base of a signature σ consists of all ground atoms of ''σ'': of all formulas of the form ''R''(''t''
1, ..., ''t''
''n''), where ''t''
1, ..., ''t''
''n'' are terms containing no variables (i.e. elements of the Herbrand universe) and ''R'' is an ''n''-ary relation symbol (''i.e.''
predicate
Predicate or predication may refer to:
* Predicate (grammar), in linguistics
* Predication (philosophy)
* several closely related uses in mathematics and formal logic:
**Predicate (mathematical logic)
**Propositional function
**Finitary relation, o ...
). In the case of logic with equality, it also contains all equations of the form ''t''
1 = ''t''
2, where ''t''
1 and ''t''
2 contain no variables.
Decidability
Term algebras can be shown decidable using
quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...
. The complexity of the decision problem is in
NONELEMENTARY because binary constructors are injective and thus pairing functions.
[Jeanne Ferrante; Charles W. Rackoff (1979). ''The Computational Complexity of Logical Theories''. ]Springer
Springer or springers may refer to:
Publishers
* Springer Science+Business Media, aka Springer International Publishing, a worldwide publishing group founded in 1842 in Germany formerly known as Springer-Verlag.
** Springer Nature, a multinationa ...
, Chapter 8, Theorem 1.2.
See also
*
Answer-set programming
*
Clone (algebra) In universal algebra, a clone is a set ''C'' of finitary operations on a set ''A'' such that
*''C'' contains all the projections , defined by ,
*''C'' is closed under (finitary multiple) composition (or "superposition"): if ''f'', ''g''1, …, '' ...
*
Domain of discourse
In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range.
Overview
The doma ...
/
Universe (mathematics)
In mathematics, and particularly in set theory, category theory, type theory, and the foundations of mathematics, a universe is a collection that contains all the entities one wishes to consider in a given situation.
In set theory, universes ar ...
*
Rabin's tree theorem (the monadic theory of the infinite
complete binary tree is decidable)
*
Initial algebra
In mathematics, an initial algebra is an initial object in the category of -algebras for a given endofunctor . This initiality provides a general framework for induction and recursion.
Examples
Functor
Consider the endofunctor sending ...
*
Abstract data type
In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a ''user'', of the data, specifically in terms of possible values, pos ...
*
Term rewriting system
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or redu ...
References
Further reading
* Joel Berman (2005)
"The structure of free algebras" In ''Structural Theory of Automata, Semigroups, and Universal Algebra''.
Springer
Springer or springers may refer to:
Publishers
* Springer Science+Business Media, aka Springer International Publishing, a worldwide publishing group founded in 1842 in Germany formerly known as Springer-Verlag.
** Springer Nature, a multinationa ...
. pp. 47–76. .
External links
* {{mathworld, urlname=HerbrandUniverse, title=Herbrand Universe
Universal algebra
Mathematical logic
Free algebraic structures
Unification (computer science)