# 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.
```agda
--"hide"
{-# OPTIONS --rewriting --confluence-check --lossy-unification #-}

--"/hide"
module Examples.PCF.Domain-Equations where
--"hide"

open import Examples.PCF.Abstract-Syntax
open import Notation
open Notation.Flat.Booleans using (Bool; BoolβŠ₯)
open Notation.Flat.Naturals using (NatβŠ₯; eqNat)
--"/hide"

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

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 `βŠ₯`.
```agda
Env = (Οƒ : Types) β†’ βŸͺ Vars Οƒ β†’Λ’ π’Ÿ Οƒ ⟫  -- typed environments
--"hide"
variable ρ : Env
--"/hide"
ρβŠ₯ : Env                               -- initial environment
ρβŠ₯ _ _ = βŠ₯
```
Extension or overriding typed environments, written `ρ [ v / x ]β€²`,
requires instances of the equality tests
for both variables and types. The definition of the latter is somewhat tedious.
```agda
--"hide"
open Notation.Flat.Booleans using (Eq; _==_)
open Notation.Updates using (_[_/_])
_==β±½_ : Vars Οƒ β†’ Vars Οƒ β†’ Bool
open import Agda.Builtin.Nat renaming (_==_ to _==α΄Ί_) public
(Ξ± i Οƒ ==β±½ Ξ± iβ€² Οƒ)  =  (i ==α΄Ί iβ€²)
instance
  eqV : Eq (Vars Οƒ)
  _==_ {{eqV}} = _==β±½_
open Notation.Updates using (MaybeEq; _==?_; just; nothing; refl; _[_←_])
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 ] ]
--"/hide"
```

[(MFPS2026-Agda)]: https://pdmosses.github.io/mfps2026-agda/
[(Plotkin1977LCP)]: https://doi.org/10.1016/0304-3975(77)90044-5