### (no subject)

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

so $t = i$, and therefore we should expect $t = t^5$. And in fact there is an "elementary" isomorphism between

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.

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

`BUTree`s 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.