# Semantic Functions

The $\lambda$-notation in the Agda definitions of semantic functions for *Scm*
corresponds closely to that in its published denotational semantics [(Mosses2025CSE)].
```agda
--"hide"

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

--"/hide"
module Examples.Scm.Semantic-Functions where
--"hide"

open import Examples.Scm.Abstract-Syntax
open import Examples.Scm.Domain-Equations
open import Examples.Scm.Auxiliary-Functions
import Notation
open Notation.Domains using (⟪_⟫)
open Notation.Functions using (_→ᶜ_; _→ˢ_)
open Notation.Flat using (↑)
open Notation.Flat.Booleans using (_⟶_,_; _==⊥_; true; false)
open Notation.Sums using (_in⊥_; _|⊥_)
open Notation.Products.Sequences using (_⋆; ⟨⟩; ⟨_⟩; _§_)
open Notation.Updates using (_[_/_])
--"/hide"

𝒦⟦_⟧   :  ⟪ Con →ˢ 𝐄 ⟫                      -- constant denotations
ℰ⟦_⟧   :  ⟪ Exp →ˢ 𝐔 →ᶜ (𝐄 →ᶜ 𝐂) →ᶜ 𝐂 ⟫     -- expression denotations
ℰ⋆⟦_⟧  :  ⟪ Exp⋆ →ˢ 𝐔 →ᶜ (𝐄 ⋆ →ᶜ 𝐂) →ᶜ 𝐂 ⟫  -- sequence denotations

𝒦⟦ int Z ⟧  = ↑ Z in⊥ 𝐄
𝒦⟦ #t ⟧     = ↑ true in⊥ 𝐄
𝒦⟦ #f ⟧     = ↑ false in⊥ 𝐄

ℰ⟦ con K ⟧ ρ κ               = κ (𝒦⟦ K ⟧)
ℰ⟦ ide I ⟧ ρ κ               = hold (ρ I) κ
ℰ⟦ ⦅ E ␣ E⋆ ⦆ ⟧ ρ κ          = ℰ⟦ E ⟧ ρ (λ ϵ → ℰ⋆⟦ E⋆ ⟧ ρ (λ ϵ⋆ → (ϵ |⊥ 𝐅) ϵ⋆ κ))
ℰ⟦ ⦅lambda I ␣ E ⦆ ⟧ ρ κ     = κ (   (λ ϵ⋆ κ′ →
                                       list ϵ⋆ (λ ϵ → alloc ϵ (λ α → ℰ⟦ E ⟧ (ρ [ α / I ]) κ′))
                                     ) in⊥ 𝐄 )
ℰ⟦ ⦅if E ␣ E₁ ␣ E₂ ⦆ ⟧ ρ κ   = ℰ⟦ E ⟧ ρ (λ ϵ → truish ϵ ⟶ ℰ⟦ E₁ ⟧ ρ κ , ℰ⟦ E₂ ⟧ ρ κ)
ℰ⟦ ⦅set! I ␣ E ⦆ ⟧ ρ κ       = ℰ⟦ E ⟧ ρ (λ ϵ → assign (ρ I) ϵ (κ (↑ unspecified in⊥ 𝐄)))

ℰ⋆⟦ ␣␣␣ ⟧ ρ κ      = κ ⟨⟩
ℰ⋆⟦ E ␣␣ E⋆ ⟧ ρ κ  = ℰ⟦ E ⟧ ρ (λ ϵ → ℰ⋆⟦ E⋆ ⟧ ρ (λ ϵ⋆ → κ (⟨ ϵ ⟩ § ϵ⋆)))
--"hide"

ℬ⟦_⟧   :  ⟪ Body →ˢ 𝐔 →ᶜ (𝐔 →ᶜ 𝐂) →ᶜ 𝐂 ⟫    -- body denotations
ℬ⁺⟦_⟧  :  ⟪ Body⁺ →ˢ 𝐔 →ᶜ (𝐔 →ᶜ 𝐂) →ᶜ 𝐂 ⟫   -- sequence denotations
𝒫⟦_⟧   :  ⟪ Prog →ˢ 𝐀 ⟫                     -- program execution answers

ℬ⟦ ␣␣ E ⟧ ρ κ = ℰ⟦ E ⟧ ρ (λ ϵ → κ ρ)
ℬ⟦ ⦅define I ␣ E ⦆ ⟧ ρ κ =
  ℰ⟦ E ⟧ ρ (λ ϵ → (ρ I ==⊥ ↑ unknown) ⟶ alloc ϵ (λ α → κ (ρ [ α / I ])) ,
  assign (ρ I) ϵ (κ ρ))
ℬ⟦ ⦅begin B⁺ ⦆ ⟧ ρ κ =
  ℬ⁺⟦ B⁺ ⟧ ρ κ

ℬ⁺⟦ ␣␣ B ⟧ ρ κ =
  ℬ⟦ B ⟧ ρ κ
ℬ⁺⟦ B ␣␣ B⁺ ⟧ ρ κ =
  ℬ⟦ B ⟧ ρ (λ ρ′ → ℬ⁺⟦ B⁺ ⟧ ρ′ κ)

𝒫⟦ ␣␣␣ ⟧    = finished initial-store
𝒫⟦ ␣␣ B⁺ ⟧  = ℬ⁺⟦ B⁺ ⟧ initial-env (λ ρ → finished) initial-store
--"/hide"
```

[(Mosses2025CSE)]: https://doi.org/10.1145/3759427.3760369