In mathematical logic, 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, 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 Unification (computer science).
Example
As an example of uninterpreted functions for SMT-LIB, if this input is given to an SMT solver:
(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), 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 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.[clarification needed] Solvers include satisfiability modulo theories solvers.
See also
- Algebraic data type
- Initial algebra
- Term algebra
- Theory of pure equality
Notes
References
- Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4. S2CID 9471360.
- Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.
- de Moura, Leonardo; Bjørner, Nikolaj (2009). Formal methods : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers (PDF). Berlin: Springer. ISBN 978-3-642-10452-7.
 | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
In mathematical logic 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 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 Unification computer science ExampleAs an example of uninterpreted functions for SMT LIB if this input is given to an SMT solver 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 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 DiscussionThe decision problem 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 clarification needed Solvers include satisfiability modulo theories solvers See alsoAlgebraic data type Initial algebra Term algebra Theory of pure equalityNotesReferencesBryant Randal E Lahiri Shuvendu K Seshia Sanjit A 2002 Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions PDF Computer Aided Verification Lecture Notes in Computer Science Vol 2404 pp 78 92 doi 10 1007 3 540 45657 0 7 ISBN 978 3 540 43997 4 S2CID 9471360 Baader Franz Nipkow Tobias 1999 Term Rewriting and All That Cambridge University Press p 34 ISBN 978 0 521 77920 3 de Moura Leonardo Bjorner Nikolaj 2009 Formal methods foundations and applications 12th Brazilian Symposium on Formal Methods SBMF 2009 Gramado Brazil August 19 21 2009 revised selected papers PDF Berlin Springer ISBN 978 3 642 10452 7 This formal methods related article is a stub You can help Wikipedia by expanding it vte
