\documentclass[12pt]{article}
\usepackage{blindtext}
\usepackage{enumerate}
\usepackage{hyperref, bookmark}
\usepackage{amsmath, amsfonts, amssymb, amsthm}
\usepackage{xcolor}

\title{Discrimination of Fireballs}
\author{Andrea Condoluci}

\input{macros}
\begin{document}

\maketitle

\begin{abstract}
  \ldots
\end{abstract}

\tableofcontents

\clearpage
\section{Introduction}
B\"ohm's theorem is a celebrated result of the $\lambda$-calculus,
 showing how the syntax and the reduction rules of the $\lambda$-calculus are well-matched.
Intuitively, it states that if two $\lambda$-terms are different,
  then they may behave differently when evaluated.

The original result~\cite{bohm1968alcune} concerns the vanilla $\lambda$-calculus and general $\beta\eta$-conversion,
 but it was then adapted to different evaluation strategies (\eg{} call-by-value~\cite{DBLP:conf/ictcs/Paolini01})
 and different calculi
 (\eg{} \cite{DBLP:journals/iandc/Dezani-CiancagliniTU99}, \cite{DBLP:journals/iandc/BoudolL96}, \cite{DBLP:journals/iandc/Sangiorgi94}, \ldots).

\subsection*{Outline of the report}

\section{B\"ohm's Theorem}

We define \emph{contexts} as usual, \ie{} intuitively as ``lambda-terms with a hole'':

\begin{definition}[Contexts]
 $C$ denotes an applicative context, while $C^\lambda$ is ``strong''
  (\ie{} the hole may be under lambdas):
 \[\begin{array}{ll}
    C & ::= \Box \mid t\,C \mid C\,t  \\
    C^\lambda & ::= C[\Box] \mid C[\lambda x.\, C^\lambda] \\
  \end{array}\]
\end{definition}

% \begin{definition}[Subterm]
%  $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$.
% \end{definition}

\begin{definition}[Separation]
  $t$ and $s$ are separable if there exists a context $C^\lambda$ such that:
  \[\begin{array}{rl}
    C^\lambda[t] \Downarrow \TmTrue{} & (= \lambda x\,y.\,x) \\
    C^\lambda[s] \Downarrow \TmFalse{} & (= \lambda x\,y.\,y) \\
  \end{array}\]
Note that if the terms $t$ and $s$ are closed, then a purely applicative context
 $C$ suffices in the definition above.
\end{definition}

Before stating B\"ohm's theorem, we need to define the shape of terms in $\beta$-normal form:

\begin{definition}[$\beta$-normal forms]\label{def:strong-nfs}~
  The $\lambda$-terms in normal form are described by the following grammar:
  \newcommand{\NF}{n\!f}
  \[ \NF{} \ddef \lambda x_1\cdots x_n.\, x\,\NF{}_1\cdots \NF{}_m \,\,\,(n,m\geq 0)\]
% \[\begin{array}{lllr}
%  f^s & ::= & \lambda x_1 \cdots x_n.\, i^s & \\
%  i^s & ::= & x\, f_1^s \cdots f_n^s & (n\geq 0)\\
% \end{array}\]
\end{definition}

% \newcommand{\ie}{\emph{i.e.}}
There are different ways of equating $\lambda$-terms: the most basic one is
$\alpha$-equivalence (\ie{} equivalence up-to the renaming of bound variables),
denoted by $=_\alpha$. Another useful equivalence is $\eta$-equivalence, \ie{}
equivalence up-to the expansion and reduction of ``abstractions over functions'':
\begin{definition}[$=_\eta$]
  $\eta$-equivalence is the smallest equivalence relation on $\lambda$-terms
   that is structurally closed, such that $t =_\eta \lambda x.\, t x$ for every $t$ and variable $x\not\in \operatorname{fv}(t)$.
\end{definition}

\begin{theorem}[\cite{bohm1968alcune}]
  Normal terms are pairwise either separable or $\eta$-equivalent.
\end{theorem}
% \newcommand{\Replace}[2]{\texttt{replace}^{#1}\texttt{(}#2\texttt{)}}
% \newcommand{\Rotate}[2]{\texttt{rotate}^{#1}\texttt{(}#2\texttt{)}}
\newcommand{\Replace}[2]{\texttt{replace}\texttt{(}{#1}\texttt{,}#2\texttt{)}}
\newcommand{\Select}[2]{\texttt{select}\texttt{(}{#1}\texttt{,}#2\texttt{)}}
\newcommand{\Rotate}[1]{\texttt{rotate}\texttt{(}#1\texttt{)}}

Fundamental for the proof of B\"ohm's theorem are so-called \emph{B\"ohm's transformations},
obtained by compositions of the following basic transformation operators:
\begin{itemize}
  \item $\Replace n t := \lambda x_1\cdots x_n.\, t$ (where $\vec x \# t$)
  \item (Projection) $\Select n i := \lambda x_1\cdots x_n.\, x_i$
  \item (Permutator of order $n$) $\Rotate n := \lambda x_1\cdots x_n\, x.\, x\,x_1 \ldots x_n $
\end{itemize}

\section{CBV calculi: fireballs}

\subsection{Closed (\& Weak)}
\begin{definition}[Plotkin's call-by-value]
  We denote by $\lambda_v$ the \emph{closed}, \emph{weak} call-by-value calculus
  ($\beta_v$ is its reduction rule, and $\to_v$ the reduction relation).
\end{definition}

\subsection{Open \& Weak}

We define \LambdaFire{} like in~\cite{DBLP:conf/aplas/AccattoliG16}.

\subparagraph*{Syntax}
\begin{center}\begin{tabular}{lcrl}
  Terms: & & $t,u,s,r$ & $:= x \mid v \mid t\,u$ \\
  Abstractions: & & $v$ & $:= \lambda x.\, t$ \\
  Fireballs: & & $f$ & $:= v \mid i$ \\
  Inerts: & & $i$ & $:= x\,f_1\cdots f_n$ ($n\geq 0$)\\
  Evaluation contexts: & & $E$ & $:= \Box \mid t\,E \mid E\, t$ \\
\end{tabular}\end{center}

\subparagraph*{Reduction rules}
\[\begin{array}{lcl}
  (\lambda x.\, t)\,(\lambda y.\, u) & \mapsto_{v} & t\{x\leftarrow \lambda y.\, u\} \\
  (\lambda x.\, t)\,i & \mapsto_i & t\{x\leftarrow i\} \\
\end{array}\]

The reduction $\to_f$ is obtained as usual by the closure of reduction rules under
 evaluation contexts.

\subparagraph*{Properties of \LambdaFire{}}
\begin{itemize}
  \item Open Harmony: $t$ is $f$-normal iff $t$ is a fireball;
  \item Conservative Open Extension: if $t$ is closed, $t \to_{f} u$ iff $t \to_{v} u$
\end{itemize}

\subsection{(Open \&) Strong}

\subparagraph*{Syntax}
\[\begin{array}{llcl}
  \text{Terms:} & t & \ddef & x \mid t \, t \mid v \\
  \text{Values:} & v & \ddef & \lambda x.\, A \\
  \text{Answers:} & A & \ddef & \epsilon \mid \en x t \comma A \,\,\, \text{ ($x$ variable or $*$)} \\
  % \text{:} & E & \ddef & \epsilon \mid E \comma \en x t \\
  \text{Applicative contexts:} & C & \ddef & [\cdot] \mid t \, C \mid C \, t \\
  \text{Evaluation Contexts (weak):} & E & \ddef & [\cdot] \mid A \comma \en y C \comma A \\
  \text{Evaluation Contexts (strong):} & E^s & \ddef & [\cdot] \mid A \comma \en y {C[\lambda x.\,E^s]} \comma A \\
\end{array}\]

Note: $\en \as t \comma A$ is also denoted by $t \semi A$.

\subparagraph*{Reduction rules}
\[\color{red}\begin{array}{lclc}
 C^\lambda[E \comma \en y {C[(\lambda x.\, \en {{\ast}} t \comma E')\,s]} \comma E''] & \to_m &
  C^\lambda[E \comma \en y {C[t]} \comma E' \comma \en x s \comma E''] & (*)\\
 C^\lambda[E \comma \en x v \comma E'] & \to_e &
  C^\lambda[E\{v/x\} \comma E'] & (**)\\
\end{array}\]

$\,\,(*)$ $x\#E$ and $x\#C$.

$(**)$ $x\neq\as$ (necessary only when the reduction is strong)

% \begin{theorem}[Confluency]
%   \NewSystem{} is confluent \todo{(both the weak and the strong one)}.
% \end{theorem}
% \begin{proof}
%   \begin{itemize}
%     \item $e$ vs. $e$: okay because values are closed under substitutions;
%     \item $m$ vs. $m$:
%     \item $e$ vs. $m$:
%   \end{itemize}
% \end{proof}
Note that the critical pair in \cite{DBLP:conf/aplas/AccattoliG16} does not exist anymore:
\[\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\]
\[ (\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 \]

Strong normalization and normalization do \textbf{not} coincide
 \todo{(they do if values $v$ are strong, \ie{} strong--call--by--strong--value)}.

\subparagraph*{Properties of \NewSystem{}}
 \begin{itemize}
   \item Confluent (both the weak and strong versions of the calculus).
   \item If $t \to_{???} s$, then $t\sigma \to_{???} s\sigma$.
 \end{itemize}

% \todo{Introdurre notazione semplice per termini in forma normale con garbage?}

\section{Discrimination of fireballs}
% Separating strong fireballs in the general case is not easy.

\todo{In pratica: vorremmo separazione di B-trees for fireballs, ma semplifichiamo a
B-trees con sositutzioni only}

First of all, let's relate terms in \NewSystem{} to usual $\lambda$-terms.

\begin{definition}[$\ToFire\cdot$]
  Translation from \NewSystem{}-terms to $\lambda$-terms:
  \[\begin{array}{ll}
   % \ToFire{E} & := \as\,\sigma_E \\
   \ToFire{x} & := x \\
   \ToFire{(t\,s)} & := (\ToFire{t}) \, (\ToFire{s}) \\
   \ToFire{(\lambda x.\, A)} & := \lambda x.\, (\ToFire{A}) \\
   \\
   \ToFire{\epsilon} & := \as \\
   \ToFire{(A \comma \en x t)} & := (\ToFire{A})\{x\leftarrow\ToFire{t}\} \\
   % \sigma_\epsilon & := \epsilon \\
   % \sigma_{\en x t \comma E} & := \sigma_E \cup \{x\mapsto (\ToFire{t})\sigma_E\}\\
  \end{array}\]
\end{definition}

Notes:
\begin{itemize}
  \item If $t \to_e s$ in \NewSystem{}, then $(\ToFire{t}) = (\ToFire{s})$.
  % \item {If $t \to_m s$ in \NewSystem{}, then $(\ToFire{t}) \to_\beta (\ToFire{s})$ in \LambdaFire{}.}
  % \todo{NO! It may be 0 beta steps (when on affine term) one, or infinite}
  \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'$.
  \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.
\end{itemize}

Note that -- intuitively -- $t$ usually diverges ``more'' than $\ToFire{t}$,
 because $t$ may contain additional terms in environments, that may be garbage-collected
 when doing $\ToFire\cdot$.

\paragraph{Separation in \NewSystem{}}
Let $t,s$ normal \NewSystem{}-terms. There are two cases:
\begin{enumerate}
  \item ($\not\!\!\eta$) if $(\ToFire{t}) \neq_\eta (\ToFire{s})$, then one may use an already existing
   separation algorithm for call-by-value and separate $\ToFire{t}$ from $\ToFire{s}$.
    In order to raise the separation result to \NewSystem{}, one needs to avoid
   additional divergency caused by terms in environments in $t$ and $s$.
   %(\todo{
   %intuitivamente, si possono applicare a $t,s$ termini freschi di modo che
   %i termini non siano sottotermini uno dell'altro
   %}).
  \item ($\eta$) if $(\ToFire{t}) =_\eta (\ToFire{s})$, then $t$ and $s$ cannot be separated,
   but at most \emph{semi-separated} (\todo{define!}). \todo{One needs to exploit terms in environments in $t,s$.
   The thing is that one cannot apply stuff to terms in environements,
   therefore the useful notion of separation does not use contexts but \emph{substitutions}.}
\end{enumerate}

\begin{lemma}[B\"ohm's Theorem for \NewSystem{}]
  Let $t,s$ strong normal \NewSystem{}-terms.
  $t$ and $s$ are \NewSystem{}-separable iff $\ToFire t$ and $\ToFire s$ are $f$-separable iff $\ToFire t \not=_\eta \ToFire s$.
\end{lemma}
\begin{proof}
 \todo{TODO.}
\end{proof}


\begin{lemma}[Semi-separation]
  Assume now $\ToFire t = \ToFire s$.  $t$ and $s$ are separable iff
  there is a
  \begin{verbatim}
    semi-separable iff separable OR there exists a path in the term t\downarrow

t  -pi-> u, E
t' -pi-> u', E'
and SOMEHOW E <> E'

if there is t in E not in E', and t is not seen in t' when walking pi
  \end{verbatim}
\end{lemma}

In order to tackle the problem ($\eta$) (point 2. above), first we are going to
 solve a simpler semi-separation problem, which we now call ``semi-separation with substitutions only''.

We do not work yet on \NewSystem{}-terms, but on usual normal $\lambda$-terms.

\begin{definition}[Semi-separation problem with substitutions only]\label{def:sspwso}
  A separation problem is $\langle\Delta,\nabla\rangle$ where $\Delta$ and $\nabla$ are
  sets of inerts. A solution to the problem is a substitution $\sigma$ such that
  at least one term in $\Delta\sigma$ diverges, and all terms in $\nabla\sigma$ converge.
\end{definition}

\subsection{G\"odelization algorithm}

The idea is solving a separation problem by means of ``strongly'' discriminating some of its
 subterms, \ie{} by forcing the algorithm to reduce some subterms to \emph{numerals}.

The input of the algorithm are terms in the grammar of Definition~\ref{def:strong-nfs},
 but then the algorithm works with intermediate representations of terms that include
 \emph{numerals} and \emph{matches}:

\begin{definition}[Terms]
 \[\begin{array}{ll}
  w & ::= \\
  & \mid x, y, z, \ldots \text{ (bound variables)} \\
  & \mid \alpha, \beta, \ldots \text{ (free variables)}
  \\
  t & ::=  \\
  & \mid \lambda x. \, t \mid w\, t_1 \cdots t_n \\
  & \mid \Match \alpha C \\
  & \mid \Numeral n \text{ (} n\in\mathbb{N}\text{)} \\
  % \\
  % B & ::= {\Branch {\Numeral{n_1}} {t_1}} \Sep \cdots \Sep \Branch {\Numeral{n_k}} {m_k} \\
 \end{array}\]
\end{definition}

% Convention:
% \begin{center}\begin{tabular}{ll}
%   Free variables: & $\alpha, \beta, \ldots$ \\
%   Original bound variables: & $x, y, z, \ldots$ \\
%   % Created bound variables: & $w, \ldots$ \\
% \end{tabular}\end{center}

\begin{definition}[Separation problem]
 $\SepPA{\Delta}{\nabla}{\Num}$, where:
 \begin{itemize}
  \item $\Delta$ is a term (which is required to diverge);
  \item $\nabla$ is a set of terms (which is required to converge);
  \item $\Num=\{(\alpha_1,t_1,s_1),\ldots,(\alpha_k,t_k,s_k)\}$ where
   $\alpha_i$ is the originating variable,
   $t_i$ is required to converge to different numerals,
   and $s_i$ are the branches of the match.
 \end{itemize}
\end{definition}

\begin{definition}[Solved problem]
  A problem $\SepPA{\Delta}{\nabla}{\Num}$ is \emph{solved} if:
  \begin{itemize}
    \item $\Delta \Uparrow $
    \item $\nabla \Downarrow $
    \item For every $(\alpha, t, s),(\alpha, t', s')\in\Num$,
    $t \Downarrow \Numeral n$, $t' \Downarrow \Numeral{n}'$, and $n=n'$
      iff $s = s'$.
  \end{itemize}
\end{definition}

\begin{definition}[Solution]
  A substitution $\sigma$ from free variables to strong fireballs (Definition~\ref{def:strong-nfs})
  is a solution for $\SepPA{\Delta}{\nabla}{\Num}$ if $\SepPA{\Delta\sigma}{\nabla\sigma}{\Num\sigma}$ is solved.
\end{definition}

\newcommand{\StepName}{{\normalfont\texttt{step}}}
\newcommand{\EatName}{{\normalfont\texttt{eat}}}

The algorithm works by iterating an operation which we call \StepName{},
  and finally concluding with an \EatName{}.
\begin{itemize}
 \item \StepName{}: $\sigma\colon \alpha \mapsto \Match \alpha {([\cdot] \, \alpha_1 \cdots \alpha_k)}$
  where $\vec\alpha$ are fresh variables, and $k$ is the special K.
 \item \EatName{}: $\sigma\colon \alpha \mapsto \lambda y_1\cdots y_n. \, \bot$ (\todo{where $\bot$ is the divergency, define it!})
\end{itemize}

\begin{definition}[Special K]
 Given an initial separation problem $\SepPA\Delta\nabla\emptyset$, $k$ is the
  maximum number of nested lambdas, plus one. More formally:
  % \renewcommand{\max}[2]{\operatorname{max}(#1,#2)}
  \[\begin{array}{ll}
    k(\SepPA\Delta\nabla\emptyset) & = \max {\{k(\Delta), k(\nabla) \}} \\
    k(F) & = \max {\{k(f) \mid f \in F\}} \\
    k(\lambda x_1\cdots x_n.\, i) & = \max{\{n+1, k(i)\}} \\
    k(x\,f_1\cdots f_n) & = \max{\{k(f_i) \mid 1\leq i \leq n \}} \\
   \end{array}\]
\end{definition}

The final eating can be done only if it is \emph{safe}:

\begin{definition}[Safety of eating]
  Intuitvely, eating is \emph{safe} if it cannot generate divergency.
  More formally, let $\Delta = x\,f_1\cdots f_n$: eating is safe if:
  \begin{enumerate}
    \item (Convergent) whenever
    $\nabla=C[x\,g_1\cdots g_m]$ for some $C$ and $\vec g$, $m<n$ holds.
    \item (Numerals)  \todo{complicated}
  \end{enumerate}

\end{definition}

\begin{definition}[Evaluation]~
  \begin{itemize}
    \item \todo{usual beta, todo}
    \item $C[(\Match \alpha {C'})\,t]; \Num \mapsto C[f]; \Num$  if $(\alpha,i,f)\in\Num$ with $C'[t]\Downarrow_\eta i$
    \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.
    \item $\SepPA{\Delta}{\nabla}{\Num} \to \SepPA{\Delta'}{\nabla}{\Num'}$ if $\Delta,\Num \mapsto \Delta',\Num'$
    \item $\SepPA{\Delta}{\nabla}{\Num} \to \SepPA{\Delta}{\nabla'}{\Num'}$ if $\nabla,\Num \mapsto \nabla',\Num'$
    \item $\SepPA{\Delta}{\nabla}{\Num\cup(\alpha,t,s)} \to \SepPA{\Delta}{\nabla}{\Num'\cup(\alpha,t',s)}$ if $t,\Num \mapsto t',\Num'$
    \item $\SepPA{\Delta}{\nabla}{\Num\cup(\alpha,t,s)} \to \SepPA{\Delta}{\nabla}{\Num'\cup(\alpha,t,s')}$ if $s,\Num \mapsto s',\Num'$
  \end{itemize}
\end{definition}

\todo{Precondizioni: $\Delta$ is not an eta-subterm of $\nabla$, and $\Num$ is empty}

\subsection{B\"ohm--like algorithm}
\begin{definition}[Separation problem]~

 A semi-\emph{separation problem} is a pair $\SepP\Delta\nabla$, where $\Delta$ and $\nabla$ are inerts.

 $\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}$.
\end{definition}

Steps of the algorithm:
\begin{itemize}
 \item \emph{Eat:} $x\mapsto \bot^n$ for some $n>0$
 \item \emph{Step:} $x\mapsto \lambda \vec y\,\,z.\, z\,\vec\alpha\,\vec y$ for some fresh $\vec\alpha$ and $|\vec\alpha|> 0$
\end{itemize}

\begin{lemma}
 If $\sigma$ is \ldots then $t\EtaNeq u$ implies $t\sigma \EtaNeq u\sigma$.
\end{lemma}
\begin{proof}
 By induction on the derivation of $t\EtaNeq u$:
 \begin{itemize}
  \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.
  \item $x\,\vec f \EtaNeq y\,\vec g$ and $x\neq y$:
  \item $x \, f_1\cdots f_n \EtaNeq x \, g_1\cdots g_n$ because $f_k\EtaNeq g_k$:
  \item \ldots
 \end{itemize}
\end{proof}

\begin{theorem}
 If $\Delta\not\Subtm\nabla$ and $\Delta$ not a variable, then $\SepP\Delta\nabla$ is separable.
\end{theorem}
\begin{proof} By induction on $|\SepP\Delta\nabla|$. Two cases:
 \begin{itemize}
  \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$.
  \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).

  What about the new problem $\SepP{(f_k\sigma)\vec\alpha\vec f\sigma}{\nabla\sigma}$? To prove:
  \begin{itemize}
   \item $\Delta\sigma\not\Subtm \nabla\sigma$
   \item $|\SepP{\Delta\sigma}{\nabla\sigma}|<|\SepP\Delta\nabla|$
  \end{itemize}
 \end{itemize}
\end{proof}

\begin{definition}[Trivial set of inerts]
 A set of inerts $I$ is trivial when it is empty, or it contains only variables.
\end{definition}

\begin{theorem}
 Every non-trivial set of inerts is separable.
\end{theorem}
\begin{proof}~
 \begin{itemize}
  \item Take $i\in I$ s.t. $i$ is not a subterm of any other term in $I$
  \item Solve the separation problem $\SepP{\{i\}}{I\setminus\{i\}}$
 \end{itemize}
\end{proof}

\section{Fireballs with bombs}

The goal here is separating \NewSystem{}-L\'evi-Longo trees.
 Similarly as done in the section above, let us start instead from a simpler problem:
 separating usual L\'evi-Longo trees by means of \emph{substitutions only}.

% \newcommand{\dummy}{{\#}}
\newcommand{\dummy}{\TmTrue}
\newcommand{\myfalse}{\TmFalse}
% \newcommand{\pacman}{\operatorname{P}}
\newcommand{\sep}{\cdot}

{\color{red}\begin{example}[$\eta$-differences may be invalidated by paths]
  \todo{Descrivere questo esempio e capire la sua importanza}
  \[x\, \bot^1 \, (\lambda y.\, \TmIdentity{}\comma \en{\cdot}{x\, \TmTrue\, \bot^1})\]
  \[x\, \bot^1 \, (\lambda y.\, \TmIdentity{}\comma \en{\cdot}{x\, \TmFalse\, \bot^1})\]
\end{example}}

\begin{definition}[L\'evy-Longo trees]~
 \[\begin{array}{ll}
 f & \ddef i \mid \lambda x.\, f \mid \bot\\
 i & \ddef x\, f_1 \cdots f_n \quad (n\geq 0) \\
 \end{array}\]
\end{definition}

We denote $\bot^n := \lambda\underscore{}^n.\, \bot$ ($n\geq 0$ dummy abstractions).

A semi-separation problem for this calculus may be defined similarly as in Definition~\ref{def:sspwso}.



% First note that strong fireballs with bombs cannot be always separated with substitutions in strong normal form:
%
% \begin{example} Consider the following semi-separation problem:
%
% \begin{verbatim}
% D x (_.    BOT)
% C x (_. _. BOT) t
% \end{verbatim}
%
% A separator may be $\sigma \defeq x \mapsto \lambda y.\, (y \, z \semi z)$
%
% where f is any fireball.
% \end{example}

\begin{theorem}
 Call-by-value semi-separation of L\'evy-Longo trees with substitutions only is NP-hard.
\end{theorem}
\begin{proof}
 By a reduction from \emph{graph 3-coloring}.

\newcommand{\bomb}{\operatorname{d}}

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:
 \[\begin{array}{ccccccc}
 \Uparrow & x & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \cdots & \dummy\,\dummy\,\dummy \\
 \Downarrow & x & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \cdots & t^1_n \, t^2_n \, t^3_n \\
 \vdots \\
 \Downarrow & x & \dummy\,\dummy\,\dummy & t_2^1 \, t_2^2 \, t_2^3 & \bomb\,\bomb\,\bomb\, & \cdots & \bomb\,\bomb\,\bomb\\
 \Downarrow & x & t_1^1\, t_1^2\, t_1^3 & \bomb\,\bomb\,\bomb \,& \bomb\,\bomb\,\bomb\, & \cdots & \bomb\,\bomb\,\bomb \\
 \end{array}\]

Where: $x$ is the only free variable; $\bomb := \lambda \underscore{}\underscore{}.\, \bot$; $\dummy := \lambda xy.\, x$; $\myfalse := \lambda xy. \, y$.

We now to define the terms $t_j^i$ for $i=1,2,3$ and $j=1\ldots n$.

Intuitively:
\begin{itemize}

 \item $\begin{array}{ll}
  t_1^1 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \myfalse{}\bomb\bomb \sep\bomb\ldots \\
  t_1^2 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \bomb\myfalse{}\bomb \sep\bomb\ldots \\
  t_1^3 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \bomb\bomb\myfalse{} \sep\bomb\ldots \\
 \end{array}$

 \item $t_2^1 \defeq \begin{cases}
  \lambda\underscore{}\underscore{}.\, x \sep \bomb \dummy\dummy \sep \myfalse{}\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\
  \lambda\underscore{}\underscore{}.\, x \sep \dummy\dummy\dummy \sep \myfalse{}\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\
 \end{cases}$

 \item \ldots
\end{itemize}

In order to be more formal, we first need to define an index notation:

\begin{definition}[Index notation]
 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$.
 \end{definition}

We can now define $t_j^i$:
\[t_j^i[\,_{j'}^{i'}]\defeq\begin{cases}
 \bomb & \text{if } j<j' \\
 \begin{cases}
  \bomb & \text{if } i\neq i' \\
  \myfalse{} & \text{if } i = i' \\
 \end{cases} & \text{if } j = j' \\
 \begin{cases}
  \bomb & \text{if } i = i' \\
  \dummy & \text{if } i \neq i' \\
 \end{cases} & \text{if } (v_j,v_{j'}) \in E \\
 \dummy & \text{if } (v_j,v_{j'}) \not\in E
\end{cases}\]

Intuitively, if $\sigma(x)$ ``uses'' $t_j^i$, then $\sigma$ colors the vertex $v_j$ with color $i$.

% Dimensione del problema: circa $(3\times m^2)^2$.
Size of the problem: $|t_j^i|$ is $O(n)$, therefore the size of the problem is $O(n^2)$.

% \begin{lemma}[Extraction of the coloring]
%  Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:
%
% \begin{itemize}
%  \item $\operatorname{color}(v_1) = 2$ iff
%   \[(x \sep \pacman\,\bomb\,\pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]
%  \item $\operatorname{color}(v_2) = 3$ iff:
%   \[(x \sep \dummy\,\dummy\,\dummy \sep \pacman\,\pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]
% \end{itemize}
% \end{lemma}

\end{proof}

\nocite{*}
\bibliographystyle{apalike}
\bibliography{bibliography}

\end{document}
