6 ms·
Can someone please explain what is an "uninterpreted function", in the context of Ante's refinement types? The Wikipedia article didn't help much (https://en.wi
by VladimirGolovin 4y ago
Can someone please explain what is an "uninterpreted function", in the context of Ante's refinement types? The Wikipedia article didn't help much (https://en.wikipedia.org/wiki/Uninterpreted_function https://en.wikipedia.org/wiki/Uninterpreted_function).
- jfecher 4y agoHi! An uninterpreted function is one where the only thing we can assume about it is that `(x = y) => (f x = f y)`. That is if we give it the same input, we should get the same result out. In the context of refinement types this can be used for, among other things, tagging values with some predicate. For example, if we know `good_index array 3` and `x = 3` then we know `good_index array x`.