ac_notes.tex

   1 \documentclass[12pt]{article}\r
   2 \usepackage{blindtext}\r
   3 \usepackage{enumerate}\r
   4 \usepackage{hyperref, bookmark}\r
   5 \usepackage{amsmath, amsfonts, amssymb, amsthm}\r
   6 \usepackage{xcolor}\r
   7 \r
   8 \title{Ideas on Strong Separation}\r
   9 \author{Anonymous}\r
  10 \r
  11 \input{macros}\r
  12 \begin{document}\r
  13 \r
  14 \maketitle\r
  15 \r
  16 \newcommand{\Prgm}[2]{[#1\Comma #2]}\r
  17 \r
  18 \subparagraph{Syntax}\r
  19 \[\begin{array}{lll}\r
  20   \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \Prgm{\tm}{\vec\tm} \\\r
  21   n & \ddef & \Lam\var \Prgm{n}{\vec n} \mid \var\,\vec n \\\r
  22   \\\r
  23   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
  24   P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
  25 \end{array}\]\r
  26 \r
  27 \subparagraph{Reduction}\r
  28 \[\begin{array}{lll}\r
  29   P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\in \Prgm\tm{\vec\tm}} &\r
  30    P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
  31    P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\Prgm\tm{\vec\tm}} &\r
  32     P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
  33 \end{array}\]\r
  34 \r
  35 \subparagraph{Properties of the calculus:}\r
  36 \begin{itemize}\r
  37   \item Every term is normalizing iff it is strongly normalizing.\r
  38   \item Ogni strategia e' perpetua!\r
  39 \end{itemize}\r
  40 \r
  41 \clearpage\r
  42 \section*{Syntactic Condition}\r
  43 \r
  44 \begin{definition}[Separable]\r
  45   Let $t$, $s$ normal terms.\r
  46 \r
  47   They are (semi?) separable iff\r
  48   there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$\r
  49   S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,\r
  50   $t'' <> s''$.\r
  51 \end{definition}\r
  52 \r
  53 An occurrence of a bound variable is usable if its head is not stuck.\r
  54 \r
  55 A head is stuck\r
  56 \r
  57 \begin{verbatim}\r
  58   Ctx[] is stuck (unappicable) if:\r
  59    - it is an application and the head variable is stuck\r
  60    - it is a garbage\r
  61    -\r
  62 \r
  63 \end{verbatim}\r
  64 \r
  65 \end{document}\r