House notation¶
Every chapter writes mathematics the same way, so a symbol means one thing across all twenty-five chapters. This page is the reference. Each chapter's README.md has a ## Notation section that lists the symbols that chapter uses, pointing here for the shared ones and defining any new ones.
Math is LaTeX inside Markdown: $…$ inline and $$…$$ for display (see STYLE.md §5). Use only standard LaTeX that both KaTeX (the course website) and GitHub's MathJax render: no custom macros, and nothing from §10's list of macros KaTeX does not support. ./course validate renders every formula with the site's KaTeX and reports the ones that fail (§10). The "Write" column is the exact source to use.
1. Sets, functions, logic¶
| Concept | Write | Renders |
|---|---|---|
| set literal, empty set | \{a, b\}, \emptyset |
\(\{a, b\}\), \(\emptyset\) |
| set-builder | \{\, x \in S \mid P(x) \,\} |
\(\{\, x \in S \mid P(x) \,\}\) |
| union, intersection, difference | \cup, \cap, \setminus, \bigcup_{p}, \bigcap_{p} |
\(A \cup B\), \(A \cap B\), \(A \setminus B\) |
| subset, proper subset | \subseteq, \subsetneq |
\(A \subseteq B\), \(A \subsetneq B\) |
| cardinality | \lvert S \rvert (never a bare | inside a table) |
\(\lvert S \rvert\) |
| power set | \mathcal{P}(S) |
\(\mathcal{P}(S)\) |
| function, partial function | f : A \to B, f : A \rightharpoonup B |
\(f : A \to B\) |
| update | f[x \mapsto v] |
\(f[x \mapsto v]\) |
| sequence, concatenation, empty sequence | \langle a_1, \dots, a_k \rangle, u \cdot v, \langle\rangle |
\(\langle a_1, \dots, a_k \rangle\) |
| logic | \land, \lor, \neg, \Rightarrow, \iff, \forall, \exists |
\(\forall x.\ P(x) \Rightarrow Q(x)\) |
| definitional equality | \triangleq |
\(\mathrm{Dom}(n) \triangleq \dots\) |
Names of functions and relations with more than one letter are upright: \mathrm{idom}(n), never idom(n) (which typesets as a product of four variables).
2. Orders and lattices¶
| Concept | Write | Renders |
|---|---|---|
| partial order, strict | \sqsubseteq, \sqsubset |
\(x \sqsubseteq y\) |
| join, meet (binary, big) | \sqcup, \sqcap, \bigsqcup_{p}, \mathop{\Large\sqcap}_{p} (not \bigsqcap: KaTeX has no such macro, §10) |
\(x \sqcup y\), \(\bigsqcup_{p} x_p\), \(\mathop{\Large\sqcap}_{p} x_p\) |
| top, bottom | \top, \bot |
\(\top\), \(\bot\) |
| lattice | (L, \sqsubseteq, \sqcup, \sqcap, \bot, \top) |
\((L, \sqsubseteq)\) |
| height | h(L) |
\(h(L)\) |
| monotone / distributive | prose + f(x \sqcup y) = f(x) \sqcup f(y) |
|
| least / greatest fixed point | \mathrm{lfp}(F), \mathrm{gfp}(F) |
\(\mathrm{lfp}(F)\) |
| Kleene iterates | F^{i}(\bot) |
\(F^{i}(\bot)\) |
Convention: dataflow facts grow up the lattice, \(\bot\) is "no information yet" for may-analyses. When a chapter uses the opposite (dual) orientation — dominators are the classic case — it says so in its Notation section.
3. Graphs and control-flow graphs¶
| Concept | Write | Renders |
|---|---|---|
| flowgraph | G = (N, E, r) with entry r |
\(G = (N, E, r)\) |
| edge | u \to v, (u, v) \in E |
\(u \to v\) |
| predecessors, successors | \mathrm{preds}(n), \mathrm{succs}(n) |
\(\mathrm{preds}(n)\) |
| path, path of length ≥ 1 | u \leadsto v, u \to^{+} v |
\(u \leadsto v\), \(u \to^{+} v\) |
| reverse graph | G^{R} |
\(G^{R}\) |
| sizes | n = \lvert N \rvert, e = \lvert E \rvert |
\(n\), \(e\) |
| DFS preorder / postorder / RPO number | \mathrm{pre}(v), \mathrm{post}(v), \mathrm{rpo}(v) |
\(\mathrm{rpo}(v)\) |
| DFS spanning tree, ancestor | T, u \preceq_T v ("u is an ancestor of v") |
\(u \preceq_T v\) |
| loop connectedness | d(G) |
\(d(G)\) |
Node names in math match the diagrams and tables exactly (\(B\), not \(b\) or B1).
4. Dominance and loops¶
| Concept | Write | Renders |
|---|---|---|
| dominates, strictly dominates | d \mathrel{\mathrm{dom}} n, d \mathrel{\mathrm{sdom}} n |
\(d \mathrel{\mathrm{dom}} n\), \(d \mathrel{\mathrm{sdom}} n\) |
| post-dominates | p \mathrel{\mathrm{pdom}} n |
\(p \mathrel{\mathrm{pdom}} n\) |
| dominator set | \mathrm{Dom}(n) |
\(\mathrm{Dom}(n)\) |
| immediate (post-)dominator | \mathrm{idom}(n), \mathrm{ipdom}(n) |
\(\mathrm{idom}(n)\) |
| semidominator | \mathrm{sdom}(n) (the function; context disambiguates it from the relation) |
\(\mathrm{sdom}(n)\) |
| dominator tree, depth | \mathcal{D}, \mathrm{depth}_{\mathcal{D}}(n) |
\(\mathcal{D}\) |
| dominance frontier, of a set, iterated | \mathrm{DF}(n), \mathrm{DF}(S), \mathrm{DF}^{+}(S) |
\(\mathrm{DF}^{+}(S)\) |
| control dependence | \mathrm{CD}(n) |
\(\mathrm{CD}(n)\) |
| natural loop of back edge / of header | \mathrm{loop}(t \to h), \mathrm{body}(h) |
\(\mathrm{loop}(t \to h)\) |
5. Grammars and parsing¶
| Concept | Write | Renders |
|---|---|---|
| grammar | G = (N, T, P, S) |
\(G = (N, T, P, S)\) |
| nonterminals, terminals, strings | A, B \in N; a, b \in T; \alpha, \beta, \gamma \in (N \cup T)^{*}; w \in T^{*} |
\(\alpha \in (N \cup T)^{*}\) |
| production | A \to \alpha |
\(A \to \alpha\) |
| derivation step, closure, leftmost | \Rightarrow, \Rightarrow^{*}, \Rightarrow^{+}, \Rightarrow_{\mathrm{lm}} |
\(\alpha \Rightarrow^{*} \beta\) |
| empty string, end marker | \varepsilon, \$ |
\(\varepsilon\), \(\$\) |
| language | L(G) |
\(L(G)\) |
| sets | \mathrm{Nullable}, \mathrm{FIRST}(\alpha), \mathrm{FOLLOW}(A), \mathrm{PREDICT}(A \to \alpha) |
\(\mathrm{FIRST}_k(\alpha)\) |
| k-prefix, k-concatenation | \mathrm{FIRST}_k, \oplus_k |
\(L_1 \oplus_k L_2\) |
| LR item | [A \to \alpha \bullet \beta,\ a] |
\([A \to \alpha \bullet \beta,\ a]\) |
The end marker is a literal dollar sign: in math write \$; in prose outside math write `$` (code) — a bare $ in prose starts a formula on the website.
6. Types and semantics¶
| Concept | Write | Renders |
|---|---|---|
| typing judgment | \Gamma \vdash e : \tau |
\(\Gamma \vdash e : \tau\) |
| bidirectional: synthesize / check | \Gamma \vdash e \Rightarrow \tau, \Gamma \vdash e \Leftarrow \tau |
\(\Gamma \vdash e \Rightarrow \tau\) |
| context extension | \Gamma, x : \tau |
\(\Gamma, x : \tau\) |
| type variables, schemes | \alpha, \beta; \forall \vec{\alpha}.\, \tau |
\(\forall \vec{\alpha}.\, \tau\) |
| substitution, application | \sigma = [\alpha \mapsto \tau], \sigma\tau |
\(\sigma\tau\) |
| subtyping | \tau_1 <: \tau_2 |
\(\tau_1 <: \tau_2\) |
| inference rule | \dfrac{\Gamma \vdash e_1 : \mathsf{int} \quad \Gamma \vdash e_2 : \mathsf{int}}{\Gamma \vdash e_1 + e_2 : \mathsf{int}}\ (\textsf{T-Add}) (rule names in \textsf; KaTeX has no \textsc) |
see below |
| small-step, big-step | e \longrightarrow e', \langle e, \sigma \rangle \Downarrow v |
\(e \longrightarrow e'\) |
| base types | \mathsf{int}, \mathsf{bool} |
\(\mathsf{int}\) |
(Greek letters are overloaded on purpose, as in the literature: in grammar chapters \(\alpha\) is a string of symbols, in type chapters a type variable. Each chapter's Notation section says which.)
7. Dataflow, SSA, IR¶
| Concept | Write | Renders |
|---|---|---|
| block facts | \mathrm{IN}[B], \mathrm{OUT}[B] |
\(\mathrm{IN}[B]\) |
| transfer function | f_B(x) = \mathrm{gen}_B \cup (x \setminus \mathrm{kill}_B) |
\(f_B\) |
| meet over paths, maximal fixed point | \mathrm{MOP}, \mathrm{MFP} |
\(\mathrm{MFP} \sqsubseteq \mathrm{MOP}\) |
| phi | x_3 \gets \phi(x_1, x_2) |
\(x_3 \gets \phi(x_1, x_2)\) |
| definitions / uses of a variable | \mathrm{defs}(v), \mathrm{uses}(v) |
\(\mathrm{defs}(v)\) |
| liveness | \mathrm{live\text{-}in}(B), \mathrm{live\text{-}out}(B) |
\(\mathrm{live\text{-}in}(B)\) |
| IR in running text | code spans: `%x = add i32 %a, %b` |
8. Complexity¶
- Always define every variable in the same section: "\(n = \lvert N \rvert\) blocks, \(e = \lvert E \rvert\) edges, \(d = d(G)\) loop connectedness".
O,\Theta,\Omegaare upright-free: \(O(e \,\alpha(e, n))\), \(\Theta(n^2)\). The inverse Ackermann function is \(\alpha(e, n)\); the context separates it from grammar strings.- State which cost: "worst-case time", "amortized", "expected", "passes", "space in words".
9. Numbered statements, algorithms, proofs¶
Formal statements are boxes (admonitions; STYLE.md §5). Numbers are N.k.m: chapter N, lesson k, and one counter m shared by all numbered kinds in the lesson, in order of appearance. ./course validate checks the format and the order.
| Box | Title format | Purpose |
|---|---|---|
!!! definition |
"Definition 15.1.1 (Dominance)" |
a term, with every symbol it uses already defined |
!!! theorem / proposition / lemma / corollary |
"Theorem 15.1.4 (Dominator tree)" |
a claim; followed by a proof box |
!!! proof |
"Proof", or "Proof sketch (full proof: [LT79, §3])" |
line-by-line argument; a sketch must say where the full proof is |
!!! algorithm |
"Algorithm 15.1.5 (Cooper–Harvey–Kennedy)" |
input, output, preconditions, postconditions, invariants + pseudo-code |
!!! notation |
free | a local abbreviation |
!!! example |
free | a small worked instance of a definition or theorem |
!!! real-world |
free | the concept in a real system, reproducible (STYLE.md §5a) |
!!! invariant |
free | a loop or data-structure invariant stated on its own |
!!! pitfall |
free | a common misconception |
Refer to a numbered result as "Theorem 15.1.4" (no link needed inside the lesson; link across lessons).
10. KaTeX compatibility¶
The website renders math with KaTeX 0.16 (vendored by ./course site build), which implements most, but not all, of LaTeX and AMS math. A macro it does not know shows up on the page as red error text. ./course validate renders every $…$ and $$…$$ in chapters/**/*.md, in the quiz prompts and choices, and in the flashcards with that KaTeX (throwOnError) and reports file:line and KaTeX's message: a warning, and an error under --strict for chapters with status: available. (It needs node; without it, or before KaTeX has been fetched once, the check is skipped with a warning.) The full list of what KaTeX supports is at https://katex.org/docs/supported.html.
Known-unsupported macros and what to write instead (each alternative was rendered with the vendored KaTeX):
| Don't write | KaTeX says | Write instead |
|---|---|---|
\bigsqcap_{p} x_p |
undefined control sequence | \mathop{\Large\sqcap}_{p} x_p (an operator, so limits go below in display math) |
\textsc{T-Add}, \text{\sc …}, \scshape |
undefined control sequence | \textsf{T-Add} (rule names), or \mathsf{…} |
\DeclareMathOperator{\lfp}{lfp}, custom \newcommand |
undefined / house rule | \mathrm{lfp} or \operatorname{lfp} inline, every time |
\begin{mathpar}, \inferrule{…}{…} (mathpartir) |
no such environment | \dfrac{premises}{conclusion} (§6), premises separated by \qquad |
\begin{align} / align* inside $…$ |
only in display mode | put it in a $$…$$ block, or use \begin{aligned}…\end{aligned} |
\tag{…}, \label, \ref, \eqref |
undefined, or display-only | number statements with boxes (§9) and refer to them in prose |
\sqcap\limits_p, \cup\limits_p |
limit controls must follow a math operator | \mathop{\sqcap}\limits_{p}, or \bigcup_{p} |
\llparenthesis, \rrparenthesis (stmaryrd) |
undefined control sequence | (\!\lvert … \rvert\!); semantic brackets \llbracket … \rrbracket are supported |
\sslash, \fatsemi, \oblong, \bigast, \bigcupdot, \lightning, \curlyveedownarrow |
undefined control sequence | describe it in words, or use a supported symbol (\mathbin{/\!/}, \mathbin{;}, \ast) |
\uline{…}, \smashoperator, \iddots, \textbackslash |
undefined control sequence | \underline{…}, plain operator, \ddots, \backslash |
Supported and fine to use (checked): \bigsqcup, \bigwedge, \bigodot, \biguplus, \llbracket, \rrbracket, \coloneqq, \triangleq, \leadsto, \rightharpoonup, \multimap, \mathscr, \mathbb, \mathfrak, \boldsymbol, \operatorname*, \xrightarrow, \overset, \substack, \begin{array}, \begin{aligned} / cases in display math, \texttt, \textsf, \textit.
Dollar signs in prose. A bare $ outside math pairs with the next $ on the page into a bogus formula. Write a literal dollar as `$` (code) or \$; in math, \$. ./course validate warns about lines with an odd number of bare $ outside code and math.