fixpt · Total Denotational Semantics
fixpt.de

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

  1. It is impossible to give a faithful, executable encoding of such a semantics in a programming language, and
  2. 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.

  • 𝕽𝖚𝖆𝖎𝖉𝖍𝖗𝖎𝖌𝖍@midwest.social
    1·
    2 months ago

    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.