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 concurrency^1^^2^.
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.
If was half a joke, but that mathematics might as well have been hieroglyphics.
Would you class this as computational theory? As a software developer is this field likely to be used in a day to day manner or is it more abstract than that?
Semantics was originally studied as model theory, and today is phrased with category theory. You use this every day when you imagine what a program does in terms of machine effects.