Jason (jcreed) wrote,

Meeting with Frank went pretty well. I have another batch of papers to read and some more ideas to think about.

Skipped Type Systems to go to the POP seminar. It was a really slick talk, titled "Imaginary Types". The joke is, suppose I have datatype BUTree = nil | Binary of BUTree * BUTree | Unary of BUTree. This is a solution of the type equation $t = 1 + t * t + t$. Subtracting $t + 1$ from both sides, (hah!) $t^2 = -1$
so $t = i$, and therefore we should expect $t = t^5$. And in fact there is an "elementary" isomorphism between BUTrees and pentuples of them. (of course there is an isomorphism in the sense that both sets are countable, but what holds further is that there is an isomorphism which looks down to only a constant number of levels of the tree)

This is all based on generalizing Andreas Blass's paper Seven Trees in One in which the usual type binary trees is shown to be a primitive sixth root of unity, sort of.

Later got some complexity theory homework done. This week's assignment is pretty tough. I'm cutting a lot of corners in my proofs because the details are somewhat ugly.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded