Semantic Functions

The semantic equations below correspond closely to those found in textbooks on denotational semantics (e.g., (Reynolds1998TPL)). In larger conventional definitions, fold and unfold are usually left implicit, but Agda does not support this.

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

module Examples.LC.Semantic-Functions where

  open import Examples.LC.Abstract-Syntax
  open import Examples.LC.Domain-Equations
  open import Notation.Domains
  open import Notation.Functions
  open import Notation.Recursion
  open import Notation.Updates

  ⟦_⟧ : Exp → ⟪ Env →ᶜ D∞ ⟫
  ⟦ var v ⟧ ρ        = ρ v
  ⟦ ⦅λ v ␣ e ⦆ ⟧ ρ   = fold ( λ δ → ⟦ e ⟧ (ρ [ δ / v ]) )
  ⟦ ⦅ e₁ ␣ e₂ ⦆ ⟧ ρ  = unfold ( ⟦ e₁ ⟧ ρ ) ( ⟦ e₂ ⟧ ρ )