Anticipating the future

I believe that I have finally knocked out this progress lemma, which was (appropriately enough) holding back progress on my thesis proposal. I will have to see for sure tomorrow. The difficulty is not in proving the progress theorem itself; the problem is in making the progress theorem anticipates the future appropriately.

Anticipating the future is impossible in general, but it is also one way to explain a major point of my thesis proposal. What do I mean when I say I want to anticipate the future? Consider the following rules describing a little programming language with addition:

 -------
 n value

 (σ, e₁) ↦ (σ', e₁')
 -----------------------------
 (σ, e₁ + e₂) ↦ (σ', e₁' + e₂)

 e₁ value
 (σ, e₂) ↦ (σ', e₂')
 -----------------------------
 (σ, e₁ + e₂) ↦ (σ', e₁' + e₂)

 n₁ + n₂ ⇓ n₃
 -----------------------------
 (σ, n₁ + n₂) ↦ (σ, n₃)

Depending on your background, you may be thinking what the hell is that or perhaps why did he add the σ things everywhere. Or perhaps you saw where I was going immediately, and thought "oh, Rob intends to extend this specification with some sort of imperative, mutable state at some point in the future." Which is really the point: this specification has some ugliness to it (the currently-unnecessary σ annotations) so that it can anticipate the future addition of a feature, namely state. If I wanted to anticipate parallel evaluation, on the other hand, or maybe exception handling, I would have to make additional choices now.

But without knowing (or guessing) that I want to add mutable references, the σ annotations seem awfully unmotivated. If one tried to write an Structural Operational Semantics specification for a simple thing like the addition of numbers that anticipated the addition of features like state, parallel evaluation, and exception handling, there would be a lot of unmotivated stuff hanging around dirtying up the specification. So the question becomes: is it possible to anticipate these future additions without making it utterly painfully obvious that we're anticipating these future additions? Several groups of people, at least three or four by my count, have answered "yes!" to this question, and they've answered them in different ways. I will talk about them, and about the particular answer I am exploring, in a future post (if I anticipate the future correctly!)

In the meantime, I'm trying to also make sure that the proofs of basic safety properties (such as progress and preservation lemmas) can be written to anticipate the future inclusion of language features dealing with state, parallel evaluation, and exception handling. I am increasingly confident that this will work, but then again, I can't see the future ;-).