Uninterpreted function
From Seo Wiki - Search Engine Optimization and Programming Languages
Jump to navigationJump to search
{{Expansion depth limit exceeded| left =
| #default = }}
{{Expansion depth limit exceeded| {{{Expansion depth limit exceeded}}}
| [[File:{{Expansion depth limit exceeded| speedy = Ambox speedy deletion.png
| delete = Ambox deletion.png
| content = Ambox content.png
| style = Edit-clear.svg
| move = Ambox move.png
| protection = Ambox protection.png
| notice
| #default = Ambox notice.png
}} | {{Expansion depth limit exceeded| left = 20x20px
| #default = 40x40px
}} |link=|alt=]]
}}{{Expansion depth limit exceeded| left =
| #default = |
{{{Expansion depth limit exceeded}}} |
[[Category:{{Expansion depth limit exceeded|{{{Expansion depth limit exceeded}}}|{{{Expansion depth limit exceeded}}}}}]][[Category:{{Expansion depth limit exceeded|{{{Expansion depth limit exceeded}}}|{{{Expansion depth limit exceeded}}}}}]]
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.
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.
See also
References
- ↑ 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.
If you like SEOmastering Site, you can support it by - BTC: bc1qppjcl3c2cyjazy6lepmrv3fh6ke9mxs7zpfky0 , TRC20 and more...
→
