What do you think?
Rate this book
Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory
First book-length exposition of the denotational (or 'mathematical' or 'functional') approach to the formal semantics of programming languages (in contrast to 'operational' and 'axiomatic' approaches). Treats various kinds of languages, beginning with the pure-lambda-calculus and progressing through languages with states, commands, jumps, and assignments. This somewhat discursive account is a valuable compilation of results not otherwise available in a single source. --American Mathematical Monthly
450 pages, Paperback
First published March 1, 1978
4 people are currently reading
57 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 2 of 2 reviews
November 6, 2023
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.
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.
July 5, 2019
I feel these results though the foundations are quite fundamental have a certain obviousness to them- at least as presented. Perhaps this work given it's age does contain all the implications of the results as we know them today. I am unsure.
Displaying 1 - 2 of 2 reviews