Denotational Semantics in Agda
Table of Contents
This project (started in 2024) aims to make it straightforward to take an existing denotational semantics of a programming language, and use Agda to check its well-formedness, as well to prove properties of individual programs.
The Problem #
A Scott–Strachey style denotational semantics1 is based on Scott-domains. It assumes that a domain is an appropriate kind of cpo, and defines domains (up to isomorphism) using various domain constructors, allowing mutual recursion. All functions on domains specified in λ-notation are Scott-continuous, and endofunctions have least fixed points.
Agda does not assume that types are Scott-domains, nor that functions specified in λ-notation are continuous. Some Agda libraries have been developed to support Scott-domains; but when using them, a domain is represented as a pair of a type of elements and other data; and a continuous function is represented as a pair of a function and a proof of its continuity. These representations give rise to undesirable notational overhead and obfuscation when specifying elements of domains in λ-notation.
As a novice Agda user, I developed a lightweight workaround for this problem, reported in the paper Towards Verification of a Denotational Semantics of Inheritance. However, I would like to find a more principled solution. Participation of expert Agda users will surely be needed…
A Proposed Approach #
The idea is to allow named types to be declared to be domains.
To avoid extending the syntax of Agda, it has been suggested to me that
a universe Domain (hierarchy) could be added as built-in,
but that would require extending the Agda compiler.
When declared to be a domain, an Agda type is to have a partial order with a least element ⊥, closed (at least) under limits of monotone ascending ω-chains. All functions between domains are to be Scott-continuous, preserving the partial order and limits; the limit of the ascending Kleene chain of an endofunction on a domain is then its least fixed point.
Groups of Agda types declared to be domains are to be definable (up to isomorphism) in terms of flat domains (lifted sets) and built-in domain constructors (including function domains, Cartesian products, sum domains, lifted domains). The type of all functions from an ordinary type to a domain may also be treated as a domain, implicitly ordered pointwise.
Recursive references to domains are not to require explicit guards, and type checking is to allow the isomorphisms between domains and their definitions to be left implicit when expressing elements of domains in λ-notation.
Experiments #
Some experiments with using a simplified version2 of the above approach can be browsed on web pages or PDFs at https://pdmosses.github.io/xds-agda/.
The experiments currently include denotational semantics of the untyped λ-calculus, PCF, and core Scheme.
A denotational semantics of a programming language maps programs and their phrases directly to their denotations: immutable values – typically higher-order functions. The denotation of a complete program represents its potential behaviour when executed. Denotations are compositional: the denotation of a phrase is defined inductively in terms of the denotations of its subphrases, independently of their form. The denotations of loops and recursive definitions involve fixed points of functions on denotations. ↩︎
For simplicity, domains are defined to be unordered pointed sets, and endofunctions are required only to have well-defined fixed points. Postulates corresponding to the intended cpo structure of domains, and the continuity of functions between domains, are to be added. ↩︎