For faster navigation, this Iframe is preloading the Wikiwand page for Uninterpreted function.

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

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

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. Vol. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4. S2CID 9471360.
  2. ^ Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.
  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.
{{bottomLinkPreText}} {{bottomLinkText}}
Uninterpreted function
Listen to this article

This browser is not supported by Wikiwand :(
Wikiwand requires a browser with modern capabilities in order to provide you with the best reading experience.
Please download and use one of the following browsers:

This article was just edited, click to reload
This article has been deleted on Wikipedia (Why?)

Back to homepage

Please click Add in the dialog above
Please click Allow in the top-left corner,
then click Install Now in the dialog
Please click Open in the download dialog,
then click Install
Please click the "Downloads" icon in the Safari toolbar, open the first download in the list,
then click Install
{{::$root.activation.text}}

Install Wikiwand

Install on Chrome Install on Firefox
Don't forget to rate us

Tell your friends about Wikiwand!

Gmail Facebook Twitter Link

Enjoying Wikiwand?

Tell your friends and spread the love:
Share on Gmail Share on Facebook Share on Twitter Share on Buffer

Our magic isn't perfect

You can help our automatic cover photo selection by reporting an unsuitable photo.

This photo is visually disturbing This photo is not a good choice

Thank you for helping!


Your input will affect cover photo selection, along with input from other users.

X

Get ready for Wikiwand 2.0 🎉! the new version arrives on September 1st! Don't want to wait?