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.
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?
Oh, I don’t follow the math at all, and much of the terminology is gibberish to me. I just didn’t want you thinking you couldn’t understand something you probably could, if you spent some time in the field.
I agree that understanding the math is always next level; you almost have to be working in the domain, or at least be a mathematician, to follow the maths in papers like this. I sort of gloss over it, now; despite being 4 credits short of a math minor, I’ve never use any of it outside of set theory and a little discrete math in my career and have forgotten nearly everything past algebra. It’s frustrating, but although I enjoyed it, I didn’t enjoy it enough to keep up in my free time and it’s a perishable skill.
Anyway, while coming up with and proving the research requires real skill, I hate the idea of someone assuming they’re incapable of understanding something, when it’s often not a lack of potential, only a lack of education.
Lastly: I do think we have limits. I didn’t take that last math course because I was already struggling with the number of levels of abstraction required to mentally retain the tools to do the work, and realized I’d never be a professional mathematician. There are levels of math I’m simply too stupid to understand, no matter how much time I spent studying. But the barrier in this paper IMHO seems to be that it’s highly domain specific, and so demands a fair amount of understanding of domain terminology.
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.