calculus/main.tex

   1 \documentclass[10pt]{article}
   2 \input{preambolo.tex}
   3
   4 % \usepackage{tikz}
   5
   6 \newcommand{\true}{\operatorname{tt}}
   7 \newcommand{\false}{\operatorname{ff}}
   8
   9 \newcommand{\ddef}{\mathrel{::=}}
  10 \newcommand{\semi}{\mathrel{;}}
  11
  12 \newtheorem{example}[theorem]{Example}
  13
  14
  15
  16 \begin{document}
  17
  18 Terms:
  19 \[t, u \ddef x \mid t\,u \mid \lambda x.\, t\]
  20
  21 Fireballs, inerts and normal forms:
  22
  23 \[\begin{array}{lll}
  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 \\
  27 \end{array}\]
  28
  29 Contexts $K$:
  30 \[K \ddef [\,] \mid i \semi K\]
  31
  32
  33 \[\begin{array}{lll}
  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
  37 \\
  38  K_1\langle\lambda x.\,t\rangle \, K_2\langle y \,\,\,\,\,\,\,\,\,\,\rangle &
  39  \mapsto_{\beta_v} &
  40  K_1\langle K_2\langle t\{x\leftarrow y\}\rangle\rangle
  41 \\
  42  K_1\langle\lambda x.\,t\rangle \, K_2\langle i\,\,\,\,\,\,\,\,\,\,\,\rangle &
  43  \mapsto_{\beta_i} &
  44  \begin{cases}
  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 &
  48   \text{ otherwise } \\
  49  \end{cases}
  50 \end{array}\]
  51
  52 Evaluation contexts $E$:
  53 \[E \ddef [\,] \mid t\,E \mid E\,t\]
  54
  55 \end{document}