In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, 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 elem ...
, or the empty theory, being the
theory
A theory is a systematic and rational form of abstract thinking about a phenomenon, or the conclusions derived from such thinking. It involves contemplative and logical reasoning, often supported by processes such as observation, experimentation, ...
having an empty set of
sentences
The ''Sentences'' (. ) is a compendium of Christian theology written by Peter Lombard around 1150. It was the most important religious textbook of the Middle Ages.
Background
The sentence genre emerged from works like Prosper of Aquitaine's ...
(in analogy to an
initial algebra
In mathematics, an initial algebra is an initial object in the Category (mathematics), category of F-algebra, -algebras for a given endofunctor . This initiality provides a general framework for mathematical induction, induction and recursion.
...
). 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 that has its origins in artificial intelligence, automated theorem proving, and computational linguistics.
Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...
. 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, specifically automated reasoning, unification is an algorithmic process of solving equations between symbolic expression (mathematics), expressions, each of the form ''Left-hand side = Right-hand side''. For example, ...
.
Example
As an example of uninterpreted functions for
SMT-LIB
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 involv ...
, 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 involv ...
:
(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 , "to sign") is a 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 intent. Signatures are often, but not always, Handwriting, handwritt ...
), 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 on a set of input values. An example of a decision problem is deciding whether a given natura ...
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. Solvers include
satisfiability modulo theories 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 data type, i.e., a data type formed by combining other types.
Two common classes of algebraic types are product ty ...
*
Initial algebra
In mathematics, an initial algebra is an initial object in the Category (mathematics), category of F-algebra, -algebras for a given endofunctor . This initiality provides a general framework for mathematical induction, induction and recursion.
...
*
Term algebra
Term may refer to:
Language
*Terminology, context-specific nouns or compound words
**Technical term (or ''term of art''), used by specialists in a field
***Scientific terminology, used by scientists
*Term (argumentation), part of an argument in d ...
*
Theory of pure equality
Notes
References
{{Formalmethods-stub
Specification languages