When I vis­ited Cal­gary last, I explained my bounds infer­ence scheme to Brian. It took most of an entire day of solid explan­a­tions on the white­board before he under­stood what I was talk­ing about, but he didn’t have any sug­ges­tions for how to sim­plify it. “No this is right,” he said. “This is com­pletely the right way to do it.”

Some time later he said “my biggest worry is you’re going to do all this work and no one will ever be able to under­stand it.” Aside from myself, Brian is the per­son who under­stands this best in the world, so it’s dis­con­cert­ing that it took a day to explain it to him. I have low hopes that I’ll be able to put together a thesis which is under­stand­able to my com­mit­tee, but on the other hand I have high con­fid­ence in my teach­ing abil­it­ies, and what is writ­ing a thesis if not non-​​verbal teaching?

Pola is com­plex. The syn­tax and semantics are rather arcane, neces­sar­ily so: if there were any way to sim­plify it we would, and in fact we did put a few sim­pli­fic­a­tions in. The typ­ing sys­tem is mod­er­ately if you are well versed in type the­ory; if you don’t have a strong back­ground in type the­ory I can only ima­gine it appears as a tangled vine of thorny bushes, where each thorn is recurs­ively a tangled vine of thorny bushes some­how. The bounds infer­ence sys­tem is prob­ably even worse, though only because it hasn’t been done before and I’ve had to con­jure it from the ground up. I feel most con­fid­ent about the bounds infer­ence because it’s my biggest con­tri­bu­tion but also because it’ll be the easi­est to make self-​​contained and not have to worry about whatever nota­tion is con­ven­tional or canonical.

There are mul­tiple ver­sions of Pola, vari­ations I sup­pose, which I keep mostly in my head. My thesis is focused on the “polynomial-​​time with unfolds and with duplic­a­tion by peeks” vari­ant of Pola, which I think to be the most use­ful, though prob­ably the most annoy­ing to deal with. Most of the stuff I’ve writ­ten up I’m now rewrit­ing in a new nota­tion which will hope­fully be easier to understand.

A couple weeks ago my friend Angela came to my office and we chat­ted about theses. I don’t know whether to describe the pro­cess of writ­ing a thesis as van­ity or futil­ity. Maybe it’s just com­pul­sion. Whatever it is, it doesn’t seem totally sensical to con­sume so much effort and one’s twind­ling men­tal health into it. “Remem­ber: nobody cares” she said. It’s become a bit of a man­tra for me. Even if my work goes com­pletely for­got­ten and truly no one cares, I can’t help but pre­tend that people do any­way and do everything prop­erly. Every week I spend at least a couple pan­icked hours tying up loose ends that I’m entirely con­vinced no one would ever notice were loose to begin with. This dili­gence includes put­ting most of my days into dream­ing up ways to rep­res­ent things to make them easier to under­stand, even if no one fully will.

The fur­ther I get the more I notice the hacker part of me try­ing to over­take the aca­demic part of me. It’s tempt­ing to just strike out my entire chapter 3 and say “yeah ser­i­ously just down­load the soft­ware and play with it. You will learn more in 5 minutes of play­ing around than you will reread­ing this stu­pid chapter a hun­dred times”.

Man this entry soun­ded depress­ing. It’s all worth it when you do fin­ish a sec­tion, though. You do get a bit of a rush when you finally word some­thing really eleg­antly and you can visu­al­ize your com­mit­tee nod­ding along think­ing “well that’s clear. Why did put so much emphasis on some­thing that’s so simple?”

When I visited Calgary last, I explained my bounds inference scheme to Brian. It took most of an entire day of solid explanations on the whiteboard before he understood what I was talking about, but he didn't have any suggestions for how to simplify it. "No this is right," he said. "This is completely ...

Jasna and I just got back today from a spur-​​of-​​the-​​moment camp­ing trip. We’d been want­ing to have a couple days just for the two of us for a while now, and our sched­ules aligned, so why not? We thought camp­ing would be more fun and relax­ing than any­thing else, and I’ve wanted to see the towns along the Grand River forever, so we com­bined the two and went to Rock Point Pro­vin­cial Park: it’s vir­tu­ally right where the Grand River emp­ties into Lake Erie and neces­sit­ates driv­ing along the Grand River, a fairly nice drive.

I’ve got a grand total of 3 pic­tures from the trip and I’m happy with that. It wasn’t the sort of trip to you take to take pic­tures of. Appar­ently the park is known for its fossils, but we didn’t go hunt­ing for those, either. We went down to the beach a few times — twice for moon­light swims — and spent most of the rest of our time in our camp­site sit­ting around and talk­ing and enjoy­ing one another. We got a nice camp­site with fairly good pri­vacy and shade, and none of the camp­sites dir­ectly around us were taken. It was pretty much the per­fect couple of days, only because we were together.

Jasna bought me an e-​​reader! She actu­ally bought it before we’d planned on going on the trip, but I guess this seemed a good time to give it to me, and give me an easier time read­ing. It’s a Kobo, which I adore. I’m actu­ally a bit of a freak in that I’m some­what anti-​​paper: I often prefer read­ing on screen to read­ing on paper; maybe it’s a side-​​effect of grow­ing up with a com­puter. The Kobo has a really beau­ti­ful dis­play and is easier for me to read than any­thing I’ve ever read from, CRT, LCD or paper. The dis­play can’t refresh very often — maybe once a second or some­thing like that — and it’s super low-​​powered which makes it unsuit­able for any­thing but read­ing, which suits me fine. I have only two com­plaints: firstly, that the font size is typ­ic­ally too big, but that’s a cri­ti­cism of the books that are format­ted for it, not the device itself; and secondly, that it’s really dif­fi­cult to skip for­ward or back­ward a lot of pages at a time. With paper it’s easy to do a bin­ary search for the page you want, but the Kobo seems determ­ined to make you do a lin­ear search.

I did bring my laptop, but only so I could do just enough work to make my guilt levels fall to the point where I could genu­inely relax. It turns out that’s about half an hour, ha! I’m still more or less pleased with how the thesis is progressing.

Jasna and I just got back today from a spur-of-the-moment camping trip. We'd been wanting to have a couple days just for the two of us for a while now, and our schedules aligned, so why not? We thought camping would be more fun and relaxing than anything else, and I've wanted to see ...

Check out the pic­ture gal­lery. Even though it was all cat­egory the­ory, and con­sequently I can fol­low almost none of the other talks, it’s still a won­der­ful con­fer­ence to go to. It’s a nice atmo­sphere, a good mix­ture of grad stu­dents, pro­fess­ors and pro­fess­ors emeriti.

After the con­fer­ence I stayed in Cal­gary for another couple weeks work­ing on my thesis and going through bounds infer­ence in detail with Brian. Unfor­tu­nately, and excit­ingly, we found a big prob­lem with the mix­ture of coin­duct­ive and induct­ive recur­sion which can take one out of poly­no­mial time. I may write on that more at some other time, but only after I think of a good way to describe it, at which point the first place it will appear is my thesis.

Check out the picture gallery. Even though it was all category theory, and consequently I can follow almost none of the other talks, it's still a wonderful conference to go to. It's a nice atmosphere, a good mixture of grad students, professors and professors emeriti. After the conference I stayed in Calgary for another couple ...