Uninterpreted function: Difference between revisions

Revision as of 12:49, 4 December 2019

Revision as of 20:26, 7 December 2019

Line 1:

{{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}}</ref> or '''function symbol'''<ref>{{cite book |last1=Baader |first1=Franz |authorlink1=Franz Baader |last2=Nipkow |first2=Tobias |authorlink2=Tobias Nipkow |year=1999 |title=Term Rewriting and All That |publisher=Cambridge University Press |isbn=978-0-521-77920-3 |page=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]].