appendix sectionnotation

Algebraic subtyping and biunification

symbol	meaning	first
symbol	meaning	first
$P, N$	positive/output and negative/input polar types	definition 19.1
$[Δ^{-}] P^{+}$	polar typing scheme	definition 19.1
$P \leq_{a} N$	MLsub algebraic subtype or generated constraint	definition 19.2
$S \leq_{\forall} S^{'}$	lambda-lifted scheme subsumption	definition 19.3
$ξ^{+}, ξ^{-}$	positive and negative faces of a bisubstitution	definition 19.4
${subB}_{0} (c), B_{0} (H; C)$	sorted decomposition and visited-pair biunification work list	definition 19.8
$P_{0} (Π; e)$	local polar principal-inference algorithm	definition 19.12