I'm still climbing the Twelf learning curve.
Learned in painful ways the difference between the %total and %terminates assertions, and now I know when to use one and not the other. Basically, %terminates is for hypothetical judgments, and %total is for meta-theorems. I don't know how I didn't get this before, but I now understand that you use %terminates when you need to prove that the acceptable inputs produce the required outputs, and that you use %total when you need to prove that all the possible inputs produce the required outputs.
So, that's all good. I've been struggling to figure out how to prove sort-preservation in the sorted polyadic π-calculus, and that isn't working. I keep going back to the monadic version and painting myself into a corner. I suspect some of the informative text in Chapter 9 of Milner's book warns against trying to do the thing I've been failing to do. I should have listened. It's never a good idea to second-guess Robin Milner. (And, I haven't even been meaning to... it's just that I keep analyzing my failures and finding out that Milner told me fifteen years ago not to do it that way.)
Anyway, as if that wasn't enough to make my head collapse from the strain, I've now discovered the
D-Fusion Calculus— a variant of the polyadic π-calculus with two binding operators instead of one and a symmetry between input and output. Just when I thought I had all the weird math in Milner's book figured out, I've got
yet another collection of evil Eurozone hippies hammering on my tender lobes. I am fcking doomed.
Gina is struggling her way through the undergraduate physics for earth sciences majors, and she says it's kicking her ass. I tutored physics and calculus a lot when I was in college (it was my work-study program), so I have some idea how badly she's getting pasted by it. She's working hard, but things are coming together slowly for her. I have seen people work a lot harder for worse results, but they usually fail out. She might scrape out a passing grade, but she needs encouragement that she really can do the math. She can. I've seen her do it. But she makes mistakes and gets frustrated too easily. I can almost see the wheels in her brain start grinding when she loses the plot in a homework problem: it's not just that she can't see how to do the problem; it's that she's convincing herself that she's not smart enough to see it. That's her biggest challenge, I think. I'm afraid she might drop out before she hits her stride. She's working hard, and she's learning it. She's never going to be a quantum physicist, but she can probably pass the physics class for earth sciences majors if she just keeps up her current level of effort through to the end of the semester.
She has her first big mid-term quiz today. I hope she manages to scrape out a passing grade. If she fails it, I'm going to have a lot harder time encouraging her to stick with it. I don't think the Wilbur Robinson "Keep Moving Forward" pep-talk of the century is going to work very well.
Anyway, I say all this because I'm pretty sure I know exactly how Gina feels right now. All this programming language theory I've been learning lately is scary complicated, and I'm pretty sure if I was learning it in a classroom setting, I'd fail out pretty hard. I often wonder if the reason it seems to come so slowly to me is that I'm just not smart enough to learn it sufficiently well that I can trust my intuitions with it. You can't really call yourself a scientist until you can get new results added to the literature. I'm a long way off from that: I can barely read the literature, much less have any hope of writing a paper that would be readable.
So my head hurts. A lot.
Comments