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 \subparagraph{Syntax}\r
  17 \[\begin{array}{lll}\r
  18   \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\\r
  19   n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\\r
  20   \\\r
  21   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
  22   P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm  \\\r
  23   \tilde P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
  24 \end{array}\]\r
  25 \r
  26 \subparagraph{Reduction}\r
  27 \[\begin{array}{lll}\r
  28   P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} &\r
  29    P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\\r
  30    P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} &\r
  31     P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\\r
  32 \end{array}\]\r
  33 \r
  34 \subparagraph{Properties of the calculus:}\r
  35 \begin{itemize}\r
  36   \item Every term is normalizing iff it is strongly normalizing.\r
  37 \end{itemize}\r
  38 \r
  39 \clearpage\r
  40 \section*{Syntactic Condition}\r
  41 \r
  42 \begin{definition}[Separable]\r
  43   Let $t$, $s$ normal terms.\r
  44 \r
  45   They are (semi?) separable iff\r
  46   there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$\r
  47   S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,\r
  48   $t'' <> s''$.\r
  49 \end{definition}\r
  50 \r
  51 An occurrence of a bound variable is usable if its head is not stuck.\r
  52 \r
  53 A head is stuck\r
  54 \r
  55 \begin{verbatim}\r
  56   Ctx[] is stuck (unappicable) if:\r
  57    - it is an application and the head variable is stuck\r
  58    - it is a garbage\r
  59    -\r
  60 \r
  61 \end{verbatim}\r
  62 \r
  63 \end{document}\r