There are a lot of things that I could talk about (there are already four post-its on my monitor reminding me of this fact), so I’m going to be bouncing around quite a bit. I want to talk about grad school now, though, and air out some of my thoughts on the research I am doing/plan to do.
I’m taking three courses this semester. Two of them look like they’re going to consist of a lot of review (or at least looking at old concepts in new ways), but I’m also taking a linguistics course. It’s on formal semantics, so of course it’s related to the broad area of math/CS/logic/etc. that I’m interested in, but I think it’s going to be very helpful for getting me to think about things in the right way.
What do I mean by “the right way”? First off, I don’t mean objectively the right way; I mean the right way for my own style/interests. If I may paraphrase something that Bob Harper said when talking about the connections between programming languages, logic, and category theory: if you discover the same concepts arising independently in three different areas of study, it’s clear that you have hit upon a fundamental fact of the way humans reason.
My own butcherings and/or misinterpretations of things Bob said aside, I think this is an excellent thing to keep in mind when approaching research in any of these areas, for a few reasons. First, and most obviously, when you are studying something in one of those areas, think about the connections you can make to the others. Now, my category theory is still not really up to par, but the Curry-Howard correspondence (which is the coolest thing ever and the reason I’m in grad school right now) is an excellent example of a methodology. Thinking about logic? Consider how it would impact a programming language. Thinking about a programming language? Think: does it feel like something you could describe as a logic?
This has been done for a while, and even taught in a few undergrad courses that I’ve taken, but I think the other reason is a bit less emphasized, or maybe even a bit less teachable. If the connections between these things happened because they are fundamental to how humans reason, then what other, unexplored methods of human reason have applications in these areas? This, I think, is the area that I am really interested in, but I don’t think I’ve done a good job of making my meaning clear, so here are a few examples.
A while ago (as my livejournal friends know), I talked about a “logic of obligation”, as I’ve taken to calling it. It started when I was trying to formalize (in my mind, at least) what we mean when we say “X should do Y”. I think I’ve got a decent account of it now, though it’s been a while since I’ve thought about it; I should probably actually write something up about it at some point. But the point is that it came about when I took something I said quite often—”X should do Y”—and tried to think about it in a precise, formal manner.
Another example: a couple of weeks ago, I started working with some folks here on a (new, better) programming language for interactive fiction. The guy who approached me about it has actually been talking to Zarf, who is not entirely satisfied with the current state of IF languages. There are slides from a talk he gave on the topic, but the main idea was that he was thinking about things as rules, and exceptions to rules. As it turns out, there’s a logic for that (logics are kind of like apps!) called “defeasible logic” whose purpose is to deal with rules that may have exceptions. From what I can tell, defeasible logic hasn’t been studied very in-depth, which is something I would really like to fix. And again, it exactly matches the way Zarf thinks: “A, unless B, unless C, unless D, unless…”. Rules, and exceptions, and exceptions to exceptions, and so on. This doesn’t come out of nowhere, or from some contrived problem that someone came up with after being crammed in their office with no sunlight for a few weeks. This is the way we think, rigorously defined and closely examined.
Which brings us back to semantics. What better way is there to study the way we reason than to study the way we communicate? I already think about what the things we say really mean and ways to think about them formally; why not take a class on it? I’m sure my ideas about what a semantician does are a little naive, but regardless of how far off-base I am, I still think I will get some valuable insight into how to think about these kinds of problems.
I guess my point here is that cool stuff happens when you combine math and CS, and even more cool stuff happens when you take that combined approach and apply it to anything that looks like it should be formalized and understood. I have more to say about formalizing things (spoiler alert: I think it’s good!) and making them precise (even better!), but that’s now a fifth post-it on my monitor. That will probably be more of a legit blog; this was more of a rambly attempt to get some of my thoughts down. I hope I didn’t lose anyone along the way!