Jason (jcreed) wrote,

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.
Tags: categories, math
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded