Skip to content

Domain Equations

The domains π’Ÿ Οƒ form a "standard collection of domains for arithmetic" in PCF, written \(\mathcal D_\sigma\) in (Plotkin1977LCP). As PCF is a simply-typed language, the domains π’Ÿ Οƒ are not reflexive, so their embedding in Agda can use ordinary type definitions, not involving bijections.

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

module Examples.PCF.Domain-Equations where

  open import Examples.PCF.Abstract-Syntax
  open import Notation.Domains
  open import Notation.Functions
  open import Notation.Flat.Booleans
  open import Notation.Flat.Naturals
  open import Notation.Updates
  open import Agda.Builtin.Nat renaming (_==_ to _==α΄Ί_) public

  π’Ÿ : Types β†’ Domain       -- standard domains
  π’Ÿ ΞΉ        = NatβŠ₯        -- natural numbers
  π’Ÿ o        = BoolβŠ₯       -- truth-values
  π’Ÿ (Οƒ β‡’ Ο„)  = π’Ÿ Οƒ β†’αΆœ π’Ÿ Ο„  -- functions
  variable x y z : βŸͺ π’Ÿ Οƒ ⟫

Environments ρ are type-preserving maps from variables to values. They are naturally modeled by a dependent type: Env Οƒ consists of type-preserving maps from variables in Vars Οƒ to their values in the domain π’Ÿ Οƒ. The environment ρβŠ₯ maps all variables to βŠ₯.

  Env = (Οƒ : Types) β†’ βŸͺ Vars Οƒ β†’Λ’ π’Ÿ Οƒ ⟫  -- typed environments
  variable ρ : Env
  ρβŠ₯ : Env                               -- initial environment
  ρβŠ₯ _ _ = βŠ₯

Extension or overriding typed environments, written ρ [ v / x ]β€² here, requires instances of the equality tests for both variables and types. The definition of the latter is somewhat tedious:

  _==β±½_ : Vars Οƒ β†’ Vars Οƒ β†’ Bool
  (Ξ± i Οƒ ==β±½ Ξ± iβ€² Οƒ)  =  (i ==α΄Ί iβ€²)
  instance
    eqV : Eq (Vars Οƒ)
    _==_ {{eqV}} = _==β±½_
  instance
    eqT : MaybeEq Types
    eqT ._==?_ ΞΉ ΞΉ = just refl
    eqT ._==?_ o o = just refl
    eqT ._==?_ (Οƒ β‡’ Ο„) (σ₁ β‡’ τ₁) with Οƒ ==? σ₁  | Ο„ ==? τ₁
    eqT ._==?_ (Οƒ β‡’ Ο„) (σ₁ β‡’ τ₁)    | just refl | just refl = just refl
    eqT ._==?_ (Οƒ β‡’ Ο„) (σ₁ β‡’ τ₁)    | _         | _         = nothing
    eqT ._==?_ _ _ = nothing

  _[_/_]β€² : Env β†’ βŸͺ π’Ÿ Οƒ ⟫ β†’ Vars Οƒ β†’ Env
  -- ρ [ v / x ]β€² maps x to v, and other xβ€² to ρ xβ€²
  _[_/_]β€² {Οƒ} ρ x v = ρ [ Οƒ ← ρ Οƒ [ x / v ] ]