Uninterpreted function: Difference between revisions

Revision as of 13:44, 11 May 2014

Latest revision as of 15:10, 21 September 2024

(44 intermediate revisions by 19 users not shown)

Line 1:

{{Short description|Type of function in mathematical logic}}

{{Context|date=October 2009}}

In [[mathematical logic]], an '''uninterpreted function'''<ref>Bryant,{{Cite Lahiri,book Seshia| (2002)chapter-url=https://link.springer.com/content/pdf/10.1007/3-540-45657-0_7.pdf |doi = 10.1007/3-540-45657-0_7|chapter = "Modeling and verifyingVerifying systemsSystems usingUsing a logicLogic of counterCounter arithmeticArithmetic with lambdaLambda expressionsExpressions and uninterpretedUninterpreted functions".Functions|title = ''Computer Aided Verification''|volume = '''2404/|pages = 78–92|series = Lecture Notes in Computer Science|year = 2002''',|last1 106&ndash;122= Bryant|first1 = Randal E.|last2 = Lahiri|first2 = Shuvendu K.|last3 = Seshia|first3 = Sanjit A.|isbn = 978-3-540-43997-4| s2cid=9471360 }}</ref> or '''function symbol'''<ref>{{cite book |last1=Baader |author1first1=Franz |authorlink1=Franz Baader |author2last2=Nipkow |first2=Tobias |authorlink2=Tobias Nipkow |year=1999 |title=Term Rewriting and All That|year=1999 |publisher=Cambridge University Press |isbn=978-0-521-77920-3 |pagespage=34}}</ref> is one that has no other property than its name and arity.''[[Arity|n-ary]]'' form. Function symbols are used, together with constants and variables, to form [[term (logic)|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 (mathematical logic)|theory]] having an empty set of [[sentence (mathematical logic)|sentences]] (in analogy to an [[initial algebra]]). Theories with a non-empty set of equations are known as [[equational theory|equational theories]]. The [[decision problemsatisfiability]] problem for free theories is a [[satisfiability]] problem, and is solved by [[syntactic unification]].; Italgorithms isfor particularlythe important,latter asare manyused otherby theories can be reduced to it. Interpretersinterpreters for various computer languages, such as [[Prolog]],. requireSyntactic unification is also used in algorithms for solving the freesatisfiability theoryproblem 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 [[Satisfiability modulo theories|SMT solver]]:

<syntaxhighlight lang="text" line="1">

An [[array data structure|array]] can be specified by the following equational [[axiom]]:<ref group=note>Here, ''select''(''a'',''i'') informally designates the value of the ''i''th element of ''a'', written e.g. in [[C (programming language)|C]] as <code lang="C">a[i]</code>, while ''store''(''a'',''i'',''v'') informally designates the array resulting from writing the value ''v'' to the ''i''th element of ''a'', written in C as <code lang="C">a[i]=v</code>.

(declare-fun f (Int) Int)

The axiom then informally means that the value obtained by <code lang="C">a[i]=v;return a[j];</code> equals <code lang="C">v</code> if <code lang="C">i</code>=<code lang="C">j</code>, and <code lang="C">a[j]</code>, else.</ref>

(assert (= (f 10) 1))

</syntaxhighlight>

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

the SMT solver would return "This input is satisfiable". That happens because <code>f</code> is an uninterpreted function (i.e., all that is known about <code>f</code> is its [[Signature (logic)|signature]]), so it is possible that <code>f(10) = 1</code>. But by applying the input below:

<syntaxhighlight lang="text" line="1">

This axiom can be used to deduce

(declare-fun f (Int) Int)

(assert (= (f 10) 1))

: ''select''(''store''(''store''(''a'',1,−1),2,−2),1)

(assert (= (f 10) 42))

:: = ''select''(''store''(''a'',1,−1),1)

</syntaxhighlight>

:: = −1

the SMT solver would return "This input is unsatisfiable". That happens because <code>f</code>, being a function, can never return different values for the same input.

Note that this reasoning did '''not''' use any 'definition' or [[interpretation (logic)|interpretation]] for the functions ''select'' and ''store''. All that is known is the axiom.

==Discussion==

The [[decision problem]] for free theories is particularly important, asbecause many theories can be reduced toby it;.<ref>{{cite thebook above|last1=de exampleMoura is|first1=Leonardo the|last2=Bjørner prototypical|first2=Nikolaj example|title=Formal ofmethods the: theoryfoundations ofand [[arrayapplications data: structure|arrays]],12th whereBrazilian 'select'Symposium andon 'store'Formal areMethods, theSBMF canonical2009, arrayGramado, accessBrazil, functions.<ref>J.August McCarthy19-21, (1962)2009 "Towards: arevised mathematicalselected sciencepapers of|date=2009 computation."|publisher=Springer '''IFIP|___location=Berlin Congress.''',|isbn=978-3-642-10452-7 pp|url=https://leodemoura. 21–28github.io/files/sbmf09.pdf}}</ref>

Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]].{{clarify|reason=Indicate about solving which problem in free theories the sentence is supposed to speak. E.g. to solve the satisfiability problem of conjunctions of equations, the Martelli-Montanari syntactic unification algorithm suffices, neither common subexpressions nor congruence closures are needed. Maybe, satisfiability of arbitrary Boolean combinations of equations is meant?|date=May 2014}} Solvers include [[satisfiability modulo theories]] solvers.

== See also ==

* [[algebraicAlgebraic data type]]

* [[initialInitial algebra]]

* [[termTerm algebra]]

* [[Theory of pure equality]]

==Notes==

{{reflist |group=note}}

==References==

{{Reflist}}

{{reflist group=note}}

[[Category:Specification languages]]

{{reflist}}

{{Mathematical logic}}

{{Formalmethods-stub}}

[[Category:Specification languages]]