In 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...

, an uninterpreted function or function symbol is one that has no other property than its name and arity. Function symbols are used, together with constants and variables, to form terms

Term (logic)

In mathematical logic, universal algebra, and rewriting systems, terms are expressions which can be obtained from constant symbols, variables and function symbols...

.

The theory of uninterpreted functions is also sometimes called the free theory, because it is freely generated, and thus a free object

Free object

In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. It is a part of universal algebra, in the sense that it relates to all types of algebraic structure . It also has a formulation in terms of category theory, although this is in yet more abstract terms....

, or the empty theory, being the theory

Theory (mathematical logic)

In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...

 having an empty set of sentences

Sentence (mathematical logic)

In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...

 (in analogy to 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....

). Theories with a non-empty set of equations are known as equational theories. The decision problem

Decision problem

In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...

 for free theories is a satisfiability problem, and is solved by syntactic unification. It is particularly important, as many other theories can be reduced to it. Interpreters for various computer languages, such as Prolog

Prolog

Prolog is a general purpose 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 declarative: the program logic is expressed in terms of...

, require algorithms for solving the free theory.

Example

An array can be specified by the following equational axiom

Axiom

In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...

:

select(store(a,i,v),j) = (if i = j then v else select(a,j))

This axiom can be used to deduce

select(store(store(a,1,−1),2,−2),1)

= select(store(a,1,−1),1)

= −1

Note that this reasoning did not use any 'definition' or interpretation

Interpretation (logic)

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...

 for the functions select and store. All that is known is the axiom.

Discussion

The decision problem

Decision problem

In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...

 for free theories is particularly important, as many theories can be reduced to it; the above example is the prototypical example of the theory of arrays, where 'select' and 'store' are the canonical array access functions.

Free theories can be solved by searching for common subexpressions to form the congruence closure. Solvers include satisfiability modulo theories

Satisfiability Modulo Theories

In computer science, the Satisfiability Modulo Theories problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality...

solvers.