Uninterpreted function

In mathematical logic, an uninterpreted function^[1] or function symbol^[2] 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, or the empty theory, being the theory having an empty set of sentences (in analogy to an initial algebra). Theories with a non-empty set of equations are known as equational theories. The satisfiability problem for free theories is solved by syntactic unification; algorithms for the latter are used by interpreters for various computer languages, such as Prolog. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see E-Unification and Narrowing.

Example

An array can be specified by the following equational axiom:^{[note 1]}

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

This axiom can be used to deduce^{[note 2]}

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 for the functions select and store. All that is known is the axiom.

Discussion

The 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.^[3]

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
• Initial algebra
• Term algebra

References

1. Bryant, Lahiri, Seshia (2002) "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions". Computer Aided Verification 2404/2002, 106–122.
2. Franz Baader; Tobias Nipkow (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.
3. John McCarthy (1962). "Towards a Mathematical Science of Computation". IFIP Congress. North-Holland. pp. 21–28.

Notes

1. Here, select(a,i) informally designates the value of the ith element of a, written e.g. in C as a[i], while store(a,i,v) informally designates the array resulting from writing the value v to the ith element of a, written in C as a[i]=v. The axiom then informally means that the value obtained by the statements a[i]=v;return a[j]; equals v if i=j, and a[j], else.
2. This deduction corresponds to the computation of the value obtained by a[1]=-1;a[2]=-2;return a[1];