appendix sectionnotation

Specialization, driving, and staged terms

notation	meaning	owner
notation	meaning	owner
$P; ρ ⊢ e ⇓ v$ , $known (n)$ , $res (r)$	Scheme0 evaluation and the static/residual result distinction	chapter 127
$Q ≼ Q^{'}$ , $msg (e, e^{'})$	homeomorphic embedding used by the whistle and most-specific generalization on de Bruijn-encoded first-order configuration trees, with substitution only at free-variable leaves	chapter 128
$e ⊑_{op} e^{'}$ , $e ⪯_{imp} e^{'}$ , $e ⪯_{s} e^{'}$ , $e ≃_{cost} e^{'}$	may-termination approximation, named-call improvement, and strong improvement, with bidirectional cost equivalence, for SC-CBV	chapter 128
$Δ; Γ ⊢ M : A$ , $u :: A \in Δ$	dual-context staged typing and a persistent assumption; $Δ$ is the chapter-local modal-context exception	chapter 129
$M \approx_{ctx} N$	contextual observational equality in the imported staging comparison	chapter 129
$V [[τ]]$ , $E [[τ]]$ , $G [[Γ]]$	Tan–Wei step-indexed value, term, and closing-environment relations for stage-erased types and environments	chapter 129
$σ_{1}; Ω; Γ ⊢_{n}^{⋆} e : τ ⇝ e^{'}; σ_{2}$	MacoCaml source elaboration at level $n$ and compiler mode $⋆$ , with input and output compile-time heaps	chapter 129
$Γ ⊢ M : τ @ A$ , $▹_{α} τ$ , $⟶_{s}$	dependent term typing at stage word $A$ , code type for stage $α$ , and staged execution	chapter 130
$⟨ M ⟩_{α}$ , $\sim_{α} M$ , $%_{α} M$	quotation, escape, and cross-stage persistence	chapter 130
$V^{A}$ , $h^{A}$ , $E_{B}^{A}$	staged values, constant-headed final forms, and evaluation contexts with whole stage $A$ and hole stage $B$	chapter 130
$⌊ M ⌋_{a}$ , $u ⟶_{a} v$	binder-annotation erasure and its annotation-free full reduction; every computational and staging constructor is retained	chapter 130