Term algebra
Encyclopedia
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, anarchic algebra.
From a category theory
perspective, a term algebra is the initial object
for the category of all 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.
An 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 which 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 type
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.
. The complexity of the decision problem is in NONELEMENTARY
.
consisting of the alphabet of constants O, the function symbols F, and the predicates P. The Herbrand base of a signature σ consists of all ground atoms of σ: of all formulas of the form R(t1, …, tn), where t1, …, tn are terms containing no variables (i.e. elements of the Herbrand universe) and R is an n-ary relation symbol (i.e. predicate). In the case of logic with equality, it also contains all equations of the form t1=t2, where t1 and t2 contain no variables.
Universal algebra
Universal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....
and mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a term algebra is a freely generated algebraic structure
Algebraic structure
In abstract algebra, an algebraic structure consists of one or more sets, called underlying sets or carriers or sorts, closed under one or more operations, satisfying some axioms. Abstract algebra is primarily the study of algebraic structures and their properties...
over a given signature
Signature (logic)
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language. In universal algebra, a signature lists the operations that characterize an algebraic structure. In model theory, signatures are used for both purposes.Signatures play the same...
. For example, in a signature consisting of a single binary operation
Binary operation
In mathematics, a binary operation is a calculation involving two operands, in other words, an operation whose arity is two. Examples include the familiar arithmetic operations of addition, subtraction, multiplication and division....
, 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, anarchic algebra.
From a category theory
Category theory
Category theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
perspective, a term algebra is the initial object
Initial object
In category theory, an abstract branch of mathematics, an initial object of a category C is an object I in C such that for every object X in C, there exists precisely one morphism I → X...
for the category of all algebras of the same signature
F-algebra
In mathematics, specifically in category theory, an F-algebra is a structure defined according to a functor F. F-algebras can be used to represent data structures used in programming, such as lists and trees...
, and this object, unique up to isomorphism is called an initial algebra
Initial algebra
In mathematics, an initial algebra is an initial object in the category of F-algebras for a given endofunctor F. The initiality provides a general framework for induction and recursion....
; it generates by homomorphic projection all algebras in the category.
An similar notion is that of a Herbrand universe in logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, usually used under this name in logic programming
Logic programming
Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
, which is (absolutely freely) defined starting from the set of constants and function symbols in a set of clauses
Clause (logic)
In logic, a clause is a finite disjunction ofliterals. Clausesare usually written as follows, where the symbols l_i areliterals:l_1 \vee \cdots \vee l_nIn some cases, clauses are written as sets of literals, so that clause above...
. That is, the Herbrand universe consists of all ground terms: terms which have no variables in them.
An atomic formula
Atomic formula
In mathematical logic, an atomic 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 subformulas. Atoms are thus the simplest well-formed formulas of the logic...
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
Jacques Herbrand
Jacques Herbrand was a French mathematician who was born in Paris, France and died in La Bérarde, Isère, France. Although he died at only 23 years of age, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse, and Richard Courant.He...
.
Term algebras also play a role in the semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
of abstract data type
Abstract data type
In computing, an abstract data type is a mathematical model for a certain class of data structures that have similar behavior; or for certain data types of one or more programming languages that have similar semantics...
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.
Decidability of term algebras
Term algebras can be shown decidable using quantifier eliminationQuantifier elimination
Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification...
. The complexity of the decision problem is in NONELEMENTARY
NONELEMENTARY
In computational complexity theory, the complexity class NONELEMENTARY is the complement of the class ELEMENTARY.Example decidable problems in NONELEMENTARY this class are:* the problem of regular expression equivalence with not...
.
Herbrand base
The signature σ of a language is a tripleSee also
- Domain of discourseDomain of discourseIn the formal sciences, the domain of discourse, also called the universe of discourse , is the set of entities over which certain variables of interest in some formal treatment may range...
/ Universe (mathematics)Universe (mathematics)In mathematics, and particularly in set theory and the foundations of mathematics, a universe is a class that contains all the entities one wishes to consider in a given situation... - Herbrand interpretationHerbrand interpretationIn mathematical logic, a Herbrand interpretation is an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it...
/ Herbrand structure - Answer-set programming