--- /dev/null
+@inproceedings{DBLP:conf/aplas/AccattoliG16,\r
+ author = {Beniamino Accattoli and\r
+ Giulio Guerrieri},\r
+ title = {Open Call-by-Value},\r
+ booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS}\r
+ 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},\r
+ pages = {206--226},\r
+ year = {2016},\r
+ crossref = {DBLP:conf/aplas/2016},\r
+ url = {https://doi.org/10.1007/978-3-319-47958-3_12},\r
+ doi = {10.1007/978-3-319-47958-3_12},\r
+ timestamp = {Fri, 19 May 2017 01:25:54 +0200},\r
+ biburl = {https://dblp.org/rec/bib/conf/aplas/AccattoliG16},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
+@proceedings{DBLP:conf/aplas/2016,\r
+ editor = {Atsushi Igarashi},\r
+ title = {Programming Languages and Systems - 14th Asian Symposium, {APLAS}\r
+ 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},\r
+ series = {Lecture Notes in Computer Science},\r
+ volume = {10017},\r
+ year = {2016},\r
+ url = {https://doi.org/10.1007/978-3-319-47958-3},\r
+ doi = {10.1007/978-3-319-47958-3},\r
+ isbn = {978-3-319-47957-6},\r
+ timestamp = {Fri, 19 May 2017 01:25:54 +0200},\r
+ biburl = {https://dblp.org/rec/bib/conf/aplas/2016},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
+\r
+@article{bohm1968alcune,\r
+ title={Alcune proprieta delle forme $\beta$-$\eta$-normali nel $\lambda$-K-calcolo},\r
+ author={B{\"o}hm, Corrado},\r
+ journal={Pubblicazioni dell’Istituto per le Applicazioni del Calcolo},\r
+ volume={696},\r
+ pages={19},\r
+ year={1968}\r
+}\r
+\r
+@inproceedings{DBLP:conf/ictcs/Paolini01,\r
+ author = {Luca Paolini},\r
+ title = {Call-by-Value Separability and Computability},\r
+ booktitle = {Theoretical Computer Science, 7th Italian Conference, {ICTCS} 2001,\r
+ Torino, Italy, October 4-6, 2001, Proceedings},\r
+ pages = {74--89},\r
+ year = {2001},\r
+ crossref = {DBLP:conf/ictcs/2001},\r
+ url = {https://doi.org/10.1007/3-540-45446-2_5},\r
+ doi = {10.1007/3-540-45446-2_5},\r
+ timestamp = {Sun, 04 Jun 2017 10:10:18 +0200},\r
+ biburl = {https://dblp.org/rec/bib/conf/ictcs/Paolini01},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
+@proceedings{DBLP:conf/ictcs/2001,\r
+ editor = {Antonio Restivo and\r
+ Simona Ronchi Della Rocca and\r
+ Luca Roversi},\r
+ title = {Theoretical Computer Science, 7th Italian Conference, {ICTCS} 2001,\r
+ Torino, Italy, October 4-6, 2001, Proceedings},\r
+ series = {Lecture Notes in Computer Science},\r
+ volume = {2202},\r
+ publisher = {Springer},\r
+ year = {2001},\r
+ url = {https://doi.org/10.1007/3-540-45446-2},\r
+ doi = {10.1007/3-540-45446-2},\r
+ isbn = {3-540-42672-8},\r
+ timestamp = {Fri, 26 May 2017 14:09:15 +0200},\r
+ biburl = {https://dblp.org/rec/bib/conf/ictcs/2001},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
+\r
+@article{DBLP:journals/iandc/BoudolL96,\r
+ author = {G{\'{e}}rard Boudol and\r
+ Cosimo Laneve},\r
+ title = {The Discriminating Power of Multiplicities in the Lambda-Calculus},\r
+ journal = {Inf. Comput.},\r
+ volume = {126},\r
+ number = {1},\r
+ pages = {83--102},\r
+ year = {1996},\r
+ url = {https://doi.org/10.1006/inco.1996.0037},\r
+ doi = {10.1006/inco.1996.0037},\r
+ timestamp = {Thu, 18 May 2017 09:54:15 +0200},\r
+ biburl = {https://dblp.org/rec/bib/journals/iandc/BoudolL96},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
+\r
+@article{DBLP:journals/iandc/Sangiorgi94,\r
+ author = {Davide Sangiorgi},\r
+ title = {The Lazy Lambda Calculus in a Concurrency Scenario},\r
+ journal = {Inf. Comput.},\r
+ volume = {111},\r
+ number = {1},\r
+ pages = {120--153},\r
+ year = {1994},\r
+ url = {https://doi.org/10.1006/inco.1994.1042},\r
+ doi = {10.1006/inco.1994.1042},\r
+ timestamp = {Thu, 18 May 2017 09:54:16 +0200},\r
+ biburl = {https://dblp.org/rec/bib/journals/iandc/Sangiorgi94},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
+\r
+@article{DBLP:journals/iandc/Dezani-CiancagliniTU99,\r
+ author = {Mariangiola Dezani{-}Ciancaglini and\r
+ Jerzy Tiuryn and\r
+ Pawel Urzyczyn},\r
+ title = {Discrimination by Parallel Observers: The Algorithm},\r
+ journal = {Inf. Comput.},\r
+ volume = {150},\r
+ number = {2},\r
+ pages = {153--186},\r
+ year = {1999},\r
+ url = {https://doi.org/10.1006/inco.1998.2773},\r
+ doi = {10.1006/inco.1998.2773},\r
+ timestamp = {Thu, 18 May 2017 09:54:15 +0200},\r
+ biburl = {https://dblp.org/rec/bib/journals/iandc/Dezani-CiancagliniTU99},\r
+ bibsource = {dblp computer science bibliography, https://dblp.org}\r
+}\r
--- /dev/null
+\documentclass[12pt]{article}\r
+\usepackage{blindtext}\r
+\usepackage{enumerate}\r
+\usepackage{hyperref, bookmark}\r
+\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
+\usepackage{xcolor}\r
+\r
+\title{Discrimination of Fireballs}\r
+\author{Andrea Condoluci}\r
+\r
+\input{macros}\r
+\begin{document}\r
+\r
+\maketitle\r
+\r
+\begin{abstract}\r
+ \ldots\r
+\end{abstract}\r
+\r
+\tableofcontents\r
+\r
+\clearpage\r
+\section{Introduction}\r
+B\"ohm's theorem is a celebrated result of the $\lambda$-calculus,\r
+ showing how the syntax and the reduction rules of the $\lambda$-calculus are well-matched.\r
+Intuitively, it states that if two $\lambda$-terms are different,\r
+ then they may behave differently when evaluated.\r
+\r
+The original result~\cite{bohm1968alcune} concerns the vanilla $\lambda$-calculus and general $\beta\eta$-conversion,\r
+ but it was then adapted to different evaluation strategies (\eg{} call-by-value~\cite{DBLP:conf/ictcs/Paolini01})\r
+ and different calculi\r
+ (\eg{} \cite{DBLP:journals/iandc/Dezani-CiancagliniTU99}, \cite{DBLP:journals/iandc/BoudolL96}, \cite{DBLP:journals/iandc/Sangiorgi94}, \ldots).\r
+\r
+\subsection*{Outline of the report}\r
+\r
+\section{B\"ohm's Theorem}\r
+\r
+We define \emph{contexts} as usual, \ie{} intuitively as ``lambda-terms with a hole'':\r
+\r
+\begin{definition}[Contexts]\r
+ $C$ denotes an applicative context, while $C^\lambda$ is ``strong''\r
+ (\ie{} the hole may be under lambdas):\r
+ \[\begin{array}{ll}\r
+ C & ::= \Box \mid t\,C \mid C\,t \\\r
+ C^\lambda & ::= C[\Box] \mid C[\lambda x.\, C^\lambda] \\\r
+ \end{array}\]\r
+\end{definition}\r
+\r
+% \begin{definition}[Subterm]\r
+% $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
+% \end{definition}\r
+\r
+\begin{definition}[Separation]\r
+ $t$ and $s$ are separable if there exists a context $C^\lambda$ such that:\r
+ \[\begin{array}{rl}\r
+ C^\lambda[t] \Downarrow \TmTrue{} & (= \lambda x\,y.\,x) \\\r
+ C^\lambda[s] \Downarrow \TmFalse{} & (= \lambda x\,y.\,y) \\\r
+ \end{array}\]\r
+Note that if the terms $t$ and $s$ are closed, then a purely applicative context\r
+ $C$ suffices in the definition above.\r
+\end{definition}\r
+\r
+Before stating B\"ohm's theorem, we need to define the shape of terms in $\beta$-normal form:\r
+\r
+\begin{definition}[$\beta$-normal forms]\label{def:strong-nfs}~\r
+ The $\lambda$-terms in normal form are described by the following grammar:\r
+ \newcommand{\NF}{n\!f}\r
+ \[ \NF{} \ddef \lambda x_1\cdots x_n.\, x\,\NF{}_1\cdots \NF{}_m \,\,\,(n,m\geq 0)\]\r
+% \[\begin{array}{lllr}\r
+% f^s & ::= & \lambda x_1 \cdots x_n.\, i^s & \\\r
+% i^s & ::= & x\, f_1^s \cdots f_n^s & (n\geq 0)\\\r
+% \end{array}\]\r
+\end{definition}\r
+\r
+% \newcommand{\ie}{\emph{i.e.}}\r
+There are different ways of equating $\lambda$-terms: the most basic one is\r
+$\alpha$-equivalence (\ie{} equivalence up-to the renaming of bound variables),\r
+denoted by $=_\alpha$. Another useful equivalence is $\eta$-equivalence, \ie{}\r
+equivalence up-to the expansion and reduction of ``abstractions over functions'':\r
+\begin{definition}[$=_\eta$]\r
+ $\eta$-equivalence is the smallest equivalence relation on $\lambda$-terms\r
+ that is structurally closed, such that $t =_\eta \lambda x.\, t x$ for every $t$ and variable $x\not\in \operatorname{fv}(t)$.\r
+\end{definition}\r
+\r
+\begin{theorem}[\cite{bohm1968alcune}]\r
+ Normal terms are pairwise either separable or $\eta$-equivalent.\r
+\end{theorem}\r
+% \newcommand{\Replace}[2]{\texttt{replace}^{#1}\texttt{(}#2\texttt{)}}\r
+% \newcommand{\Rotate}[2]{\texttt{rotate}^{#1}\texttt{(}#2\texttt{)}}\r
+\newcommand{\Replace}[2]{\texttt{replace}\texttt{(}{#1}\texttt{,}#2\texttt{)}}\r
+\newcommand{\Select}[2]{\texttt{select}\texttt{(}{#1}\texttt{,}#2\texttt{)}}\r
+\newcommand{\Rotate}[1]{\texttt{rotate}\texttt{(}#1\texttt{)}}\r
+\r
+Fundamental for the proof of B\"ohm's theorem are so-called \emph{B\"ohm's transformations},\r
+obtained by compositions of the following basic transformation operators:\r
+\begin{itemize}\r
+ \item $\Replace n t := \lambda x_1\cdots x_n.\, t$ (where $\vec x \# t$)\r
+ \item (Projection) $\Select n i := \lambda x_1\cdots x_n.\, x_i$\r
+ \item (Permutator of order $n$) $\Rotate n := \lambda x_1\cdots x_n\, x.\, x\,x_1 \ldots x_n $\r
+\end{itemize}\r
+\r
+\section{CBV calculi: fireballs}\r
+\r
+\subsection{Closed (\& Weak)}\r
+\begin{definition}[Plotkin's call-by-value]\r
+ We denote by $\lambda_v$ the \emph{closed}, \emph{weak} call-by-value calculus\r
+ ($\beta_v$ is its reduction rule, and $\to_v$ the reduction relation).\r
+\end{definition}\r
+\r
+\subsection{Open \& Weak}\r
+\r
+We define \LambdaFire{} like in~\cite{DBLP:conf/aplas/AccattoliG16}.\r
+\r
+\subparagraph*{Syntax}\r
+\begin{center}\begin{tabular}{lcrl}\r
+ Terms: & & $t,u,s,r$ & $:= x \mid v \mid t\,u$ \\\r
+ Abstractions: & & $v$ & $:= \lambda x.\, t$ \\\r
+ Fireballs: & & $f$ & $:= v \mid i$ \\\r
+ Inerts: & & $i$ & $:= x\,f_1\cdots f_n$ ($n\geq 0$)\\\r
+ Evaluation contexts: & & $E$ & $:= \Box \mid t\,E \mid E\, t$ \\\r
+\end{tabular}\end{center}\r
+\r
+\subparagraph*{Reduction rules}\r
+\[\begin{array}{lcl}\r
+ (\lambda x.\, t)\,(\lambda y.\, u) & \mapsto_{v} & t\{x\leftarrow \lambda y.\, u\} \\\r
+ (\lambda x.\, t)\,i & \mapsto_i & t\{x\leftarrow i\} \\\r
+\end{array}\]\r
+\r
+The reduction $\to_f$ is obtained as usual by the closure of reduction rules under\r
+ evaluation contexts.\r
+\r
+\subparagraph*{Properties of \LambdaFire{}}\r
+\begin{itemize}\r
+ \item Open Harmony: $t$ is $f$-normal iff $t$ is a fireball;\r
+ \item Conservative Open Extension: if $t$ is closed, $t \to_{f} u$ iff $t \to_{v} u$\r
+\end{itemize}\r
+\r
+\subsection{(Open \&) Strong}\r
+\r
+\subparagraph*{Syntax}\r
+\[\begin{array}{llcl}\r
+ \text{Terms:} & t & \ddef & x \mid t \, t \mid v \\\r
+ \text{Values:} & v & \ddef & \lambda x.\, A \\\r
+ \text{Answers:} & A & \ddef & \epsilon \mid \en x t \comma A \,\,\, \text{ ($x$ variable or $*$)} \\\r
+ % \text{:} & E & \ddef & \epsilon \mid E \comma \en x t \\\r
+ \text{Applicative contexts:} & C & \ddef & [\cdot] \mid t \, C \mid C \, t \\\r
+ \text{Evaluation Contexts (weak):} & E & \ddef & [\cdot] \mid A \comma \en y C \comma A \\\r
+ \text{Evaluation Contexts (strong):} & E^s & \ddef & [\cdot] \mid A \comma \en y {C[\lambda x.\,E^s]} \comma A \\\r
+\end{array}\]\r
+\r
+Note: $\en \as t \comma A$ is also denoted by $t \semi A$.\r
+\r
+\subparagraph*{Reduction rules}\r
+\[\color{red}\begin{array}{lclc}\r
+ C^\lambda[E \comma \en y {C[(\lambda x.\, \en {{\ast}} t \comma E')\,s]} \comma E''] & \to_m &\r
+ C^\lambda[E \comma \en y {C[t]} \comma E' \comma \en x s \comma E''] & (*)\\\r
+ C^\lambda[E \comma \en x v \comma E'] & \to_e &\r
+ C^\lambda[E\{v/x\} \comma E'] & (**)\\\r
+\end{array}\]\r
+\r
+$\,\,(*)$ $x\#E$ and $x\#C$.\r
+\r
+$(**)$ $x\neq\as$ (necessary only when the reduction is strong)\r
+\r
+% \begin{theorem}[Confluency]\r
+% \NewSystem{} is confluent \todo{(both the weak and the strong one)}.\r
+% \end{theorem}\r
+% \begin{proof}\r
+% \begin{itemize}\r
+% \item $e$ vs. $e$: okay because values are closed under substitutions;\r
+% \item $m$ vs. $m$:\r
+% \item $e$ vs. $m$:\r
+% \end{itemize}\r
+% \end{proof}\r
+Note that the critical pair in \cite{DBLP:conf/aplas/AccattoliG16} does not exist anymore:\r
+\[\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
+\[ (\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
+\r
+Strong normalization and normalization do \textbf{not} coincide\r
+ \todo{(they do if values $v$ are strong, \ie{} strong--call--by--strong--value)}.\r
+\r
+\subparagraph*{Properties of \NewSystem{}}\r
+ \begin{itemize}\r
+ \item Confluent (both the weak and strong versions of the calculus).\r
+ \item If $t \to_{???} s$, then $t\sigma \to_{???} s\sigma$.\r
+ \end{itemize}\r
+\r
+% \todo{Introdurre notazione semplice per termini in forma normale con garbage?}\r
+\r
+\section{Discrimination of fireballs}\r
+% Separating strong fireballs in the general case is not easy.\r
+\r
+\todo{In pratica: vorremmo separazione di B-trees for fireballs, ma semplifichiamo a\r
+B-trees con sositutzioni only}\r
+\r
+First of all, let's relate terms in \NewSystem{} to usual $\lambda$-terms.\r
+\r
+\begin{definition}[$\ToFire\cdot$]\r
+ Translation from \NewSystem{}-terms to $\lambda$-terms:\r
+ \[\begin{array}{ll}\r
+ % \ToFire{E} & := \as\,\sigma_E \\\r
+ \ToFire{x} & := x \\\r
+ \ToFire{(t\,s)} & := (\ToFire{t}) \, (\ToFire{s}) \\\r
+ \ToFire{(\lambda x.\, A)} & := \lambda x.\, (\ToFire{A}) \\\r
+ \\\r
+ \ToFire{\epsilon} & := \as \\\r
+ \ToFire{(A \comma \en x t)} & := (\ToFire{A})\{x\leftarrow\ToFire{t}\} \\\r
+ % \sigma_\epsilon & := \epsilon \\\r
+ % \sigma_{\en x t \comma E} & := \sigma_E \cup \{x\mapsto (\ToFire{t})\sigma_E\}\\\r
+ \end{array}\]\r
+\end{definition}\r
+\r
+Notes:\r
+\begin{itemize}\r
+ \item If $t \to_e s$ in \NewSystem{}, then $(\ToFire{t}) = (\ToFire{s})$.\r
+ % \item {If $t \to_m s$ in \NewSystem{}, then $(\ToFire{t}) \to_\beta (\ToFire{s})$ in \LambdaFire{}.}\r
+ % \todo{NO! It may be 0 beta steps (when on affine term) one, or infinite}\r
+ \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
+ \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
+\end{itemize}\r
+\r
+Note that -- intuitively -- $t$ usually diverges ``more'' than $\ToFire{t}$,\r
+ because $t$ may contain additional terms in environments, that may be garbage-collected\r
+ when doing $\ToFire\cdot$.\r
+\r
+\paragraph{Separation in \NewSystem{}}\r
+Let $t,s$ normal \NewSystem{}-terms. There are two cases:\r
+\begin{enumerate}\r
+ \item ($\not\!\!\eta$) if $(\ToFire{t}) \neq_\eta (\ToFire{s})$, then one may use an already existing\r
+ separation algorithm for call-by-value and separate $\ToFire{t}$ from $\ToFire{s}$.\r
+ In order to raise the separation result to \NewSystem{}, one needs to avoid\r
+ additional divergency caused by terms in environments in $t$ and $s$.\r
+ %(\todo{\r
+ %intuitivamente, si possono applicare a $t,s$ termini freschi di modo che\r
+ %i termini non siano sottotermini uno dell'altro\r
+ %}).\r
+ \item ($\eta$) if $(\ToFire{t}) =_\eta (\ToFire{s})$, then $t$ and $s$ cannot be separated,\r
+ but at most \emph{semi-separated} (\todo{define!}). \todo{One needs to exploit terms in environments in $t,s$.\r
+ The thing is that one cannot apply stuff to terms in environements,\r
+ therefore the useful notion of separation does not use contexts but \emph{substitutions}.}\r
+\end{enumerate}\r
+\r
+\begin{lemma}[B\"ohm's Theorem for \NewSystem{}]\r
+ Let $t,s$ strong normal \NewSystem{}-terms.\r
+ $t$ and $s$ are \NewSystem{}-separable iff $\ToFire t$ and $\ToFire s$ are $f$-separable iff $\ToFire t \not=_\eta \ToFire s$.\r
+\end{lemma}\r
+\begin{proof}\r
+ \todo{TODO.}\r
+\end{proof}\r
+\r
+\r
+\begin{lemma}[Semi-separation]\r
+ Assume now $\ToFire t = \ToFire s$. $t$ and $s$ are separable iff\r
+ there is a\r
+ \begin{verbatim}\r
+ semi-separable iff separable OR there exists a path in the term t\downarrow\r
+\r
+t -pi-> u, E\r
+t' -pi-> u', E'\r
+and SOMEHOW E <> E'\r
+\r
+if there is t in E not in E', and t is not seen in t' when walking pi\r
+ \end{verbatim}\r
+\end{lemma}\r
+\r
+In order to tackle the problem ($\eta$) (point 2. above), first we are going to\r
+ solve a simpler semi-separation problem, which we now call ``semi-separation with substitutions only''.\r
+\r
+We do not work yet on \NewSystem{}-terms, but on usual normal $\lambda$-terms.\r
+\r
+\begin{definition}[Semi-separation problem with substitutions only]\label{def:sspwso}\r
+ A separation problem is $\langle\Delta,\nabla\rangle$ where $\Delta$ and $\nabla$ are\r
+ sets of inerts. A solution to the problem is a substitution $\sigma$ such that\r
+ at least one term in $\Delta\sigma$ diverges, and all terms in $\nabla\sigma$ converge.\r
+\end{definition}\r
+\r
+\subsection{G\"odelization algorithm}\r
+\r
+The idea is solving a separation problem by means of ``strongly'' discriminating some of its\r
+ subterms, \ie{} by forcing the algorithm to reduce some subterms to \emph{numerals}.\r
+\r
+The input of the algorithm are terms in the grammar of Definition~\ref{def:strong-nfs},\r
+ but then the algorithm works with intermediate representations of terms that include\r
+ \emph{numerals} and \emph{matches}:\r
+\r
+\begin{definition}[Terms]\r
+ \[\begin{array}{ll}\r
+ w & ::= \\\r
+ & \mid x, y, z, \ldots \text{ (bound variables)} \\\r
+ & \mid \alpha, \beta, \ldots \text{ (free variables)}\r
+ \\\r
+ t & ::= \\\r
+ & \mid \lambda x. \, t \mid w\, t_1 \cdots t_n \\\r
+ & \mid \Match \alpha C \\\r
+ & \mid \Numeral n \text{ (} n\in\mathbb{N}\text{)} \\\r
+ % \\\r
+ % B & ::= {\Branch {\Numeral{n_1}} {t_1}} \Sep \cdots \Sep \Branch {\Numeral{n_k}} {m_k} \\\r
+ \end{array}\]\r
+\end{definition}\r
+\r
+% Convention:\r
+% \begin{center}\begin{tabular}{ll}\r
+% Free variables: & $\alpha, \beta, \ldots$ \\\r
+% Original bound variables: & $x, y, z, \ldots$ \\\r
+% % Created bound variables: & $w, \ldots$ \\\r
+% \end{tabular}\end{center}\r
+\r
+\begin{definition}[Separation problem]\r
+ $\SepPA{\Delta}{\nabla}{\Num}$, where:\r
+ \begin{itemize}\r
+ \item $\Delta$ is a term (which is required to diverge);\r
+ \item $\nabla$ is a set of terms (which is required to converge);\r
+ \item $\Num=\{(\alpha_1,t_1,s_1),\ldots,(\alpha_k,t_k,s_k)\}$ where\r
+ $\alpha_i$ is the originating variable,\r
+ $t_i$ is required to converge to different numerals,\r
+ and $s_i$ are the branches of the match.\r
+ \end{itemize}\r
+\end{definition}\r
+\r
+\begin{definition}[Solved problem]\r
+ A problem $\SepPA{\Delta}{\nabla}{\Num}$ is \emph{solved} if:\r
+ \begin{itemize}\r
+ \item $\Delta \Uparrow $\r
+ \item $\nabla \Downarrow $\r
+ \item For every $(\alpha, t, s),(\alpha, t', s')\in\Num$,\r
+ $t \Downarrow \Numeral n$, $t' \Downarrow \Numeral{n}'$, and $n=n'$\r
+ iff $s = s'$.\r
+ \end{itemize}\r
+\end{definition}\r
+\r
+\begin{definition}[Solution]\r
+ A substitution $\sigma$ from free variables to strong fireballs (Definition~\ref{def:strong-nfs})\r
+ is a solution for $\SepPA{\Delta}{\nabla}{\Num}$ if $\SepPA{\Delta\sigma}{\nabla\sigma}{\Num\sigma}$ is solved.\r
+\end{definition}\r
+\r
+\newcommand{\StepName}{{\normalfont\texttt{step}}}\r
+\newcommand{\EatName}{{\normalfont\texttt{eat}}}\r
+\r
+The algorithm works by iterating an operation which we call \StepName{},\r
+ and finally concluding with an \EatName{}.\r
+\begin{itemize}\r
+ \item \StepName{}: $\sigma\colon \alpha \mapsto \Match \alpha {([\cdot] \, \alpha_1 \cdots \alpha_k)}$\r
+ where $\vec\alpha$ are fresh variables, and $k$ is the special K.\r
+ \item \EatName{}: $\sigma\colon \alpha \mapsto \lambda y_1\cdots y_n. \, \bot$ (\todo{where $\bot$ is the divergency, define it!})\r
+\end{itemize}\r
+\r
+\begin{definition}[Special K]\r
+ Given an initial separation problem $\SepPA\Delta\nabla\emptyset$, $k$ is the\r
+ maximum number of nested lambdas, plus one. More formally:\r
+ % \renewcommand{\max}[2]{\operatorname{max}(#1,#2)}\r
+ \[\begin{array}{ll}\r
+ k(\SepPA\Delta\nabla\emptyset) & = \max {\{k(\Delta), k(\nabla) \}} \\\r
+ k(F) & = \max {\{k(f) \mid f \in F\}} \\\r
+ k(\lambda x_1\cdots x_n.\, i) & = \max{\{n+1, k(i)\}} \\\r
+ k(x\,f_1\cdots f_n) & = \max{\{k(f_i) \mid 1\leq i \leq n \}} \\\r
+ \end{array}\]\r
+\end{definition}\r
+\r
+The final eating can be done only if it is \emph{safe}:\r
+\r
+\begin{definition}[Safety of eating]\r
+ Intuitvely, eating is \emph{safe} if it cannot generate divergency.\r
+ More formally, let $\Delta = x\,f_1\cdots f_n$: eating is safe if:\r
+ \begin{enumerate}\r
+ \item (Convergent) whenever\r
+ $\nabla=C[x\,g_1\cdots g_m]$ for some $C$ and $\vec g$, $m<n$ holds.\r
+ \item (Numerals) \todo{complicated}\r
+ \end{enumerate}\r
+\r
+\end{definition}\r
+\r
+\begin{definition}[Evaluation]~\r
+ \begin{itemize}\r
+ \item \todo{usual beta, todo}\r
+ \item $C[(\Match \alpha {C'})\,t]; \Num \mapsto C[f]; \Num$ if $(\alpha,i,f)\in\Num$ with $C'[t]\Downarrow_\eta i$\r
+ \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
+ \item $\SepPA{\Delta}{\nabla}{\Num} \to \SepPA{\Delta'}{\nabla}{\Num'}$ if $\Delta,\Num \mapsto \Delta',\Num'$\r
+ \item $\SepPA{\Delta}{\nabla}{\Num} \to \SepPA{\Delta}{\nabla'}{\Num'}$ if $\nabla,\Num \mapsto \nabla',\Num'$\r
+ \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
+ \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
+ \end{itemize}\r
+\end{definition}\r
+\r
+\todo{Precondizioni: $\Delta$ is not an eta-subterm of $\nabla$, and $\Num$ is empty}\r
+\r
+\subsection{B\"ohm--like algorithm}\r
+\begin{definition}[Separation problem]~\r
+\r
+ A semi-\emph{separation problem} is a pair $\SepP\Delta\nabla$, where $\Delta$ and $\nabla$ are inerts.\r
+\r
+ $\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
+\end{definition}\r
+\r
+Steps of the algorithm:\r
+\begin{itemize}\r
+ \item \emph{Eat:} $x\mapsto \bot^n$ for some $n>0$\r
+ \item \emph{Step:} $x\mapsto \lambda \vec y\,\,z.\, z\,\vec\alpha\,\vec y$ for some fresh $\vec\alpha$ and $|\vec\alpha|> 0$\r
+\end{itemize}\r
+\r
+\begin{lemma}\r
+ If $\sigma$ is \ldots then $t\EtaNeq u$ implies $t\sigma \EtaNeq u\sigma$.\r
+\end{lemma}\r
+\begin{proof}\r
+ By induction on the derivation of $t\EtaNeq u$:\r
+ \begin{itemize}\r
+ \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
+ \item $x\,\vec f \EtaNeq y\,\vec g$ and $x\neq y$:\r
+ \item $x \, f_1\cdots f_n \EtaNeq x \, g_1\cdots g_n$ because $f_k\EtaNeq g_k$:\r
+ \item \ldots\r
+ \end{itemize}\r
+\end{proof}\r
+\r
+\begin{theorem}\r
+ If $\Delta\not\Subtm\nabla$ and $\Delta$ not a variable, then $\SepP\Delta\nabla$ is separable.\r
+\end{theorem}\r
+\begin{proof} By induction on $|\SepP\Delta\nabla|$. Two cases:\r
+ \begin{itemize}\r
+ \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
+ \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
+\r
+ What about the new problem $\SepP{(f_k\sigma)\vec\alpha\vec f\sigma}{\nabla\sigma}$? To prove:\r
+ \begin{itemize}\r
+ \item $\Delta\sigma\not\Subtm \nabla\sigma$\r
+ \item $|\SepP{\Delta\sigma}{\nabla\sigma}|<|\SepP\Delta\nabla|$\r
+ \end{itemize}\r
+ \end{itemize}\r
+\end{proof}\r
+\r
+\begin{definition}[Trivial set of inerts]\r
+ A set of inerts $I$ is trivial when it is empty, or it contains only variables.\r
+\end{definition}\r
+\r
+\begin{theorem}\r
+ Every non-trivial set of inerts is separable.\r
+\end{theorem}\r
+\begin{proof}~\r
+ \begin{itemize}\r
+ \item Take $i\in I$ s.t. $i$ is not a subterm of any other term in $I$\r
+ \item Solve the separation problem $\SepP{\{i\}}{I\setminus\{i\}}$\r
+ \end{itemize}\r
+\end{proof}\r
+\r
+\section{Fireballs with bombs}\r
+\r
+The goal here is separating \NewSystem{}-L\'evi-Longo trees.\r
+ Similarly as done in the section above, let us start instead from a simpler problem:\r
+ separating usual L\'evi-Longo trees by means of \emph{substitutions only}.\r
+\r
+% \newcommand{\dummy}{{\#}}\r
+\newcommand{\dummy}{\TmTrue}\r
+\newcommand{\myfalse}{\TmFalse}\r
+% \newcommand{\pacman}{\operatorname{P}}\r
+\newcommand{\sep}{\cdot}\r
+\r
+{\color{red}\begin{example}[$\eta$-differences may be invalidated by paths]\r
+ \todo{Descrivere questo esempio e capire la sua importanza}\r
+ \[x\, \bot^1 \, (\lambda y.\, \TmIdentity{}\comma \en{\cdot}{x\, \TmTrue\, \bot^1})\]\r
+ \[x\, \bot^1 \, (\lambda y.\, \TmIdentity{}\comma \en{\cdot}{x\, \TmFalse\, \bot^1})\]\r
+\end{example}}\r
+\r
+\begin{definition}[L\'evy-Longo trees]~\r
+ \[\begin{array}{ll}\r
+ f & \ddef i \mid \lambda x.\, f \mid \bot\\\r
+ i & \ddef x\, f_1 \cdots f_n \quad (n\geq 0) \\\r
+ \end{array}\]\r
+\end{definition}\r
+\r
+We denote $\bot^n := \lambda\underscore{}^n.\, \bot$ ($n\geq 0$ dummy abstractions).\r
+\r
+A semi-separation problem for this calculus may be defined similarly as in Definition~\ref{def:sspwso}.\r
+\r
+\r
+\r
+% First note that strong fireballs with bombs cannot be always separated with substitutions in strong normal form:\r
+%\r
+% \begin{example} Consider the following semi-separation problem:\r
+%\r
+% \begin{verbatim}\r
+% D x (_. BOT)\r
+% C x (_. _. BOT) t\r
+% \end{verbatim}\r
+%\r
+% A separator may be $\sigma \defeq x \mapsto \lambda y.\, (y \, z \semi z)$\r
+%\r
+% where f is any fireball.\r
+% \end{example}\r
+\r
+\begin{theorem}\r
+ Call-by-value semi-separation of L\'evy-Longo trees with substitutions only is NP-hard.\r
+\end{theorem}\r
+\begin{proof}\r
+ By a reduction from \emph{graph 3-coloring}.\r
+\r
+\newcommand{\bomb}{\operatorname{d}}\r
+\r
+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
+ \[\begin{array}{ccccccc}\r
+ \Uparrow & x & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \cdots & \dummy\,\dummy\,\dummy \\\r
+ \Downarrow & x & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \dummy\,\dummy\,\dummy & \cdots & t^1_n \, t^2_n \, t^3_n \\\r
+ \vdots \\\r
+ \Downarrow & x & \dummy\,\dummy\,\dummy & t_2^1 \, t_2^2 \, t_2^3 & \bomb\,\bomb\,\bomb\, & \cdots & \bomb\,\bomb\,\bomb\\\r
+ \Downarrow & x & t_1^1\, t_1^2\, t_1^3 & \bomb\,\bomb\,\bomb \,& \bomb\,\bomb\,\bomb\, & \cdots & \bomb\,\bomb\,\bomb \\\r
+ \end{array}\]\r
+\r
+Where: $x$ is the only free variable; $\bomb := \lambda \underscore{}\underscore{}.\, \bot$; $\dummy := \lambda xy.\, x$; $\myfalse := \lambda xy. \, y$.\r
+\r
+We now to define the terms $t_j^i$ for $i=1,2,3$ and $j=1\ldots n$.\r
+\r
+Intuitively:\r
+\begin{itemize}\r
+\r
+ \item $\begin{array}{ll}\r
+ t_1^1 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \myfalse{}\bomb\bomb \sep\bomb\ldots \\\r
+ t_1^2 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \bomb\myfalse{}\bomb \sep\bomb\ldots \\\r
+ t_1^3 \defeq & \lambda\underscore{}\underscore{}. \,\, x \sep \bomb\bomb\myfalse{} \sep\bomb\ldots \\\r
+ \end{array}$\r
+\r
+ \item $t_2^1 \defeq \begin{cases}\r
+ \lambda\underscore{}\underscore{}.\, x \sep \bomb \dummy\dummy \sep \myfalse{}\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\\r
+ \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
+ \end{cases}$\r
+\r
+ \item \ldots\r
+\end{itemize}\r
+\r
+In order to be more formal, we first need to define an index notation:\r
+\r
+\begin{definition}[Index notation]\r
+ 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
+ \end{definition}\r
+\r
+We can now define $t_j^i$:\r
+\[t_j^i[\,_{j'}^{i'}]\defeq\begin{cases}\r
+ \bomb & \text{if } j<j' \\\r
+ \begin{cases}\r
+ \bomb & \text{if } i\neq i' \\\r
+ \myfalse{} & \text{if } i = i' \\\r
+ \end{cases} & \text{if } j = j' \\\r
+ \begin{cases}\r
+ \bomb & \text{if } i = i' \\\r
+ \dummy & \text{if } i \neq i' \\\r
+ \end{cases} & \text{if } (v_j,v_{j'}) \in E \\\r
+ \dummy & \text{if } (v_j,v_{j'}) \not\in E\r
+\end{cases}\]\r
+\r
+Intuitively, if $\sigma(x)$ ``uses'' $t_j^i$, then $\sigma$ colors the vertex $v_j$ with color $i$.\r
+\r
+% Dimensione del problema: circa $(3\times m^2)^2$.\r
+Size of the problem: $|t_j^i|$ is $O(n)$, therefore the size of the problem is $O(n^2)$.\r
+\r
+% \begin{lemma}[Extraction of the coloring]\r
+% Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:\r
+%\r
+% \begin{itemize}\r
+% \item $\operatorname{color}(v_1) = 2$ iff\r
+% \[(x \sep \pacman\,\bomb\,\pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
+% \item $\operatorname{color}(v_2) = 3$ iff:\r
+% \[(x \sep \dummy\,\dummy\,\dummy \sep \pacman\,\pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
+% \end{itemize}\r
+% \end{lemma}\r
+\r
+\end{proof}\r
+\r
+\nocite{*}\r
+\bibliographystyle{apalike}\r
+\bibliography{bibliography}\r
+\r
+\end{document}\r
projects / fireball-separation.git / commitdiff