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?
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.
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.