8 Dec
2008
8 Dec
'08
6:10 p.m.
2008/12/8 Joachim Breitner
So A^(B+C) = A^B × A^C ?
That's part of the basis for Hinze's paper on memoization: http://www.informatik.uni-bonn.de/~ralf/publications/WGP00b.ps.gz
It's always nice to see that I havn't learned the elementary power calculation rules for nothing :-)
More generally, all of Tarski's "high school algebra" axioms carry over to types. You can see the axioms here: http://math.bu.edu/people/kayeats/papers/saga_paper4.ps That proves type theory is child's play :-) -- Dan