Uninterpreted function: Difference between revisions

Revision as of 16:12, 13 June 2011

Revision as of 10:30, 9 May 2012

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|author1=Franz Baader|author2=Tobias Nipkow|title=Term Rewriting and All That|year=1999|publisher=Cambridge University Press|isbn=9780521779203978-0-521-77920-3|pages=34}}</ref> is one that has no other property than its name and arity. 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 problem]] for free theories is a [[satisfiability]] problem, and is solved by [[syntactic unification]]. It is particularly important, as many other theories can be reduced to it. Interpreters for various computer languages, such as [[Prolog]], require algorithms for solving the free theory.

Line 19:

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, 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>J. McCarthy, (1962) "Towards a mathematical science of computation." '''IFIP Congress.''', pp. 21–28</ref>.