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
8 \title{Discrimination of Fireballs}
\r
9 \author{Andrea Condoluci}
\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
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
34 \subsection*{Outline of the report}
\r
36 \section{B\"ohm's Theorem}
\r
38 We define \emph{contexts} as usual, \ie{} intuitively as ``lambda-terms with a hole'':
\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
44 C & ::= \Box \mid t\,C \mid C\,t \\
\r
45 C^\lambda & ::= C[\Box] \mid C[\lambda x.\, C^\lambda] \\
\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
53 \begin{definition}[Separation]
\r
54 $t$ and $s$ are separable if there exists a context $C^\lambda$ such that:
\r
56 C^\lambda[t] \Downarrow \TmTrue{} & (= \lambda x\,y.\,x) \\
\r
57 C^\lambda[s] \Downarrow \TmFalse{} & (= \lambda x\,y.\,y) \\
\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
63 Before stating B\"ohm's theorem, we need to define the shape of terms in $\beta$-normal form:
\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
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
85 \begin{theorem}[\cite{bohm1968alcune}]
\r
86 Normal terms are pairwise either separable or $\eta$-equivalent.
\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
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
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
102 \section{CBV calculi: fireballs}
\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
110 \subsection{Open \& Weak}
\r
112 We define \LambdaFire{} like in~\cite{DBLP:conf/aplas/AccattoliG16}.
\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
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
129 The reduction $\to_f$ is obtained as usual by the closure of reduction rules under
\r
130 evaluation contexts.
\r
132 \subparagraph*{Properties of \LambdaFire{}}
\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
138 \subsection{(Open \&) Strong}
\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
151 Note: $\en \as t \comma A$ is also denoted by $t \semi A$.
\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
161 $\,\,(*)$ $x\#E$ and $x\#C$.
\r
163 $(**)$ $x\neq\as$ (necessary only when the reduction is strong)
\r
165 % \begin{theorem}[Confluency]
\r
166 % \NewSystem{} is confluent \todo{(both the weak and the strong one)}.
\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
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
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
182 \subparagraph*{Properties of \NewSystem{}}
\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
188 % \todo{Introdurre notazione semplice per termini in forma normale con garbage?}
\r
190 \section{Discrimination of fireballs}
\r
191 % Separating strong fireballs in the general case is not easy.
\r
193 \todo{In pratica: vorremmo separazione di B-trees for fireballs, ma semplifichiamo a
\r
194 B-trees con sositutzioni only}
\r
196 First of all, let's relate terms in \NewSystem{} to usual $\lambda$-terms.
\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
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
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
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
226 \paragraph{Separation in \NewSystem{}}
\r
227 Let $t,s$ normal \NewSystem{}-terms. There are two cases:
\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
234 %intuitivamente, si possono applicare a $t,s$ termini freschi di modo che
\r
235 %i termini non siano sottotermini uno dell'altro
\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
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
252 \begin{lemma}[Semi-separation]
\r
253 Assume now $\ToFire t = \ToFire s$. $t$ and $s$ are separable iff
\r
256 semi-separable iff separable OR there exists a path in the term t\downarrow
\r
260 and SOMEHOW E <> E'
\r
262 if there is t in E not in E', and t is not seen in t' when walking pi
\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
269 We do not work yet on \NewSystem{}-terms, but on usual normal $\lambda$-terms.
\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
277 \subsection{G\"odelization algorithm}
\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
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
286 \begin{definition}[Terms]
\r
287 \[\begin{array}{ll}
\r
289 & \mid x, y, z, \ldots \text{ (bound variables)} \\
\r
290 & \mid \alpha, \beta, \ldots \text{ (free variables)}
\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
297 % B & ::= {\Branch {\Numeral{n_1}} {t_1}} \Sep \cdots \Sep \Branch {\Numeral{n_k}} {m_k} \\
\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
308 \begin{definition}[Separation problem]
\r
309 $\SepPA{\Delta}{\nabla}{\Num}$, where:
\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
320 \begin{definition}[Solved problem]
\r
321 A problem $\SepPA{\Delta}{\nabla}{\Num}$ is \emph{solved} if:
\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
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
336 \newcommand{\StepName}{{\normalfont\texttt{step}}}
\r
337 \newcommand{\EatName}{{\normalfont\texttt{eat}}}
\r
339 The algorithm works by iterating an operation which we call \StepName{},
\r
340 and finally concluding with an \EatName{}.
\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
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
359 The final eating can be done only if it is \emph{safe}:
\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
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
372 \begin{definition}[Evaluation]~
\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
384 \todo{Precondizioni: $\Delta$ is not an eta-subterm of $\nabla$, and $\Num$ is empty}
\r
386 \subsection{B\"ohm--like algorithm}
\r
387 \begin{definition}[Separation problem]~
\r
389 A semi-\emph{separation problem} is a pair $\SepP\Delta\nabla$, where $\Delta$ and $\nabla$ are inerts.
\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
394 Steps of the algorithm:
\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
401 If $\sigma$ is \ldots then $t\EtaNeq u$ implies $t\sigma \EtaNeq u\sigma$.
\r
404 By induction on the derivation of $t\EtaNeq u$:
\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
414 If $\Delta\not\Subtm\nabla$ and $\Delta$ not a variable, then $\SepP\Delta\nabla$ is separable.
\r
416 \begin{proof} By induction on $|\SepP\Delta\nabla|$. Two cases:
\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
421 What about the new problem $\SepP{(f_k\sigma)\vec\alpha\vec f\sigma}{\nabla\sigma}$? To prove:
\r
423 \item $\Delta\sigma\not\Subtm \nabla\sigma$
\r
424 \item $|\SepP{\Delta\sigma}{\nabla\sigma}|<|\SepP\Delta\nabla|$
\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
434 Every non-trivial set of inerts is separable.
\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
443 \section{Fireballs with bombs}
\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
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
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
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
468 We denote $\bot^n := \lambda\underscore{}^n.\, \bot$ ($n\geq 0$ dummy abstractions).
\r
470 A semi-separation problem for this calculus may be defined similarly as in Definition~\ref{def:sspwso}.
\r
474 % First note that strong fireballs with bombs cannot be always separated with substitutions in strong normal form:
\r
476 % \begin{example} Consider the following semi-separation problem:
\r
480 % C x (_. _. BOT) t
\r
483 % A separator may be $\sigma \defeq x \mapsto \lambda y.\, (y \, z \semi z)$
\r
485 % where f is any fireball.
\r
489 Call-by-value semi-separation of L\'evy-Longo trees with substitutions only is NP-hard.
\r
492 By a reduction from \emph{graph 3-coloring}.
\r
494 \newcommand{\bomb}{\operatorname{d}}
\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
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
505 Where: $x$ is the only free variable; $\bomb := \lambda \underscore{}\underscore{}.\, \bot$; $\dummy := \lambda xy.\, x$; $\myfalse := \lambda xy. \, y$.
\r
507 We now to define the terms $t_j^i$ for $i=1,2,3$ and $j=1\ldots n$.
\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
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
526 In order to be more formal, we first need to define an index notation:
\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
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
536 \bomb & \text{if } i\neq i' \\
\r
537 \myfalse{} & \text{if } i = i' \\
\r
538 \end{cases} & \text{if } j = j' \\
\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
546 Intuitively, if $\sigma(x)$ ``uses'' $t_j^i$, then $\sigma$ colors the vertex $v_j$ with color $i$.
\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
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
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
565 \bibliographystyle{apalike}
\r
566 \bibliography{bibliography}
\r