1 \documentclass[10pt]{article}
6 \newcommand{\true}{\operatorname{tt}}
7 \newcommand{\false}{\operatorname{ff}}
9 \newcommand{\ddef}{\mathrel{::=}}
10 \newcommand{\semi}{\mathrel{;}}
12 \newtheorem{example}[theorem]{Example}
19 \[t, u \ddef x \mid t\,u \mid \lambda x.\, t\]
21 Fireballs, inerts and normal forms:
24 f & \ddef & x \mid i \mid \lambda x.\, t \\
25 i & \ddef & x\,F_1\cdots F_n \\
26 F & \ddef & K\langle f\rangle \\
30 \[K \ddef [\,] \mid i \semi K\]
34 K_1\langle\lambda x.\,t\rangle \, K_2\langle \lambda y.\, u\rangle &
35 \mapsto_{\beta_\lambda} &
36 K_1\langle K_2\langle t\{x\leftarrow \lambda y.\, u\}\rangle\rangle
38 K_1\langle\lambda x.\,t\rangle \, K_2\langle y \,\,\,\,\,\,\,\,\,\,\rangle &
40 K_1\langle K_2\langle t\{x\leftarrow y\}\rangle\rangle
42 K_1\langle\lambda x.\,t\rangle \, K_2\langle i\,\,\,\,\,\,\,\,\,\,\,\rangle &
45 K_1\langle K_2\langle t\{x\leftarrow i\}\rangle\rangle &
46 \text{ if } x \text{ occurs in } t \\
47 K_1\langle K_2\langle i \semi t\rangle\rangle &
52 Evaluation contexts $E$:
53 \[E \ddef [\,] \mid t\,E \mid E\,t\]