blergity blerg mcBlerg-Blerg

[tiedyedave]

Unnnh. It's five in the morning. I just finished my homework for PL. It looks ok now, but I have insufficient confidence in my proof techniques, and I feel like a tool for my incomplete understanding of rule induction and derivation induction. And why does the Winskel text not even mention glorious, glorious inversion even though Pfenning used it all the time?

I sleep now. More work tomorrow. I was hoping my life as a grad student would start on a slightly firmer footing than this. que sera sera.

Comments

[adamch.livejournal.com]

Inversion is easy to prove from rule induction; it's a degenerate case.

[tiedyedave]

I know that now, and I think I knew it all along, but it took me an hour or two to convince myself of it.