Semantic functions (Revised7.0 Report on the Algorithmic Language Scheme (Unofficial))

Next: Auxiliary functions, Previous: Domain equations, Up: Formal semantics [Contents][Index]

7.2.3 Semantic functions ¶

 $\begin{array}{l} 𝒦 & : & Con \to E \\ ℰ & : & Exp \to U \to P \to K \to C \\ ℰ^{*} & : & {Exp}^{*} \to U \to P \to K \to C \\ 𝒞 & : & {Com}^{*} \to U \to P \to C \to C \end{array}$

Definition of $𝒦$ deliberately omitted.

$ℰ ⟦ K ⟧ = λ, ρ, ω, κ . send (𝒦 ⟦ K ⟧), κ$

$ℰ ⟦ I ⟧ = λ, ρ, ω, κ . hold$

$(lookup ρ, I)$

$(single (λ, ϵ .$

$ϵ = undefined \to$

$wrong “ undefined variable ”,$

$send ϵ κ))$

$ℰ ⟦ (E_{0}, E^{*}) ⟧ =$

$λ, ρ, ω, κ . ℰ^{*}$

$(permute (⟨ E_{0} ⟩ § E^{*}))$

$ρ$

$ω$

$(λ, ϵ^{*} . ($

$(λ, ϵ^{*} . applicate (ϵ^{*} ↓ 1), (ϵ^{*} † 1), ω, κ)$

$(unpermute ϵ^{*})))$

$ℰ ⟦ (lambda (I^{*}), Γ^{*}, E_{0}) ⟧ =$

$λ, ρ, ω, κ . λ, σ .$

$new σ \in L \to$

$send$

$($

$⟨$

$new σ | L,$

$λ, ϵ^{*}, ω^{'}, κ^{'} . # ϵ^{*} = # I^{*} \to$

$tievals$

$(λ, α^{*} .$

$(λ, ρ^{'} . 𝒞 ⟦ Γ^{*} ⟧ ρ^{'}, ω^{'}, (ℰ ⟦ E_{0} ⟧, ρ^{'} ω^{'} κ^{'}))$

$(extends ρ, I^{*}, α^{*}))$

$ϵ^{*},$

$wrong “ wrong number of arguments ” ⟩$

$in E$

$κ$

$(update (new σ | L), unspecified σ),$

$wrong “ out of memory ”, σ$

$ℰ ⟦ (lambda (I^{*} . I), Γ^{*}, E_{0}) ⟧ =$

$λ, ρ, ω, κ . λ, σ .$

$new σ \in L \to$

$send$

$($

$⟨$

$new σ | L,$

$λ, ϵ^{*}, ω^{'}, κ^{'} .$

$# ϵ^{*} \geq # I^{*} \to$

$tievalsrest$

$(λ, α^{*} .$

$(λ, ρ^{'} . 𝒞 ⟦ Γ^{*} ⟧ ρ^{'}, ω^{'}, (ℰ ⟦ E_{0} ⟧, ρ^{'} ω^{'} κ^{'}))$

$(extends ρ, (I^{*} § ⟨ I ⟩), α^{*}))$

$ϵ^{*}$

$(# I^{*}),$

$wrong “ too few arguments ” ⟩ in E)$

$κ$

$(update (new σ | L), unspecified σ),$

$wrong “ out of memory ”, σ$

$ℰ ⟦ (lambda I, Γ^{*}, E_{0}) ⟧ = ℰ ⟦ (lambda (. I), Γ^{*}, E_{0}) ⟧$

$ℰ ⟦ (if E_{0}, E_{1}, E_{2}) ⟧ =$

$λ, ρ, ω, κ . ℰ ⟦ E_{0} ⟧, ρ, ω, (single (λ, ϵ .$

$truish ϵ \to ℰ ⟦ E_{1} ⟧, ρ, ω, κ,$

$ℰ ⟦ E_{2} ⟧, ρ, ω, κ))$

$ℰ ⟦ (if E_{0}, E_{1}) ⟧ =$

$λ, ρ, ω, κ . ℰ ⟦ E_{0} ⟧, ρ, ω, (single (λ, ϵ .$

$truish ϵ \to ℰ ⟦ E_{1} ⟧, ρ, ω, κ,$

$send unspecified κ))$

Here and elsewhere, any expressed value other than $undefined$ may be used in place of $unspecified$ .

$ℰ ⟦ (set! I, E) ⟧ =$

$λ, ρ, ω, κ . ℰ ⟦ E ⟧, ρ, ω, (single (λ, ϵ . assign$

$(lookup ρ, I)$

$ϵ$

$(send unspecified κ)))$

$ℰ^{*} ⟦ ⟧ = λ, ρ, ω, κ . κ ⟨ ⟩$

$ℰ^{*} ⟦ E_{0}, E^{*} ⟧ =$

$λ, ρ, ω, κ . ℰ ⟦ E_{0} ⟧, ρ, ω, (single (λ, ϵ_{0} . ℰ^{*} ⟦ E^{*} ⟧, ρ, ω, (λ, ϵ^{*} . κ, (⟨ ϵ_{0} ⟩ § ϵ^{*}))))$

$𝒞 ⟦ ⟧ = λ, ρ, ω, θ . θ$

$𝒞 ⟦ Γ_{0}, Γ^{*} ⟧ = λ, ρ, ω, θ . ℰ ⟦ Γ_{0} ⟧, ρ, ω, (λ, ϵ^{*} . 𝒞 ⟦ Γ^{*} ⟧, ρ, ω, θ)$