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 example of uninterpreted functions in SMT-LIB, an input standard for SMT Solvers:

(declare-fun f (Int) Int)
(assert (= (f 10) 1))

This is satisfiable: f is an uninterpreted function. All that is known about f is its signature, so it is possible that f(10) = 1.

(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))

This is unsatisfiable: although f has no interpretation, it is impossible that it returns different values for the same input.

Discussion

The decision problem for free theories is particularly important, as many theories can be reduced to it.

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

gollark: FINALLY someone spells discreet right.
gollark: Bold of you to assume my productivity is above zero.
gollark: I found it on twitter. Apparently someone has an extremely cursed printer, and didn't even consistently describe the problem.
gollark: No, the repost detector is just bad.
gollark: MONKEYS

See also

Notes

    References
    1. 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. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4.
    2. Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.


    This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.