Global metalanguage

These forms retain one role throughout the book. A chapter that follows a standard source with different notation records the exception in the notation registry and introduces the symbol where it is first used.

form	semantic role	binding / scope
form	semantic role	binding / scope
$E[u/x]$, $E[B/X]$	single capture-avoiding substitution	postfix; global
$E[\theta ]$, $E[\gamma ]$	simultaneous substitution or family action	postfix; global
$\theta ;\eta$	right-action substitution composition: $E[\theta ;\eta ]=(E[\theta ])[\eta ]$	composition; global
$fa$	object-language application	left associative
$t[A]$	explicit type application	postfix
$F(a)$	meta-level function application	ordinary mathematics
$E⟨e⟩$	fill the unique hole of evaluation context $E$	postfix; global
$r{⇝}_0{r}^{\prime }$	one root contraction	relation; global
$e⟶e^{\prime }$	one compatible small step	relation; global
$e{⟶}^{\ast }{e}^{\prime }$	reflexive-transitive compatible reduction	relation; global
$s⇝a$	elaboration or insertion output	relation; global
${\mathcal{T}}_{S\to T}(e)$	named syntax-to-syntax translation	application; global
$\mathrm{strip}(e)$	named removal/stripping map on syntax	application; first used in chapter 35
$[[e{]]}_{\eta }$	semantic interpretation under valuation $\eta$	atom; global
$e{=}_{\alpha }{e}^{\prime }$	alpha-equivalence of raw named terms	relation; first defined in definition 1.53

Application and postfix substitution bind more tightly than arrows; arrows associate to the right; binder scope extends to the next explicit delimiter. Double brackets are reserved for semantic interpretation. Erasure, normalization, elaboration, CPS maps, and other syntax transformations receive named operators.