Uninterpreted function

From Seo Wiki - Search Engine Optimization and Programming Languages

An uninterpreted function^[1] 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.

[edit] Example

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(store(a,1,-1),2,-2),1)

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

[edit] See also

• algebraic data type
• initial algebra

[edit] References