Total Denotational Semantics (blog)
Total Denotational Semantics (blog)
Background: What are denotational semantics, and what are they useful for?
Also: Operational and Denotational Semantics
Denotational semantics assign meaning to a program (e.g. in untyped lambda calculus) by mapping the program into a self-contained domain model in some meta language (e.g. Scott domains). Traditionally, what is complicated about denotational semantics is not so much the function that defines them; rather it is to find a sound mathematical definition of the semantic domain, and a general methodology of doing so that scales to recursive types and hence general recursion, global mutable state, exceptions and concurrency12.
In this post, I discuss a related issue: I argue that traditional Scott/Strachey denotational semantics are partial (in a precise sense), which means that
- It is impossible to give a faithful, executable encoding of such a semantics in a programming language, and
- Internal details of the semantic domain inhibit high-level, equational reasonining about programs
After exemplifying the problem, I will discuss total denotational semantics as a viable alternative, and how to define one using guarded recursion.
I do not claim that any of these considerations are novel or indisputable, but I hope that they are helpful to some people who
- know how to read Haskell
- like playing around with operational semantics and definitional interpreters
- wonder how denotational semantics can be executed in a programming language
- want to get excited about guarded recursion.
I hope that this topic becomes more accessible to people with this background due to a focus on computation.
I also hope that this post finds its way to a few semanticists who might provide a useful angle or have answers to the conjectures in the later parts of this post.
If you are in a rush and just want to see how a total denotational semantics can be defined in Agda, have a look at this gist.
I thought I might learn something new about programming, instead I just learnt I'm not smart enough to understand this. :-(
You probably are. It's just an extremely specific domain and terminatory, and you are missing several underlying concepts required to understand it. It's literally a different language and you haven't learned the vocabulary; it looks like English, but the words have specific meanings in the context.
Not that it isn't complex, but I think it's a mistake to think that, just because you haven't learned Greek, that you're not smart enough to understand it. You're simply undereducated in the domain.
Yeah this sort of stuff reads a lot like philosophy nonsense babble to me. I think maybe it isn't nonsense like the philosophy stuff but it sure would be nice if they gave a few concrete examples to demonstrate that.
The
Backgroundlink does make sense... but it also seems kind of trivial. Giving the idea of mapping programming language semantics to an existing domain like mathematics a complex name like "denotational semantics" just serves to make it harder to understand and more impenetrable.Generally I think naming things should make them easier to understand, e.g. naming "a number that represents the address of another object" a "pointer" is great, because it literally is something that points to another thing.
Denotational semantics is a terrible terrible name. I'm not even sure it should have a name. Can we call it "mathematical semantics" (if you map to maths)?
(I may be totally wrong here because I'm not a denotational semantics expert, but I have at least tried to follow it before getting whacked in the face with a load of philosophy.)
Reminds me a lot of REST. The core idea of REST is very simple, but it's also really hard to learn what that idea is because so much of it is hidden behind bullshit philosophy.
Nah, you're just not good with maths. Programming languages are mathematical objects and denotational semantics is merely treating languages as categories and looking for functors leading out of them.