Skip to content

Domain Equations

The domains for Scm are somewhat simpler than for the denotational semantics in the Scheme standards (Scheme), but still involve all our postulated domain constructors. Using definitional equations D = E instead of postulated bijections D ≅ E for non-recursive collections of domains avoids the need for the functions fold and unfold in definitions of denotations.

{-# OPTIONS --rewriting --confluence-check #-}

module Examples.Scm.Domain-Equations where

  open import Examples.Scm.Abstract-Syntax
  open import Notation.Domains
  open import Notation.Functions
  open import Notation.Flat
  open import Notation.Flat.Booleans
  open import Notation.Flat.Naturals
  open import Notation.Sums
  open import Notation.Products
  open import Notation.Products.Sequences

  postulate Loc : Set
  𝐋  =  Loc +⊥                -- locations
  𝐍  =  Nat⊥                  -- natural numbers
  𝐓  =  Bool⊥                 -- booleans
  𝐑  =  Int +⊥                -- numbers
  𝐏  =  𝐋 × 𝐋                 -- pairs
  𝐔  =  Ide →ˢ 𝐋              -- environments
  data Misc : Set where null unallocated undefined unspecified : Misc
  𝐌  =  Misc +⊥               -- miscellaneous
  postulate 𝐄 : Domain        -- expressed values
  𝐒  =  𝐋 →ᶜ 𝐄                -- stores
  postulate 𝐀 : Domain        -- answers
  𝐂  =  𝐒 →ᶜ 𝐀                -- command continuations
  𝐅  =  𝐄 ⋆ →ᶜ (𝐄 →ᶜ 𝐂) →ᶜ 𝐂  -- procedure values

The published denotational semantics of Scm (Mosses2025CSE) defines the domain \(𝐄\) of expression values by the equation \(𝐄 = 𝐓 + 𝐑 + 𝐏 + 𝐌 + 𝐅\), and the domain \(𝐅\) of procedure values by \(𝐅 = 𝐄^* \to (𝐄 \to 𝐂) \to 𝐂\). Mutually recursive groups of domain equations have well-defined solutions, but in Agda, defining both the corresponding domains 𝐄 and 𝐅 by equations would cause the type checker to diverge. Postulating one (or both) of these domains avoids divergence; postulating 𝐄 also has the benefit that the embeddings and projections for its summands subsume the bijection between 𝐄 and its intended structure.

The following postulates instantiate the notation used in denotational semantics for sum domains: injection (δ in⊥ 𝐄), inspection (ε ∈⊥ D), and projection (ε |⊥ D) for each summand D of 𝐄.

  postulate instance
    E+=T  : 𝐄 ≳ 1 ↦ 𝐓
    E+=R  : 𝐄 ≳ 2 ↦ 𝐑
    E+=P  : 𝐄 ≳ 3 ↦ 𝐏
    E+=M  : 𝐄 ≳ 4 ↦ 𝐌
    E+=F  : 𝐄 ≳ 5 ↦ 𝐅

(where the numerical indices and order of the summand declarations are arbitrary).


  postulate instance
    eqL   : Eq Loc
    eqM   : Eq Misc
    eqR   : Eq Int

  variable
    α : ⟪ 𝐋 ⟫;  ρ : ⟪ 𝐔 ⟫;  μ  : ⟪ 𝐌 ⟫;    ϵ : ⟪ 𝐄 ⟫
    σ : ⟪ 𝐒 ⟫;  θ : ⟪ 𝐂 ⟫;  ϵ⋆ : ⟪ 𝐄 ⋆ ⟫;   φ : ⟪ 𝐅 ⟫;  κ : ⟪ 𝐄 →ᶜ 𝐂 ⟫