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 avoids the need for the functions fold and unfold.

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

module Examples.Scm.Domain-Equations where

open import Examples.Scm.Abstract-Syntax using (Ide; Int)
import Notation
open Notation.Domains using (Domain; ⟪_⟫)
open Notation.Functions using (_→ᶜ_; _→ˢ_)
open Notation.Flat using (_+⊥)
open Notation.Flat.Booleans using (Bool⊥)
open Notation.Flat.Naturals using (Nat⊥)
open Notation.Sums using (_≳_↦_)
open Notation.Products using (_×_)
open Notation.Products.Sequences using (_⋆)

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 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 ↦ 𝐅

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