October 8th, 2008

beartato phd

(no subject)

Sat in on Bob Harper's class today after being told I might like it several times by various people. There was a lot of routine category theory, but he made me appreciate that there really is "primitive corecursion" dual to ordinary primitive recursion and which is no scarier and no more "nonterminating". Also he claimed that a heuristic reason Set can't model general recursive domain equations is that it has too many equalizers; the "trailer" for next class was that we can somehow code up a weak initial algebra for the (covariant!) functor X |-> 2^(2^X) in system F, and if we could get that into Set, then we could use equalizers to cut it down to a real initial algebra.