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 $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.\r
  63   $C_{\var}$ 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 \tm\in D_\var$, $\tm_\pi \neq \Omega$;\r
  67     \item $\exists \tm\in C_\var$ s.t. $\tm \not\sim_\pi D$;\r
  68     \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.\r
  69   \end{itemize}\r
  70 \r
  71  % \item \textbf{Unlockable variables.}\r
  72  %  We use the following contexts:\r
  73  %  $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
  74  % A variable $\var$ is \emph{unlockable} in a context $E$ if:\r
  75  %  \begin{itemize}\r
  76  %    \item it is not bound in $E$, or\r
  77  %    \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
  78  %     and $\vartwo$ is unlockable in $E'$.\r
  79  %  \end{itemize}\r
  80 \r
  81 \end{itemize}\r
  82 \r
  83 % \clearpage\r
  84 % \section*{NP-hardness}\r
  85 % \newcommand{\Pacman}{\Omega}\r
  86 % \newcommand{\sep}{\cdot}\r
  87 % \begin{example}[Graph 3-coloring]\label{example:3col}\r
  88 % Let $G=(V,E)$ be a graph, with $N \defeq |V|$.\r
  89 % We encode the problem of finding a 3-coloring of $G$ in the following problem of semi-$\sigma$-separation:\r
  90 %  \[\begin{array}{cl}\r
  91 %  \Uparrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots t_n^1\,t_n^2\,t_n^3 \\\r
  92 %  \\\r
  93 %  \Downarrow & x \sep \Pacman\,\Pacman\,\Pacman \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots t_n^1\,t_n^2\,t_n^3 \\\r
  94 %  \Downarrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep \Pacman\,\Pacman\,\Pacman \sep \cdots t_n^1\,t_n^2\,t_n^3 \\\r
  95 %  \vdots & \vdots \\\r
  96 %  \Downarrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots \Pacman\,\Pacman\,\Pacman \\\r
  97 %  \end{array}\]\r
  98 %\r
  99 % Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows:\r
 100 %\r
 101 % \begin{itemize}\r
 102 %\r
 103 %  \item $\begin{array}{ll}\r
 104 %   a_1^1 \defeq & \lambda\_. \, x \sep y\bomb\bomb \sep\bomb\ldots \\\r
 105 %   a_1^2 \defeq & \lambda\_. \, x \sep \bomb y\bomb \sep\bomb\ldots \\\r
 106 %   a_1^3 \defeq & \lambda\_. \, x \sep \bomb\bomb y \sep\bomb\ldots \\\r
 107 %  \end{array}$\r
 108 %\r
 109 %  \item $a_2^1 \defeq \begin{cases}\r
 110 %   \lambda\_.\, x \sep \bomb \dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\\r
 111 %   \lambda\_.\, x \sep \dummy\dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\\r
 112 %  \end{cases}$\r
 113 %\r
 114 %  \item \ldots\r
 115 %\r
 116 % \end{itemize}\r
 117 %\r
 118 % \begin{definition}[Index notation]\r
 119 %  Let $t = x \sep x_1^1 x_2^1 x_3^1 \sep x_1^2 x_2^2 x_3^2 \sep \ldots \sep x_1^m x_2^m x_3^m$. Then: \[t[\,_k^j] \defeq x_k^j.\]\r
 120 %  \end{definition}\r
 121 %\r
 122 % Let $z_0$, $z_1$, $z_2$ be variables.\r
 123 %\r
 124 % Define:\r
 125 % \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases}\r
 126 %  \bomb & \text{if } j<j' \\\r
 127 %  \begin{cases}\r
 128 %   \bomb & \text{if } k\neq k' \\\r
 129 %   y & \text{if } k = k' \\\r
 130 %  \end{cases} & \text{if } j = j' \\\r
 131 %  \begin{cases}\r
 132 %   \bomb & \text{if } k = k' \\\r
 133 %   \dummy & \text{if } k \neq k' \\\r
 134 %  \end{cases} & \text{if } (v_j,v_{j'}) \in E \\\r
 135 %  \dummy & \text{if } (v_j,v_{j'}) \not\in E\r
 136 % \end{cases}\]\r
 137 %\r
 138 % Attenzione! Le $a$ vanno protette da lambda ($\lambda\_$)!\r
 139 %\r
 140 % % Dimensione del problema: circa $(3\times m^2)^2$.\r
 141 %\r
 142 % Intuitively, if $\sigma(x)$ ``uses'' $a_j^i$, then $\sigma$ colors $v_j$ with color $i$.\r
 143 %\r
 144 % \begin{lemma}[Extraction of the coloring]\r
 145 %  Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:\r
 146 %\r
 147 % \begin{itemize}\r
 148 %  \item $\operatorname{color}(v_1) = 2$ iff\r
 149 %   \[(x \sep \Pacman\,\bomb\,\Pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 150 %  \item $\operatorname{color}(v_2) = 3$ iff:\r
 151 %   \[(x \sep \dummy\,\dummy\,\dummy \sep \Pacman\,\Pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 152 % \end{itemize}\r
 153 % \end{lemma}\r
 154 %\r
 155 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
 156 %\r
 157 % \end{example}\r
 158 \r
 159 \end{document}\r