In
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 formal ...
, an uninterpreted function or function symbol is one that has no other property than its name and ''
n-ary'' form. Function symbols are used, together with constants and variables, to form
terms.
The theory of uninterpreted functions is also sometimes called the free theory, because it is freely generated, and thus a
free object
In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set ''A'' can be thought of as being a "generic" algebraic structure over ''A'': the only equations that hold between ele ...
, or the empty theory, being the
theory
A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may ...
having an empty set of
sentences
''The Four Books of Sentences'' (''Libri Quattuor Sententiarum'') is a book of theology written by Peter Lombard in the 12th century. It is a systematic compilation of theology, written around 1150; it derives its name from the '' sententiae'' ...
(in analogy to 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 ...
). Theories with a non-empty set of equations are known as
equational theories. The
satisfiability
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
problem for free theories is solved by
syntactic unification; algorithms for the latter are used by interpreters for various computer languages, such as
Prolog
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily a ...
. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see
Unification (computer science) In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
Depending on which expressions (also called ''terms'') are allowed to occur in an equation set (also called ''unification prob ...
.
Example
As an example of uninterpreted functions for SMT-LIB, if this input is given to an
SMT solver
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvin ...
:
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
the SMT solver would return "This input is satisfiable". That happens because
f is an uninterpreted function (i.e., all that is known about
f is its
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 ...
), so it is possible that
f(10) = 1. But by applying the input below:
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))
the SMT solver would return "This input is unsatisfiable". That happens because
f, being a function, can never return different values for the same input.
Discussion
The
decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm whethe ...
for free theories is particularly important, because many theories can be reduced by it.
Free theories can be solved by searching for
common subexpressions to form the
congruence closure
In mathematics, a subset of a given set is closed under an operation of the larger set if performing that operation on members of the subset always produces a member of that subset. For example, the natural numbers are closed under addition, but n ...
. Solvers include
satisfiability modulo theories
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvin ...
solvers.
See also
*
Algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., ...
*
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 ...
*
Term algebra
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 exa ...
*
Theory of pure equality
Notes
References
{{Formalmethods-stub
Specification languages