Evaluation-strategy translations

symbol	meaning	first
symbol	meaning	first
$M⟼N$	one compatible call-by-name beta step	definition 37.1
$M⟼N$	one compatible value-restricted beta step	definition 37.1
$M^{\mathsf{n}}$	call-by-name translation into $\mathsf{lin}$	section 37.3
$M^{\mathsf{v}}$	call-by-value or call-by-need term translation	section 37.4
$V^{+}$, $A^{+}$	unboxed value and value-type translations	section 37.4
$!A$, $!M$	exponential type and promoted target term	section 37.2
$A⊸B$	linear target function type	section 37.2
$\mathsf{let}!x=M\mathsf{in}N$	exponential elimination in $\mathsf{lin}$ or $\mathsf{aff}$	definition 37.2
$Need-G$, $Aff-Weak$	source garbage collection and its affine target image	definition 37.10

All decorated reduction arrows are roles of the shared reduction family. The calculus name in the subscript is semantically significant; no unmarked arrow abbreviates all four relations.