report.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{Discrimination of Fireballs}\r
   9 \author{Andrea Condoluci}\r
  10 \r
  11 \input{macros}\r
  12 \begin{document}\r
  13 \r
  14 \maketitle\r
  15 \r
  16 \begin{abstract}\r
  17   \ldots\r
  18 \end{abstract}\r
  19 \r
  20 \tableofcontents\r
  21 \r
  22 \clearpage\r
  23 \section{Introduction}\r
  24 B\"ohm's theorem is a celebrated result of the $\lambda$-calculus,\r
  25  showing how the syntax and the reduction rules of the $\lambda$-calculus are well-matched.\r
  26 Intuitively, it states that if two $\lambda$-terms are different,\r
  27   then they may behave differently when evaluated.\r
  28 \r
  29 The original result~\cite{bohm1968alcune} concerns the vanilla $\lambda$-calculus and general $\beta\eta$-conversion,\r
  30  but it was then adapted to different evaluation strategies (\eg{} call-by-value~\cite{DBLP:conf/ictcs/Paolini01})\r
  31  and different calculi\r
  32  (\eg{} \cite{DBLP:journals/iandc/Dezani-CiancagliniTU99}, \cite{DBLP:journals/iandc/BoudolL96}, \cite{DBLP:journals/iandc/Sangiorgi94}, \ldots).\r
  33 \r
  34 \subsection*{Outline of the report}\r
  35 \r
  36 \section{B\"ohm's Theorem}\r
  37 \r
  38 We define \emph{contexts} as usual, \ie{} intuitively as ``lambda-terms with a hole'':\r
  39 \r
  40 \begin{definition}[Contexts]\r
  41  $C$ denotes an applicative context, while $C^\lambda$ is ``strong''\r
  42   (\ie{} the hole may be under lambdas):\r
  43  \[\begin{array}{ll}\r
  44     C & ::= \Box \mid t\,C \mid C\,t  \\\r
  45     C^\lambda & ::= C[\Box] \mid C[\lambda x.\, C^\lambda] \\\r
  46   \end{array}\]\r
  47 \end{definition}\r
  48 \r
  49 % \begin{definition}[Subterm]\r
  50 %  $t \Subtm u$ if $t$ is an $\eta$-subterm of $u$, \ie{} $u\EtaEq C[t]$ for some $C$. $t \Subtmapp u$ if $t$ is an $\eta$-subterm of $u$ \emph{at toplevel}, \ie{} $u\EtaEq A[t]$ for some $A$.\r
  51 % \end{definition}\r
  52 \r
  53 \begin{definition}[Separation]\r
  54   $t$ and $s$ are separable if there exists a context $C^\lambda$ such that:\r
  55   \[\begin{array}{rl}\r
  56     C^\lambda[t] \Downarrow \TmTrue{} & (= \lambda x\,y.\,x) \\\r
  57     C^\lambda[s] \Downarrow \TmFalse{} & (= \lambda x\,y.\,y) \\\r
  58   \end{array}\]\r
  59 Note that if the terms $t$ and $s$ are closed, then a purely applicative context\r
  60  $C$ suffices in the definition above.\r
  61 \end{definition}\r
  62 \r
  63 Before stating B\"ohm's theorem, we need to define the shape of terms in $\beta$-normal form:\r
  64 \r
  65 \begin{definition}[$\beta$-normal forms]\label{def:strong-nfs}~\r
  66   The $\lambda$-terms in normal form are described by the following grammar:\r
  67   \newcommand{\NF}{n\!f}\r
  68   \[ \NF{} \ddef \lambda x_1\cdots x_n.\, x\,\NF{}_1\cdots \NF{}_m \,\,\,(n,m\geq 0)\]\r
  69 % \[\begin{array}{lllr}\r
  70 %  f^s & ::= & \lambda x_1 \cdots x_n.\, i^s & \\\r
  71 %  i^s & ::= & x\, f_1^s \cdots f_n^s & (n\geq 0)\\\r
  72 % \end{array}\]\r
  73 \end{definition}\r
  74 \r
  75 % \newcommand{\ie}{\emph{i.e.}}\r
  76 There are different ways of equating $\lambda$-terms: the most basic one is\r
  77 $\alpha$-equivalence (\ie{} equivalence up-to the renaming of bound variables),\r
  78 denoted by $=_\alpha$. Another useful equivalence is $\eta$-equivalence, \ie{}\r
  79 equivalence up-to the expansion and reduction of ``abstractions over functions'':\r
  80 \begin{definition}[$=_\eta$]\r
  81   $\eta$-equivalence is the smallest equivalence relation on $\lambda$-terms\r
  82    that is structurally closed, such that $t =_\eta \lambda x.\, t x$ for every $t$ and variable $x\not\in \operatorname{fv}(t)$.\r
  83 \end{definition}\r
  84 \r
  85 \begin{theorem}[\cite{bohm1968alcune}]\r
  86   Normal terms are pairwise either separable or $\eta$-equivalent.\r
  87 \end{theorem}\r
  88 % \newcommand{\Replace}[2]{\texttt{replace}^{#1}\texttt{(}#2\texttt{)}}\r
  89 % \newcommand{\Rotate}[2]{\texttt{rotate}^{#1}\texttt{(}#2\texttt{)}}\r
  90 \newcommand{\Replace}[2]{\texttt{replace}\texttt{(}{#1}\texttt{,}#2\texttt{)}}\r
  91 \newcommand{\Select}[2]{\texttt{select}\texttt{(}{#1}\texttt{,}#2\texttt{)}}\r
  92 \newcommand{\Rotate}[1]{\texttt{rotate}\texttt{(}#1\texttt{)}}\r
  93 \r
  94 Fundamental for the proof of B\"ohm's theorem are so-called \emph{B\"ohm's transformations},\r
  95 obtained by compositions of the following basic transformation operators:\r
  96 \begin{itemize}\r
  97   \item $\Replace n t := \lambda x_1\cdots x_n.\, t$ (where $\vec x \# t$)\r
  98   \item (Projection) $\Select n i := \lambda x_1\cdots x_n.\, x_i$\r
  99   \item (Permutator of order $n$) $\Rotate n := \lambda x_1\cdots x_n\, x.\, x\,x_1 \ldots x_n $\r
 100 \end{itemize}\r
 101 \r
 102 \section{CBV calculi: fireballs}\r
 103 \r
 104 \subsection{Closed (\& Weak)}\r
 105 \begin{definition}[Plotkin's call-by-value]\r
 106   We denote by $\lambda_v$ the \emph{closed}, \emph{weak} call-by-value calculus\r
 107   ($\beta_v$ is its reduction rule, and $\to_v$ the reduction relation).\r
 108 \end{definition}\r
 109 \r
 110 \subsection{Open \& Weak}\r
 111 \r
 112 We define \LambdaFire{} like in~\cite{DBLP:conf/aplas/AccattoliG16}.\r
 113 \r
 114 \subparagraph*{Syntax}\r
 115 \begin{center}\begin{tabular}{lcrl}\r
 116   Terms: & & $t,u,s,r$ & $:= x \mid v \mid t\,u$ \\\r
 117   Abstractions: & & $v$ & $:= \lambda x.\, t$ \\\r
 118   Fireballs: & & $f$ & $:= v \mid i$ \\\r
 119   Inerts: & & $i$ & $:= x\,f_1\cdots f_n$ ($n\geq 0$)\\\r
 120   Evaluation contexts: & & $E$ & $:= \Box \mid t\,E \mid E\, t$ \\\r
 121 \end{tabular}\end{center}\r
 122 \r
 123 \subparagraph*{Reduction rules}\r
 124 \[\begin{array}{lcl}\r
 125   (\lambda x.\, t)\,(\lambda y.\, u) & \mapsto_{v} & t\{x\leftarrow \lambda y.\, u\} \\\r
 126   (\lambda x.\, t)\,i & \mapsto_i & t\{x\leftarrow i\} \\\r
 127 \end{array}\]\r
 128 \r
 129 The reduction $\to_f$ is obtained as usual by the closure of reduction rules under\r
 130  evaluation contexts.\r
 131 \r
 132 \subparagraph*{Properties of \LambdaFire{}}\r
 133 \begin{itemize}\r
 134   \item Open Harmony: $t$ is $f$-normal iff $t$ is a fireball;\r
 135   \item Conservative Open Extension: if $t$ is closed, $t \to_{f} u$ iff $t \to_{v} u$\r
 136 \end{itemize}\r
 137 \r
 138 \subsection{(Open \&) Strong}\r
 139 \r
 140 \subparagraph*{Syntax}\r
 141 \[\begin{array}{llcl}\r
 142   \text{Terms:} & t & \ddef & x \mid t \, t \mid v \\\r
 143   \text{Values:} & v & \ddef & \lambda x.\, A \\\r
 144   \text{Answers:} & A & \ddef & \epsilon \mid \en x t \comma A \,\,\, \text{ ($x$ variable or $*$)} \\\r
 145   % \text{:} & E & \ddef & \epsilon \mid E \comma \en x t \\\r
 146   \text{Applicative contexts:} & C & \ddef & [\cdot] \mid t \, C \mid C \, t \\\r
 147   \text{Evaluation Contexts (weak):} & E & \ddef & [\cdot] \mid A \comma \en y C \comma A \\\r
 148   \text{Evaluation Contexts (strong):} & E^s & \ddef & [\cdot] \mid A \comma \en y {C[\lambda x.\,E^s]} \comma A \\\r
 149 \end{array}\]\r
 150 \r
 151 Note: $\en \as t \comma A$ is also denoted by $t \semi A$.\r
 152 \r
 153 \subparagraph*{Reduction rules}\r
 154 \[\color{red}\begin{array}{lclc}\r
 155  C^\lambda[E \comma \en y {C[(\lambda x.\, \en {{\ast}} t \comma E')\,s]} \comma E''] & \to_m &\r
 156   C^\lambda[E \comma \en y {C[t]} \comma E' \comma \en x s \comma E''] & (*)\\\r
 157  C^\lambda[E \comma \en x v \comma E'] & \to_e &\r
 158   C^\lambda[E\{v/x\} \comma E'] & (**)\\\r
 159 \end{array}\]\r
 160 \r
 161 $\,\,(*)$ $x\#E$ and $x\#C$.\r
 162 \r
 163 $(**)$ $x\neq\as$ (necessary only when the reduction is strong)\r
 164 \r
 165 % \begin{theorem}[Confluency]\r
 166 %   \NewSystem{} is confluent \todo{(both the weak and the strong one)}.\r
 167 % \end{theorem}\r
 168 % \begin{proof}\r
 169 %   \begin{itemize}\r
 170 %     \item $e$ vs. $e$: okay because values are closed under substitutions;\r
 171 %     \item $m$ vs. $m$:\r
 172 %     \item $e$ vs. $m$:\r
 173 %   \end{itemize}\r
 174 % \end{proof}\r
 175 Note that the critical pair in \cite{DBLP:conf/aplas/AccattoliG16} does not exist anymore:\r
 176 \[\ldots \leftarrow I\semi \en y {\delta\,\delta} \leftarrow I\semi \en y {x\,x} \comma \en x \delta \leftarrow (\lambda x.(I\semi \en y {x\,x}))\delta \leftarrow (\lambda x.(\lambda y.I)(x x))\delta\]\r
 177 \[ (\lambda x.(\lambda y.I)(x x))\delta \to (\lambda y.I)(x\,x)\semi \en x \delta \to (\lambda y.I)(\delta\,\delta) \to I \semi \en y {\delta\,\delta} \to \ldots \]\r
 178 \r
 179 Strong normalization and normalization do \textbf{not} coincide\r
 180  \todo{(they do if values $v$ are strong, \ie{} strong--call--by--strong--value)}.\r
 181 \r
 182 \subparagraph*{Properties of \NewSystem{}}\r
 183  \begin{itemize}\r
 184    \item Confluent (both the weak and strong versions of the calculus).\r
 185    \item If $t \to_{???} s$, then $t\sigma \to_{???} s\sigma$.\r
 186  \end{itemize}\r
 187 \r
 188 % \todo{Introdurre notazione semplice per termini in forma normale con garbage?}\r
 189 \r
 190 \section{Discrimination of fireballs}\r
 191 % Separating strong fireballs in the general case is not easy.\r
 192 \r
 193 \todo{In pratica: vorremmo separazione di B-trees for fireballs, ma semplifichiamo a\r
 194 B-trees con sositutzioni only}\r
 195 \r
 196 First of all, let's relate terms in \NewSystem{} to usual $\lambda$-terms.\r
 197 \r
 198 \begin{definition}[$\ToFire\cdot$]\r
 199   Translation from \NewSystem{}-terms to $\lambda$-terms:\r
 200   \[\begin{array}{ll}\r
 201    % \ToFire{E} & := \as\,\sigma_E \\\r
 202    \ToFire{x} & := x \\\r
 203    \ToFire{(t\,s)} & := (\ToFire{t}) \, (\ToFire{s}) \\\r
 204    \ToFire{(\lambda x.\, A)} & := \lambda x.\, (\ToFire{A}) \\\r
 205    \\\r
 206    \ToFire{\epsilon} & := \as \\\r
 207    \ToFire{(A \comma \en x t)} & := (\ToFire{A})\{x\leftarrow\ToFire{t}\} \\\r
 208    % \sigma_\epsilon & := \epsilon \\\r
 209    % \sigma_{\en x t \comma E} & := \sigma_E \cup \{x\mapsto (\ToFire{t})\sigma_E\}\\\r
 210   \end{array}\]\r
 211 \end{definition}\r
 212 \r
 213 Notes:\r
 214 \begin{itemize}\r
 215   \item If $t \to_e s$ in \NewSystem{}, then $(\ToFire{t}) = (\ToFire{s})$.\r
 216   % \item {If $t \to_m s$ in \NewSystem{}, then $(\ToFire{t}) \to_\beta (\ToFire{s})$ in \LambdaFire{}.}\r
 217   % \todo{NO! It may be 0 beta steps (when on affine term) one, or infinite}\r
 218   \item If $(\ToFire{t}) \to_{f} t'$ in \LambdaFire{}, then there exists $s$ s.t. $t \to_m s$ in \NewSystem{} and $\ToFire{s} = t'$.\r
 219   \item If $t$ is a weak (resp. strong) normal form in \NewSystem{}, then $\ToFire{t}$ is a fireball (resp. normal form) in the $\lambda$-calculus.\r
 220 \end{itemize}\r
 221 \r
 222 Note that -- intuitively -- $t$ usually diverges ``more'' than $\ToFire{t}$,\r
 223  because $t$ may contain additional terms in environments, that may be garbage-collected\r
 224  when doing $\ToFire\cdot$.\r
 225 \r
 226 \paragraph{Separation in \NewSystem{}}\r
 227 Let $t,s$ normal \NewSystem{}-terms. There are two cases:\r
 228 \begin{enumerate}\r
 229   \item ($\not\!\!\eta$) if $(\ToFire{t}) \neq_\eta (\ToFire{s})$, then one may use an already existing\r
 230    separation algorithm for call-by-value and separate $\ToFire{t}$ from $\ToFire{s}$.\r
 231     In order to raise the separation result to \NewSystem{}, one needs to avoid\r
 232    additional divergency caused by terms in environments in $t$ and $s$.\r
 233    %(\todo{\r
 234    %intuitivamente, si possono applicare a $t,s$ termini freschi di modo che\r
 235    %i termini non siano sottotermini uno dell'altro\r
 236    %}).\r
 237   \item ($\eta$) if $(\ToFire{t}) =_\eta (\ToFire{s})$, then $t$ and $s$ cannot be separated,\r
 238    but at most \emph{semi-separated} (\todo{define!}). \todo{One needs to exploit terms in environments in $t,s$.\r
 239    The thing is that one cannot apply stuff to terms in environements,\r
 240    therefore the useful notion of separation does not use contexts but \emph{substitutions}.}\r
 241 \end{enumerate}\r
 242 \r
 243 \begin{lemma}[B\"ohm's Theorem for \NewSystem{}]\r
 244   Let $t,s$ strong normal \NewSystem{}-terms.\r
 245   $t$ and $s$ are \NewSystem{}-separable iff $\ToFire t$ and $\ToFire s$ are $f$-separable iff $\ToFire t \not=_\eta \ToFire s$.\r
 246 \end{lemma}\r
 247 \begin{proof}\r
 248  \todo{TODO.}\r
 249 \end{proof}\r
 250 \r
 251 \r
 252 \begin{lemma}[Semi-separation]\r
 253   Assume now $\ToFire t = \ToFire s$.  $t$ and $s$ are separable iff\r
 254   there is a\r
 255   \begin{verbatim}\r
 256     semi-separable iff separable OR there exists a path in the term t\downarrow\r
 257 \r
 258 t  -pi-> u, E\r
 259 t' -pi-> u', E'\r
 260 and SOMEHOW E <> E'\r
 261 \r
 262 if there is t in E not in E', and t is not seen in t' when walking pi\r
 263   \end{verbatim}\r
 264 \end{lemma}\r
 265 \r
 266 In order to tackle the problem ($\eta$) (point 2. above), first we are going to\r
 267  solve a simpler semi-separation problem, which we now call ``semi-separation with substitutions only''.\r
 268 \r
 269 We do not work yet on \NewSystem{}-terms, but on usual normal $\lambda$-terms.\r
 270 \r
 271 \begin{definition}[Semi-separation problem with substitutions only]\label{def:sspwso}\r
 272   A separation problem is $\langle\Delta,\nabla\rangle$ where $\Delta$ and $\nabla$ are\r
 273   sets of inerts. A solution to the problem is a substitution $\sigma$ such that\r
 274   at least one term in $\Delta\sigma$ diverges, and all terms in $\nabla\sigma$ converge.\r
 275 \end{definition}\r
 276 \r
 277 \subsection{G\"odelization algorithm}\r
 278 \r
 279 The idea is solving a separation problem by means of ``strongly'' discriminating some of its\r
 280  subterms, \ie{} by forcing the algorithm to reduce some subterms to \emph{numerals}.\r
 281 \r
 282 The input of the algorithm are terms in the grammar of Definition~\ref{def:strong-nfs},\r
 283  but then the algorithm works with intermediate representations of terms that include\r
 284  \emph{numerals} and \emph{matches}:\r
 285 \r
 286 \begin{definition}[Terms]\r
 287  \[\begin{array}{ll}\r
 288   w & ::= \\\r
 289   & \mid x, y, z, \ldots \text{ (bound variables)} \\\r
 290   & \mid \alpha, \beta, \ldots \text{ (free variables)}\r
 291   \\\r
 292   t & ::=  \\\r
 293   & \mid \lambda x. \, t \mid w\, t_1 \cdots t_n \\\r
 294   & \mid \Match \alpha C \\\r
 295   & \mid \Numeral n \text{ (} n\in\mathbb{N}\text{)} \\\r
 296   % \\\r
 297   % B & ::= {\Branch {\Numeral{n_1}} {t_1}} \Sep \cdots \Sep \Branch {\Numeral{n_k}} {m_k} \\\r
 298  \end{array}\]\r
 299 \end{definition}\r
 300 \r
 301 % Convention:\r
 302 % \begin{center}\begin{tabular}{ll}\r
 303 %   Free variables: & $\alpha, \beta, \ldots$ \\\r
 304 %   Original bound variables: & $x, y, z, \ldots$ \\\r
 305 %   % Created bound variables: & $w, \ldots$ \\\r
 306 % \end{tabular}\end{center}\r
 307 \r
 308 \begin{definition}[Separation problem]\r
 309  $\SepPA{\Delta}{\nabla}{\Num}$, where:\r
 310  \begin{itemize}\r
 311   \item $\Delta$ is a term (which is required to diverge);\r
 312   \item $\nabla$ is a set of terms (which is required to converge);\r
 313   \item $\Num=\{(\alpha_1,t_1,s_1),\ldots,(\alpha_k,t_k,s_k)\}$ where\r
 314    $\alpha_i$ is the originating variable,\r
 315    $t_i$ is required to converge to different numerals,\r
 316    and $s_i$ are the branches of the match.\r
 317  \end{itemize}\r
 318 \end{definition}\r
 319 \r
 320 \begin{definition}[Solved problem]\r
 321   A problem $\SepPA{\Delta}{\nabla}{\Num}$ is \emph{solved} if:\r
 322   \begin{itemize}\r
 323     \item $\Delta \Uparrow $\r
 324     \item $\nabla \Downarrow $\r
 325     \item For every $(\alpha, t, s),(\alpha, t', s')\in\Num$,\r
 326     $t \Downarrow \Numeral n$, $t' \Downarrow \Numeral{n}'$, and $n=n'$\r
 327       iff $s = s'$.\r
 328   \end{itemize}\r
 329 \end{definition}\r
 330 \r
 331 \begin{definition}[Solution]\r
 332   A substitution $\sigma$ from free variables to strong fireballs (Definition~\ref{def:strong-nfs})\r
 333   is a solution for $\SepPA{\Delta}{\nabla}{\Num}$ if $\SepPA{\Delta\sigma}{\nabla\sigma}{\Num\sigma}$ is solved.\r
 334 \end{definition}\r
 335 \r
 336 \newcommand{\StepName}{{\normalfont\texttt{step}}}\r
 337 \newcommand{\EatName}{{\normalfont\texttt{eat}}}\r
 338 \r
 339 The algorithm works by iterating an operation which we call \StepName{},\r
 340   and finally concluding with an \EatName{}.\r
 341 \begin{itemize}\r
 342  \item \StepName{}: $\sigma\colon \alpha \mapsto \Match \alpha {([\cdot] \, \alpha_1 \cdots \alpha_k)}$\r
 343   where $\vec\alpha$ are fresh variables, and $k$ is the special K.\r
 344  \item \EatName{}: $\sigma\colon \alpha \mapsto \lambda y_1\cdots y_n. \, \bot$ (\todo{where $\bot$ is the divergency, define it!})\r
 345 \end{itemize}\r
 346 \r
 347 \begin{definition}[Special K]\r
 348  Given an initial separation problem $\SepPA\Delta\nabla\emptyset$, $k$ is the\r
 349   maximum number of nested lambdas, plus one. More formally:\r
 350   % \renewcommand{\max}[2]{\operatorname{max}(#1,#2)}\r
 351   \[\begin{array}{ll}\r
 352     k(\SepPA\Delta\nabla\emptyset) & = \max {\{k(\Delta), k(\nabla) \}} \\\r
 353     k(F) & = \max {\{k(f) \mid f \in F\}} \\\r
 354     k(\lambda x_1\cdots x_n.\, i) & = \max{\{n+1, k(i)\}} \\\r
 355     k(x\,f_1\cdots f_n) & = \max{\{k(f_i) \mid 1\leq i \leq n \}} \\\r
 356    \end{array}\]\r
 357 \end{definition}\r
 358 \r
 359 The final eating can be done only if it is \emph{safe}:\r
 360 \r
 361 \begin{definition}[Safety of eating]\r
 362   Intuitvely, eating is \emph{safe} if it cannot generate divergency.\r
 363   More formally, let $\Delta = x\,f_1\cdots f_n$: eating is safe if:\r
 364   \begin{enumerate}\r
 365     \item (Convergent) whenever\r
 366     $\nabla=C[x\,g_1\cdots g_m]$ for some $C$ and $\vec g$, $m<n$ holds.\r
 367     \item (Numerals)  \todo{complicated}\r
 368   \end{enumerate}\r
 369 \r
 370 \end{definition}\r
 371 \r
 372 \begin{definition}[Evaluation]~\r
 373   \begin{itemize}\r
 374     \item \todo{usual beta, todo}\r
 375     \item $C[(\Match \alpha {C'})\,t]; \Num \mapsto C[f]; \Num$  if $(\alpha,i,f)\in\Num$ with $C'[t]\Downarrow_\eta i$\r
 376     \item $C[(\Match \alpha {C'})\,t]; \Num \mapsto C[\alpha']; \Num, (\alpha,i,\beta)$ if $(x,i,-)\not\in\Num$ where $C'[t]\Downarrow_\eta i$ and $\beta$ fresh.\r
 377     \item $\SepPA{\Delta}{\nabla}{\Num} \to \SepPA{\Delta'}{\nabla}{\Num'}$ if $\Delta,\Num \mapsto \Delta',\Num'$\r
 378     \item $\SepPA{\Delta}{\nabla}{\Num} \to \SepPA{\Delta}{\nabla'}{\Num'}$ if $\nabla,\Num \mapsto \nabla',\Num'$\r
 379     \item $\SepPA{\Delta}{\nabla}{\Num\cup(\alpha,t,s)} \to \SepPA{\Delta}{\nabla}{\Num'\cup(\alpha,t',s)}$ if $t,\Num \mapsto t',\Num'$\r
 380     \item $\SepPA{\Delta}{\nabla}{\Num\cup(\alpha,t,s)} \to \SepPA{\Delta}{\nabla}{\Num'\cup(\alpha,t,s')}$ if $s,\Num \mapsto s',\Num'$\r
 381   \end{itemize}\r
 382 \end{definition}\r
 383 \r
 384 \todo{Precondizioni: $\Delta$ is not an eta-subterm of $\nabla$, and $\Num$ is empty}\r
 385 \r
 386 \subsection{B\"ohm--like algorithm}\r
 387 \begin{definition}[Separation problem]~\r
 388 \r
 389  A semi-\emph{separation problem} is a pair $\SepP\Delta\nabla$, where $\Delta$ and $\nabla$ are inerts.\r
 390 \r
 391  $\SepP\Delta\nabla$ is \emph{separable} if there exists a substitution $\sigma$ (called a \emph{separator}) such that $\Delta\sigma {\Uparrow}$ and $\nabla\sigma {\Downarrow}$.\r
 392 \end{definition}\r
 393 \r
 394 Steps of the algorithm:\r
 395 \begin{itemize}\r
 396  \item \emph{Eat:} $x\mapsto \bot^n$ for some $n>0$\r
 397  \item \emph{Step:} $x\mapsto \lambda \vec y\,\,z.\, z\,\vec\alpha\,\vec y$ for some fresh $\vec\alpha$ and $|\vec\alpha|> 0$\r
 398 \end{itemize}\r
 399 \r
 400 \begin{lemma}\r
 401  If $\sigma$ is \ldots then $t\EtaNeq u$ implies $t\sigma \EtaNeq u\sigma$.\r
 402 \end{lemma}\r
 403 \begin{proof}\r
 404  By induction on the derivation of $t\EtaNeq u$:\r
 405  \begin{itemize}\r
 406   \item if $\lambda \vec x.\, t \EtaNeq \lambda \vec x.\, u$, then by \ih{} $t\sigma\EtaNeq u\sigma$, $\lambda \vec x.\, t\sigma \EtaNeq \lambda \vec x.\, u\sigma$ by properties of eta, and finally $(\lambda \vec x.\, t)\sigma \EtaNeq (\lambda \vec x.\, u)\sigma$ by freshness of bound variables.\r
 407   \item $x\,\vec f \EtaNeq y\,\vec g$ and $x\neq y$:\r
 408   \item $x \, f_1\cdots f_n \EtaNeq x \, g_1\cdots g_n$ because $f_k\EtaNeq g_k$:\r
 409   \item \ldots\r
 410  \end{itemize}\r
 411 \end{proof}\r
 412 \r
 413 \begin{theorem}\r
 414  If $\Delta\not\Subtm\nabla$ and $\Delta$ not a variable, then $\SepP\Delta\nabla$ is separable.\r
 415 \end{theorem}\r
 416 \begin{proof} By induction on $|\SepP\Delta\nabla|$. Two cases:\r
 417  \begin{itemize}\r
 418   \item If $\Delta=x\,f_1\cdots f_n$, but $\nabla \not\Subtmapp x\,g_1\cdots g_n$ for no $g_1,\ldots,g_n$: eat $x\mapsto \bot^n$.\r
 419   \item Otherwise, $\nabla \EtaEq A[x\, g_1\cdots g_n]$. By the hypothesis that $\Delta$ is not a subterm of $\nabla$, there is $k$ s.t. $f_k \EtaNeq g_k $. Step with $x\mapsto \lambda \vec y \, z.\, z\,\vec\alpha\,\vec y$ with $|\vec y|=k-1$ and $|\vec\alpha|=$(numero di lambda in tutti i k-esimi argomenti di x ovunque).\r
 420 \r
 421   What about the new problem $\SepP{(f_k\sigma)\vec\alpha\vec f\sigma}{\nabla\sigma}$? To prove:\r
 422   \begin{itemize}\r
 423    \item $\Delta\sigma\not\Subtm \nabla\sigma$\r
 424    \item $|\SepP{\Delta\sigma}{\nabla\sigma}|<|\SepP\Delta\nabla|$\r
 425   \end{itemize}\r
 426  \end{itemize}\r
 427 \end{proof}\r
 428 \r
 429 \begin{definition}[Trivial set of inerts]\r
 430  A set of inerts $I$ is trivial when it is empty, or it contains only variables.\r
 431 \end{definition}\r
 432 \r
 433 \begin{theorem}\r
 434  Every non-trivial set of inerts is separable.\r
 435 \end{theorem}\r
 436 \begin{proof}~\r
 437  \begin{itemize}\r
 438   \item Take $i\in I$ s.t. $i$ is not a subterm of any other term in $I$\r
 439   \item Solve the separation problem $\SepP{\{i\}}{I\setminus\{i\}}$\r
 440  \end{itemize}\r
 441 \end{proof}\r
 442 \r
 443 \section{Fireballs with bombs}\r
 444 \r
 445 The goal here is separating \NewSystem{}-L\'evi-Longo trees.\r
 446  Similarly as done in the section above, let us start instead from a simpler problem:\r
 447  separating usual L\'evi-Longo trees by means of \emph{substitutions only}.\r
 448 \r
 449 % \newcommand{\dummy}{{\#}}\r
 450 \newcommand{\dummy}{\TmTrue}\r
 451 \newcommand{\myfalse}{\TmFalse}\r
 452 % \newcommand{\pacman}{\operatorname{P}}\r
 453 \newcommand{\sep}{\cdot}\r
 454 \r
 455 {\color{red}\begin{example}[$\eta$-differences may be invalidated by paths]\r
 456   \todo{Descrivere questo esempio e capire la sua importanza}\r
 457   \[x\, \bot^1 \, (\lambda y.\, \TmIdentity{}\comma \en{\cdot}{x\, \TmTrue\, \bot^1})\]\r
 458   \[x\, \bot^1 \, (\lambda y.\, \TmIdentity{}\comma \en{\cdot}{x\, \TmFalse\, \bot^1})\]\r
 459 \end{example}}\r
 460 \r
 461 \begin{definition}[L\'evy-Longo trees]~\r
 462  \[\begin{array}{ll}\r
 463  f & \ddef i \mid \lambda x.\, f \mid \bot\\\r
 464  i & \ddef x\, f_1 \cdots f_n \quad (n\geq 0) \\\r
 465  \end{array}\]\r
 466 \end{definition}\r
 467 \r
 468 We denote $\bot^n := \lambda\underscore{}^n.\, \bot$ ($n\geq 0$ dummy abstractions).\r
 469 \r
 470 A semi-separation problem for this calculus may be defined similarly as in Definition~\ref{def:sspwso}.\r
 471 \r
 472 \r
 473 \r
 474 % First note that strong fireballs with bombs cannot be always separated with substitutions in strong normal form:\r
 475 %\r
 476 % \begin{example} Consider the following semi-separation problem:\r
 477 %\r
 478 % \begin{verbatim}\r
 479 % D x (_.    BOT)\r
 480 % C x (_. _. BOT) t\r
 481 % \end{verbatim}\r
 482 %\r
 483 % A separator may be $\sigma \defeq x \mapsto \lambda y.\, (y \, z \semi z)$\r
 484 %\r
 485 % where f is any fireball.\r
 486 % \end{example}\r
 487 \r
 488 \begin{theorem}\r
 489  Call-by-value semi-separation of L\'evy-Longo trees with substitutions only is NP-hard.\r
 490 \end{theorem}\r
 491 \begin{proof}\r
 492  By a reduction from \emph{graph 3-coloring}.\r
 493 \r
 494 \newcommand{\bomb}{\operatorname{d}}\r
 495 \r
 496 Let $G=(V,E)$ be a graph, with $n\defeq |V|$. We encode the problem of finding a 3-coloring of $G$ in the following semi-separation problem:\r
 497  \[\begin{array}{ccccccc}\r
 498  \Uparrow & x & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \cdots & \dummy\,\dummy\,\dummy \\\r
 499  \Downarrow & x & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \cdots & t^1_n \, t^2_n \, t^3_n \\\r
 500  \vdots \\\r
 501  \Downarrow & x & \dummy\,\dummy\,\dummy & t_2^1 \, t_2^2 \, t_2^3 & \bomb\,\bomb\,\bomb\, & \cdots & \bomb\,\bomb\,\bomb\\\r
 502  \Downarrow & x & t_1^1\, t_1^2\, t_1^3 & \bomb\,\bomb\,\bomb \,& \bomb\,\bomb\,\bomb\, & \cdots & \bomb\,\bomb\,\bomb \\\r
 503  \end{array}\]\r
 504 \r
 505 Where: $x$ is the only free variable; $\bomb := \lambda \underscore{}\underscore{}.\, \bot$; $\dummy := \lambda xy.\, x$; $\myfalse := \lambda xy. \, y$.\r
 506 \r
 507 We now to define the terms $t_j^i$ for $i=1,2,3$ and $j=1\ldots n$.\r
 508 \r
 509 Intuitively:\r
 510 \begin{itemize}\r
 511 \r
 512  \item $\begin{array}{ll}\r
 513   t_1^1 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \myfalse{}\bomb\bomb \sep\bomb\ldots \\\r
 514   t_1^2 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \bomb\myfalse{}\bomb \sep\bomb\ldots \\\r
 515   t_1^3 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \bomb\bomb\myfalse{} \sep\bomb\ldots \\\r
 516  \end{array}$\r
 517 \r
 518  \item $t_2^1 \defeq \begin{cases}\r
 519   \lambda\underscore{}\underscore{}.\, x \sep \bomb \dummy\dummy \sep \myfalse{}\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\\r
 520   \lambda\underscore{}\underscore{}.\, x \sep \dummy\dummy\dummy \sep \myfalse{}\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\\r
 521  \end{cases}$\r
 522 \r
 523  \item \ldots\r
 524 \end{itemize}\r
 525 \r
 526 In order to be more formal, we first need to define an index notation:\r
 527 \r
 528 \begin{definition}[Index notation]\r
 529  Let $t = \lambda\underscore{}\underscore{}. \, x \sep s_1^1 s_1^2 s_1^3 \sep s_2^1 s_2^2 s_2^3 \sep \ldots \sep s_n^1 s_n^2 s_n^3$. We denote $t[\,_j^i] \defeq s_j^i$.\r
 530  \end{definition}\r
 531 \r
 532 We can now define $t_j^i$:\r
 533 \[t_j^i[\,_{j'}^{i'}]\defeq\begin{cases}\r
 534  \bomb & \text{if } j<j' \\\r
 535  \begin{cases}\r
 536   \bomb & \text{if } i\neq i' \\\r
 537   \myfalse{} & \text{if } i = i' \\\r
 538  \end{cases} & \text{if } j = j' \\\r
 539  \begin{cases}\r
 540   \bomb & \text{if } i = i' \\\r
 541   \dummy & \text{if } i \neq i' \\\r
 542  \end{cases} & \text{if } (v_j,v_{j'}) \in E \\\r
 543  \dummy & \text{if } (v_j,v_{j'}) \not\in E\r
 544 \end{cases}\]\r
 545 \r
 546 Intuitively, if $\sigma(x)$ ``uses'' $t_j^i$, then $\sigma$ colors the vertex $v_j$ with color $i$.\r
 547 \r
 548 % Dimensione del problema: circa $(3\times m^2)^2$.\r
 549 Size of the problem: $|t_j^i|$ is $O(n)$, therefore the size of the problem is $O(n^2)$.\r
 550 \r
 551 % \begin{lemma}[Extraction of the coloring]\r
 552 %  Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:\r
 553 %\r
 554 % \begin{itemize}\r
 555 %  \item $\operatorname{color}(v_1) = 2$ iff\r
 556 %   \[(x \sep \pacman\,\bomb\,\pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 557 %  \item $\operatorname{color}(v_2) = 3$ iff:\r
 558 %   \[(x \sep \dummy\,\dummy\,\dummy \sep \pacman\,\pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 559 % \end{itemize}\r
 560 % \end{lemma}\r
 561 \r
 562 \end{proof}\r
 563 \r
 564 \nocite{*}\r
 565 \bibliographystyle{apalike}\r
 566 \bibliography{bibliography}\r
 567 \r
 568 \end{document}\r