Total Denotational Semantics
September 23, 2024
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.
Read More ...