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{Strong Separation}\r
   9 % \author{---}\r
  10 \date{\vspace{-2em}\today{}}\r
  11 \r
  12 \input{macros}\r
  13 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
  14 \r
  15 \begin{document}\r
  16 \r
  17 \maketitle\r
  18 \r
  19 \section*{The Calculus}\r
  20 \subparagraph{Syntax}\r
  21 \[\begin{array}{lll}\r
  22   \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\\r
  23   n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\\r
  24   \\\r
  25   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
  26   P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
  27 \end{array}\]\r
  28 \r
  29 \subparagraph{Reduction rules}\r
  30 \[\begin{array}{lll}\r
  31   P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &\r
  32    P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
  33    P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &\r
  34     P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
  35 \end{array}\]\r
  36 \r
  37 \subparagraph{Properties}\r
  38 \begin{itemize}\r
  39   \item Every term is normalizing iff it is strongly normalizing.\r
  40   \item Ogni strategia e' perpetua!\r
  41   \item \ldots\r
  42 \end{itemize}\r
  43 \r
  44 \clearpage\r
  45 \section*{Separation}\r
  46 \newcommand{\HeadOf}[1]{\operatorname{head}(#1)}\r
  47 \newcommand{\FstOf}[1]{\operatorname{fst}(#1)}\r
  48 \newcommand{\DegOf}[1]{\operatorname{deg}(#1)}\r
  49 \newcommand{\SubtmOf}[2]{#1\preceq #2}\r
  50 \begin{itemize}\r
  51   % \item \textbf{$\boldsymbol\sigma$-separation.}\r
  52   %  \textcolor{red}{come definirlo? con le variabili? con i termini?\r
  53   %   problematico in cbv}\r
  54   %  Two terms are $\sigma$-separable iff there exists a substitution\r
  55   %   $\sigma$ such that \textcolor{red}{???}\r
  56   % \item \textbf{Semi-$\boldsymbol\sigma$-separation.}\r
  57   %  Two terms are semi-$\sigma$-separable iff there exists a substitution\r
  58   %   $\sigma$ such that -- in short -- it makes one diverge and the other one converge.\r
  59   % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms\r
  60    % (in deep normal form)\r
  61    \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.\r
  62    \item \textbf{Distinction:} Let $T_x \defeq \{t \preceq T \mid \HeadOf{t} = \HeadOf{D} \}$.\r
  63   Now: $C_x$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\r
  64   \begin{itemize}\r
  65     \item \emph{effective} for $D$, cioe' $\FstOf{\pi} \leq \DegOf{D}$;\r
  66     \item $\forall t\in D_x$, $t_\pi \neq \Omega$;\r
  67     \item $\exists t\in C_x$ s.t. $t \not\sim_\pi D$;\r
  68     \item $\{t\in C_x \mid t \sim_\pi D\}$ is $D$--distinct.\r
  69   \end{itemize}\r
  70 \end{itemize}\r
  71 \r
  72 \end{document}\r