||This article provides insufficient context for those unfamiliar with the subject. (October 2009)|
In mathematical logic, 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.
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 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, require algorithms for solving the free theory.
- select(store(a,i,v),j) = (if i = j then v else select(a,j))
This axiom can be used to deduce
- = 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.
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.
- 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.
- Franz Baader; Tobias Nipkow (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.
- J. McCarthy, (1962) "Towards a mathematical science of computation." IFIP Congress., pp. 21–28
|This formal methods-related article is a stub. You can help Wikipedia by expanding it.|