How to learn to do determinism proofs

A couple days ago, my advisor asked me what reading material I would suggest to a new student who wants to learn to do determinism proofs like the ones we did for LVar calculi. This is a good question! Even assuming that one knows what one means by “determinism”, I think it’s hard to come by good introductory examples of determinism proofs. If you want to know (or refresh your memory on) how, say, a standard progress-and-preservation type safety proof is set up, you can flip to chapter 8 of TAPL. But I don’t know of a similar standard resource for how a proof of determinism is set up.

I can tell you how I went about it, though. To learn what a determinism proof is shaped like, I think that the one for Featherweight CnC in the Concurrent Collections paper is a good place to start. You can skip past the stuff in the paper about the CnC programming model and go straight to the Featherweight CnC calculus. The paper doesn’t spell out every little detail of the proof, but it does actually give the statement of every lemma that the proof uses, which I think is a big help. And Featherweight CnC is a tiny calculus, but not so tiny that determinism is trivial. So it’s a good place to start.

It helps to draw pictures while reading the proof, especially to make sense of the Diamond, Strong Local Confluence, Strong One-Sided Confluence, and Strong Confluence properties. It was by studying this proof — along with the discussion of Church-Rosser for ISWIM in chapter 4 of the PLT Redex book — that we first figured out how to show determinism for the lambdaLVar language. In fact, the proofs of Strong One-Sided Confluence and Strong Confluence are almost the same for the lambdaLVar calculus as they are for Featherweight CnC.

After the Featherweight CnC proof, if you want to know how that way of writing a determinism proof applies in the setting of LVars, I suggest turning to chapter 2 of my dissertation and looking at the determinism proof for lambdaLVar. Although the gory details of the proof are rather different in the setting of LVars, the structure of the proof is a lot like the one for Featherweight CnC. I would recommend reading the version in my dissertation instead of the version in the LVars FHPC ‘13 paper and companion TR, because the paper and TR used an older formulation of lambdaLVar that made things needlessly complicated.

Chapter 3 of my dissertation shows a similar proof for the lambdaLVish language, which throws several new language features into the mix. This time, the language is merely quasi-deterministic (every run of a lambdaLVish program that produces an answer will produce the same answer, but a run could also end in an error), and not deterministic. But the structure of the quasi-determinism proof for lambdaLVish is basically the same as the determinism proof for lambdaLVar.

One thing to keep in mind about all these (quasi-)determinism proofs, though, is that they are very “operational” — they deal with individual computation steps in a manual and tedious way. There’s probably a better way. Furthermore, they are all dealing with untyped languages. If you had a type system designed to ensure determinism, proving determinism would be a matter of showing that the type system rules out programs that would have behaved nondeterministically at runtime. With LVars, ensuring deterministic behavior isn’t a matter of ruling out badly-behaved programs (although I like that approach, too), or of stopping things from happening in the wrong order; it is a matter of allowing things to happen in arbitrary order, and then preventing any resulting nondeterminism from being observed.

If you have any recommended resources on how to learn to do determinism proofs, I’d love to hear about them!