appendix sectionnotation

Recursive types, domains, and observations

symbol	meaning	first
symbol	meaning	first
$μ X . A$ , ${fold}_{μ X . A}$ , $unfold$	iso-recursive type and its explicit boundary terms	chapter 12
$ListNat$ , $nil$ , $cons$ , $cell (n, e)$	eager list type, constructor terms, and canonical folded-cell abbreviation	chapter 12
$A \equiv_{μ} B$	bisimilarity of closed contractive regular type trees	chapter 12
${PCF}_{n}$	the chapter’s call-by-name PCF language	chapter 12
$e ⇓ n$ , $e ⟼^{ω}$	PCF convergence to $n$ and infinite reduction	chapter 12
$⊑_{D}$ , $⊥$ , $⨆_{i} d_{i}$	approximation order, least element, and omega-chain lub	chapter 12
$[D \to E]_{c}$	continuous maps with pointwise order	chapter 12
$D_{⊥}$ , $↑ d$	lifting and its nonbottom injection	chapter 12
$lfp (F)$ , $μ Φ (p)$	Kleene least fixed point and parameterized least fixed point	chapter 12
$L$ , $d ↾ k$	partial-list domain and its depth- $k$ truncation	chapter 12
$out$ , $in$	inverse maps for $L ≅ ({*} + N \times L)_{⊥}$	chapter 12
$[[A]]$ , $[[e]] η$	PCF type and term denotation	chapter 12
$d R_{A} e$ , $η R_{Γ} γ$	semantic logical approximation and related environments	chapter 12
$v \approx_{n}^{A} w$ , $e E_{n}^{A} d$	indexed eager value and term equivalence	chapter 12
$γ \approx_{n}^{Γ} δ$	pointwise related closing value substitutions	chapter 12
$d \overset{k}{⇝} d^{'}$	observation of $k$ consecutive list cells and residual tail	chapter 12
$Z_{A, B}$ , $copy$	eta-delayed eager fixed point and recursive list copier	chapter 12