19 Mar 2020
I recently took a crack at Thomas Streicher’s Domain-Theoretic Foundations of Functional Programming. I can’t remember how I happened on it, but it seemed to nicely follow my foray into formal methods from last winter. On this first pass, I got through about three and a half chapters (if I’m being generous) before everything started flying over my head, so I’ve tried to capture what I did get below. (Any domain theorists out there, please forgive my grossly oversimplified model of the field.)
Domain theory is a tool for analyzing programs. The chapters of the book I read studied the relationship between the purported behavior of a program — its operational semantics — and the program’s meaning — its denotational semantics.
An observational semantics (this seemingly strange plural/ singular situation is how it appears in the literature, don’t ask me) describes the relationship between terms or expressions formed from the syntax of a language and the values to which they evaluate. There are two ways to describe that relation: big step semantics, and small step semantics. A big step semantics is (or seems to me to be) a relation in the traditional set-theoretic sense which pairs expressions with values. A small step semantics defines a relation between pairs of terms (rather than terms with values) where one reduces to the other through one application of a reduction (e.g. beta), as governed by the language’s typing rules. You might think of an interpreter as a machine which successively applies the small step semantics to evaluate a term to some value.
One of the major advantages of considering all this, which might on the surface seem to be vapid ceremony on top of an already perfectly usable programming language, is that it gives a mathematical foundation for testing. When you have a continuous integration server run tests on your code, and don’t allow merging until the tests pass, you’re really using unit tests as a means to compare programs, namely, the program as it was before your diff, and the “new” program with your diff applied. If the new program passes the tests, then we’re satisfied that it’s sufficiently equivalent to the old program. That is, if we observe that the new program evaluates to the same values as the old, we’re satisfied it’s equivalent enough on the axes we haven’t meant to change. An operational semantics gives rise to a formal notion of observational equality between two programs. For programs P and Q, if, for all contexts C, P and Q, evaluated within C, yield the same value, then they are observationally equivalent. This would give us a rigorous formal foundation for constructing correctness proofs from things like unit tests, but “context” can be a fuzzy thing, and quantifying over the universe of possible contexts is a fool’s errand.
This is one motivation for establishing a denotational semantics for your program. A denotational semantics assigns every expression some element from the semantic domain of the expression’s type. We call that particular element the expression’s “meaning,” “semantics,” or “denotation.” Domain theory studies what structures are useful to impose on that domain, for the purpose of discovering and proving properties of the programs that domain describes.
The first chapter introduces methods of equating a denotational semantics with an operational semantics, in increasing order of strength. My take away was that the stronger the equivalence between the two semantics, the more things you can prove about the operations by working with the denotations (which is desirable because in denotation land, you can work with well studied algebraic objects, and don’t run into the context quantification problem).
That’s about all I got for you on this run. I hope to find some lower level material (recommendations welcome!) and revisit this text at a later point. What I did get through made the application of denotational semantics much more concrete within my personal mental model, so I’m excited to unlock the insights from the remaining chapters.
Previous post: Coffee Log 32