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.
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic