5 ms·
That's because you can consider categories of preorders and formulas where these operators will be morphisms. (b >= c) && (a >= b) -> (a >= c) is a composition
by gettingoverit 1y ago
That's because you can consider categories of preorders and formulas where these operators will be morphisms.
(b >= c) && (a >= b) -> (a >= c) is a composition.
The more interesting consequence is that function types and implications are different names for the same thing. This is a Curry-Howard-Lambek correspondence.
This means that in order to prove
(b -> c) -> (a -> b) -> (a -> c)
it's enough to implement a function
f g h x = g (h x)
Another consequence is that exponentiation a^b can be considered the same thing as b -> a.
a^(bc) = (a^b)^c
(b && c) -> a = c -> b -> a
- spyrja 1y agoAnother consequence is that exponentiation a^b can be considered the same thing as b -> a. In the case where a and b are not strictly boolean (supposing they are instead probabilities for example) you could even generalize it somewhat in terms of "pure" mathematical operations. double implies(double a, double b) { double dif = a - b; double abx = sqrt(dif * dif); return 1 + pow(0, abx - dif) - pow(1, abx + dif); } Kind of silly, I know, but it does work.
- gettingoverit 1y agoNice to know! I thought about it in terms of cardinalities of types. If A and B are types with |A| and |B| values correspondingly, there are |B|^|A| possible functions A -> B. Another funny thing is that if you consider forall a. (a -> a) -> (a -> a) the type of natural numbers (weird, I know, but basically we encode numbers in unary with number of times we compose (a -> a) to itself), then exponentiation on such numbers will be a ^ b = b a