Uninterpreted function: Difference between revisions

Revision as of 09:58, 15 August 2016

Revision as of 10:01, 15 August 2016

Line 1:

{{Context|date=October 2009}}

In [[mathematical logic]], an '''uninterpreted function'''<ref>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&ndash;122.</ref> or '''function symbol'''<ref>{{cite book |author1lat1=Baader |first1=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|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 [[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 (computer science)|Narrowing]].

==Example==

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>.

The axiom then informally means that the value obtained by the statements <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>

Line 21 ⟶ 20:

==Discussion==

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 [[array data structure|arrays]], where 'select' and 'store' are the canonical array access functions.<ref>{{cite book |last=McCarthy author|first=John McCarthy|year=1962 |title=IFIP Congress |chapter=Towards a Mathematical Science of Computation| title=IFIP Congress| year=1962| pages=21–28| publisher=North-Holland | url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.79.8613 |pages=21–28}}</ref>{{citation needed|reason=The given reference neither mentions 'array', nor 'store', nor 'select'. Apparently it doesn't handle the example.|date=May 2014}}

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.