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.