Denotational Semantics

An excellent book, which brings forth visions of futures that never were. Written in the late 70s, this book takes denotational semantics seriously, and harps on the difficulties which arise from the operational and axiomatic approaches—both of which, unfortunately, are much more popular now than their denotational counterpart.

There's a lot going on here. Some of it is delightful historical notes about computing, like early computers which drew their text backwards, to which the solution was to mirror everything, and then put a physical window in the back of the computer for the nerds to read their (now reversed) waveforms through. Or about how dynamic scoping, in all its awfulness, was brought about because it has an easy and obvious implementation when you're writing an interpreter.

But where the book really shines is in all the MATH. Oh my god. Stoy gives us structural inductive arguments (yay!) and contrasts them against induction on the runtime (which can only ever be shown to have not yet gone wrong, but never to have actually produced the right answer.) I finally got a meaningful answer to what exactly a least-fixed point is (one function is “less” than another if it is defined on fewer inputs, thus the least fixed point is the one that is bottom in as many places as possible.)

Furthermore, there's a great deal of cool representation stuff going on. Stoy points out that we have never actually seen a function, only ever representations (closed form algorithms) of them. It's obvious when it's pointed out, but I'd never thought of the lambda calculus as a REPRESENTATION OF FUNCTIONS before. The book constructs a semantics of the lambda calculus and shows why exactly it models functions, with the entire thing being built out of lattices, with theory that I suspect is where propagators also came from.

Denotational Semantics, the book, and sadly, the ideas in it, is rather dated at this point. But that's a huge amount of the charm. Our field has gone the wrong direction and it can be hard to see the context we exist in. Highly recommended.