From Seo Wiki - Search Engine Optimization and Programming Languages
|The introduction to this article provides insufficient context for those unfamiliar with the subject. Please help improve the article with a good introductory style. (October 2009)|
An uninterpreted function is one that has no other property than its name and arity. They are often used together with equality in formal reasoning, especially using computers.
An array can be specified the following axiom:
- select(store(a,i,v),j)=(if i=j then v else select(a,j))
This axiom can be used to deduce
- = select(store(a,1,-1))
- = -1
Note that this reasoning did not use any 'definition' for the functions select and store. All that is known is the axiom.
- ↑ 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–122.