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 % Paths:\r
  47 \newcommand{\PathEmpty}{\epsilon}\r
  48 \newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}\r
  49 \newcommand{\PathArg}[3]{\mathtt{arg}_{#1}^{#2}(#3)}\r
  50 \newcommand{\PathHd}{\mathtt{hd}}\r
  51 \r
  52 \newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}\r
  53 \newcommand{\HeadOf}[1]{\operatorname{head}(#1)}\r
  54 \newcommand{\FstOf}[1]{\operatorname{fst}(#1)}\r
  55 \newcommand{\DegOf}[1]{\operatorname{deg}(#1)}\r
  56 \newcommand{\SubtmOf}[2]{#1\preceq #2}\r
  57 \newcommand{\OfHead}[2]{#1_{{\mid}#2}}\r
  58 \newcommand{\SubtmsOf}[1]{\operatorname{Sub}(#1)}\r
  59 \newcommand{\Div}{\mathtt{d}}\r
  60 \newcommand{\Conv}{\mathtt{c}}\r
  61 \newcommand{\Const}{\mathtt{K}}\r
  62 \newcommand{\NamedBoundVar}[1]{\texttt{bvar(}#1\texttt{)}}\r
  63 \newcommand{\AC}[1]{{\color{violet}#1}}\r
  64 \begin{itemize}\r
  65   % \item \textbf{$\boldsymbol\sigma$-separation.}\r
  66   %  \textcolor{red}{come definirlo? con le variabili? con i termini?\r
  67   %   problematico in cbv}\r
  68   %  Two terms are $\sigma$-separable iff there exists a substitution\r
  69   %   $\sigma$ such that \textcolor{red}{???}\r
  70   % \item \textbf{Semi-$\boldsymbol\sigma$-separation.}\r
  71   %  Two terms are semi-$\sigma$-separable iff there exists a substitution\r
  72   %   $\sigma$ such that -- in short -- it makes one diverge and the other one converge.\r
  73   % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms\r
  74    % (in deep normal form)\r
  75    \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.\r
  76    \item \textbf{Subterm at position $\boldsymbol\pi$:} TODO\r
  77    \item $\boldsymbol\sim_{\boldsymbol\pi}$\r
  78    \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.\r
  79   $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\r
  80   \begin{itemize}\r
  81     \item \emph{effective} for $D$, cioe' $\FstOf{\pi} \leq \DegOf{D}$;\r
  82     \item $\forall \tm\in D_\var$, $\tm_\pi \neq \Omega$;\r
  83     \item $\exists \tm\in C_\var$ s.t. $\tm \not\sim_\pi D$;\r
  84     \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.\r
  85   \end{itemize}\r
  86 \r
  87 \clearpage\r
  88   \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  89   $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  90   $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  91   \texttt{ prove di nuove definizioni di ac:}\r
  92 \r
  93   \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$\r
  94   \[\begin{array}{ll}\r
  95     \SubtmsOf{\var} & \defeq \{\var\} \\\r
  96     \SubtmsOf{\tm\,\tmtwo} & \defeq \SubtmsOf\tm \cup \SubtmsOf\tmtwo \cup \{\tm\,\tmtwo\} \\\r
  97     \SubtmsOf{\lambda \var.\, \vec\tm} & \defeq \{\tmtwo\{\Const/\var\} \mid \tmtwo \in\SubtmsOf{\vec\tm}\} \\\r
  98   \end{array}\]\r
  99   \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}\r
 100   \item \textbf{Subterm at position:}\r
 101   \[\begin{array}{ll}\r
 102     \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi\r
 103   \end{array}\]\r
 104   \AC{\r
 105    Given a path, one can retrieve from a term (if possible) the subterm at that position.\r
 106 \r
 107    Since the path may go through abstraction, bound variables that become free\r
 108    are renamed to variables of the form $\NamedBoundVar\pi$\r
 109    (where $\pi$ is the path in the original inert leading to the abstraction binding that variable).\r
 110   }\r
 111   \[\begin{array}{ll}\r
 112     \tm_\pi & \defeq \tm_\pi^{\Box} \\\r
 113     t_{\PathEmpty}^{-} & \defeq t \\\r
 114     (x\,t_1\cdots t_n)_{\PathHd}^{-} & \defeq x \\\r
 115     (x\,t_1\cdots t_n)_{\PathArg i \var \pi}^{\rho} & \defeq\r
 116       (t_i)_\pi^{\rho[\PathArg i \var \Box]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
 117     (\lambda x.\, t)_{\PathAbs \pi}^{\rho} & \defeq t_\pi^{\rho[\PathAbs\Box]} \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
 118     (t)_{\PathAbs \pi}^{\rho} & \defeq (\lambda x.\, t\, x)_{\PathAbs \pi}^{\rho} \text{ (with } x \text{ fresh) (eta)}\\\r
 119     % \Omega_-^- & \defeq \Omega \\\r
 120   \end{array}\]\r
 121   \item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$\r
 122   \item \textbf{Distinction:} \underline{$S,R$ is $\Div$--distinct} iff:\r
 123    $S$ is empty, or there exists a path $\pi$ \emph{effective} for $\{\Div\}\cup \OfHead{\GarbageOf\Div}{\HeadOf\Div}$, s.t. EITHER:\r
 124  \begin{itemize}\r
 125    \item $\forall \tm\in \OfHead{\SubtmsOf{\Div}}{\HeadOf\Div}$, $\tm_\pi$ is defined;\r
 126    % \item 1. $\exists s\in S$ s.t. $s \not\sim_\pi \Div$;\r
 127    \item $\{s\in S \mid s \sim_\pi \Div\},R$ is $\Div$--distinct.\r
 128  \end{itemize}\r
 129  OR:\r
 130 \begin{itemize}\r
 131    \item $\Div_\pi = \lambda\var.\, -, g$\r
 132     (note that $\Div$ has recursively only one garbage);\r
 133    % \item $\Div_\pi \neq \Omega$\r
 134    \item there is $\Div'\in\SubtmsOf g$ s.t.\r
 135     $S',R'$ is $\Div'$--distinct, where:\r
 136     $R'\defeq R\cup \bigcup\{\text{subtms of } s \text{ along } \pi \mid s\in S\}$ and\r
 137     $S' \defeq \OfHead{R'}{\HeadOf{\Div'}}$.\r
 138  \end{itemize}\r
 139 \r
 140  \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable\r
 141   IF $\OfHead{\SubtmsOf{\Conv}}{\HeadOf{\Div'}}, \SubtmsOf{\Conv}$ is $\Div'$--distinct for some $\Div'\in\SubtmsOf\Div$.\r
 142 \r
 143  \clearpage\r
 144  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 145  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 146  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 147 \r
 148  \item \textbf{Unlockable variables.}\r
 149   We use the following contexts:\r
 150   $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
 151  A variable $\var$ is \emph{unlockable} in a context $E$ if:\r
 152   \begin{itemize}\r
 153     \item it is not bound in $E$, or\r
 154     \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
 155      and $\vartwo$ is unlockable in $E'$.\r
 156   \end{itemize}\r
 157 \r
 158   Transformation removing an unlockable variable bound at position $\pi$:\r
 159   \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]\r
 160 \r
 161   % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}\r
 162 \r
 163 \end{itemize}\r
 164 \r
 165 % \clearpage\r
 166 % \section*{NP-hardness}\r
 167 % \newcommand{\Pacman}{\Omega}\r
 168 % \newcommand{\sep}{\cdot}\r
 169 % \begin{example}[Graph 3-coloring]\label{example:3col}\r
 170 % Let $G=(V,E)$ be a graph, with $N \defeq |V|$.\r
 171 % We encode the problem of finding a 3-coloring of $G$ in the following problem of semi-$\sigma$-separation:\r
 172 %  \[\begin{array}{cl}\r
 173 %  \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
 174 %  \\\r
 175 %  \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
 176 %  \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
 177 %  \vdots & \vdots \\\r
 178 %  \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
 179 %  \end{array}\]\r
 180 %\r
 181 % Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows:\r
 182 %\r
 183 % \begin{itemize}\r
 184 %\r
 185 %  \item $\begin{array}{ll}\r
 186 %   a_1^1 \defeq & \lambda\_. \, x \sep y\bomb\bomb \sep\bomb\ldots \\\r
 187 %   a_1^2 \defeq & \lambda\_. \, x \sep \bomb y\bomb \sep\bomb\ldots \\\r
 188 %   a_1^3 \defeq & \lambda\_. \, x \sep \bomb\bomb y \sep\bomb\ldots \\\r
 189 %  \end{array}$\r
 190 %\r
 191 %  \item $a_2^1 \defeq \begin{cases}\r
 192 %   \lambda\_.\, x \sep \bomb \dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\\r
 193 %   \lambda\_.\, x \sep \dummy\dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\\r
 194 %  \end{cases}$\r
 195 %\r
 196 %  \item \ldots\r
 197 %\r
 198 % \end{itemize}\r
 199 %\r
 200 % \begin{definition}[Index notation]\r
 201 %  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
 202 %  \end{definition}\r
 203 %\r
 204 % Let $z_0$, $z_1$, $z_2$ be variables.\r
 205 %\r
 206 % Define:\r
 207 % \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases}\r
 208 %  \bomb & \text{if } j<j' \\\r
 209 %  \begin{cases}\r
 210 %   \bomb & \text{if } k\neq k' \\\r
 211 %   y & \text{if } k = k' \\\r
 212 %  \end{cases} & \text{if } j = j' \\\r
 213 %  \begin{cases}\r
 214 %   \bomb & \text{if } k = k' \\\r
 215 %   \dummy & \text{if } k \neq k' \\\r
 216 %  \end{cases} & \text{if } (v_j,v_{j'}) \in E \\\r
 217 %  \dummy & \text{if } (v_j,v_{j'}) \not\in E\r
 218 % \end{cases}\]\r
 219 %\r
 220 % Attenzione! Le $a$ vanno protette da lambda ($\lambda\_$)!\r
 221 %\r
 222 % % Dimensione del problema: circa $(3\times m^2)^2$.\r
 223 %\r
 224 % Intuitively, if $\sigma(x)$ ``uses'' $a_j^i$, then $\sigma$ colors $v_j$ with color $i$.\r
 225 %\r
 226 % \begin{lemma}[Extraction of the coloring]\r
 227 %  Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:\r
 228 %\r
 229 % \begin{itemize}\r
 230 %  \item $\operatorname{color}(v_1) = 2$ iff\r
 231 %   \[(x \sep \Pacman\,\bomb\,\Pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 232 %  \item $\operatorname{color}(v_2) = 3$ iff:\r
 233 %   \[(x \sep \dummy\,\dummy\,\dummy \sep \Pacman\,\Pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 234 % \end{itemize}\r
 235 % \end{lemma}\r
 236 %\r
 237 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
 238 %\r
 239 % \end{example}\r
 240 \r
 241 \end{document}\r