appendix sectionnotation

Foundational derivations, programs, and proofs

symbol	meaning	first
symbol	meaning	first
$D :: J$	$D$ is a finite derivation with root $J$	chapter 1
$h (D)$	height of a derivation; a zero-premise rule has height one	chapter 1
$Γ ⊢_{R} J$	hypothetical derivability of $J$ from assumption judgments $Γ$ under rule set $R$	chapter 1
$e ⟼_{A} e^{'}$	one small step in the arithmetic fragment	chapter 1
$e ⟼_{A}^{*} e^{'}$	reflexive transitive closure of arithmetic-fragment steps	chapter 1
$e ⇓_{A} n$	arithmetic-fragment big-step evaluation of $e$ to numeral $n$	chapter 1
$e ⟼ e^{'}$	one full-language call-by-value small step generated by E-App-L–E-Add-S	chapter 1
$e ⟼^{*} e^{'}$	reflexive transitive closure of full-language call-by-value steps	chapter 1
$e ⇓ v$	full-language big-step evaluation of $e$ to value $v$	chapter 1
$E ⟨ e ⟩$	fill the unique hole of evaluation context $E$ with $e$	chapter 1
$FV (e)$	free term variables of $e$	chapter 1
$e =_{α} e^{'}$	alpha-equivalence of raw named terms; ordinary $=$ compares their quotient terms	definition 1.53, convention 1.57
$e [a / x]$	capture-avoiding substitution of term $a$ for free $x$	chapter 1
$e ⟨ y / x ⟩$	fresh renaming of free $x$ to $y$	chapter 1
$⊢ e : A$	abbreviation for $\cdot ⊢ e : A$	chapter 2
$e ⟶_{p} e^{'}$	compatible proof reduction, distinct from deterministic call-by-value evaluation	chapter 2
$R_{A}$	reducibility candidate indexed by simple type $A$	chapter 2
$ν (e)$	maximum reduction height of a strongly normalizing term	chapter 2
$fv (A)$	free individual variables of a first-order term, formula, or context	chapter 3
$A^{[n]}$	$n$ selected antecedent occurrences for multicut bookkeeping, not formula syntax	chapter 3
$Ξ ⊢ p : A$	labeled first-order natural-deduction proof-term typing	chapter 3
$Λ a . p, p [t]$	universal proof abstraction and instantiation	chapter 3
$pack (t, p)$	existential package with witness $t$ and proof $p$	chapter 3
$unpack (p; a, h . q)$	existential elimination binding witness $a$ and proof name $h$ in $q$	chapter 3