[fireball-separation.git] / notes.tex

\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{Strong Separation}\r
% \author{---}\r
\date{\vspace{-2em}\today{}}\r
\r
\input{macros}\r
\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
\r
\begin{document}\r
\r
\maketitle\r
\r
\section*{The Calculus}\r
\subparagraph{Syntax}\r
\[\begin{array}{lll}\r
  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\\r
  n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\\r
  \\\r
  C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
  P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
\end{array}\]\r
\r
\subparagraph{Reduction rules}\r
\[\begin{array}{lll}\r
  P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &\r
   P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
   P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &\r
    P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
\end{array}\]\r
\r
\subparagraph{Properties}\r
\begin{itemize}\r
  \item Every term is normalizing iff it is strongly normalizing.\r
  \item Ogni strategia e' perpetua!\r
  \item \ldots\r
\end{itemize}\r
\r
\clearpage\r
\section*{Separation}\r
% Paths:\r
\newcommand{\PathEmpty}{\epsilon}\r
\newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}\r
\newcommand{\PathArg}[3]{\mathtt{arg}_{#2}^{#1}(#3)}\r
\newcommand{\PathHd}{\mathtt{hd}}\r
\r
\newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}\r
\newcommand{\HeadOf}[1]{\operatorname{head}(#1)}\r
\newcommand{\FstOf}[1]{\operatorname{fst}(#1)}\r
\newcommand{\DegOf}[1]{\operatorname{deg}(#1)}\r
\newcommand{\SubtmOf}[2]{#1\preceq #2}\r
\newcommand{\OfHead}[2]{#1_{{\mid}#2}}\r
\newcommand{\SubtmsOf}[1]{\operatorname{Sub}(#1)}\r
\newcommand{\Div}{\mathtt{d}}\r
\newcommand{\Conv}{\mathtt{c}}\r
\newcommand{\Const}{\mathtt{K}}\r
\newcommand{\NamedBoundVar}[1]{\texttt{bvar(}#1\texttt{)}}\r
\newcommand{\AC}[1]{{\color{violet}#1}}\r
\begin{itemize}\r
  % \item \textbf{$\boldsymbol\sigma$-separation.}\r
  %  \textcolor{red}{come definirlo? con le variabili? con i termini?\r
  %   problematico in cbv}\r
  %  Two terms are $\sigma$-separable iff there exists a substitution\r
  %   $\sigma$ such that \textcolor{red}{???}\r
  % \item \textbf{Semi-$\boldsymbol\sigma$-separation.}\r
  %  Two terms are semi-$\sigma$-separable iff there exists a substitution\r
  %   $\sigma$ such that -- in short -- it makes one diverge and the other one converge.\r
  % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms\r
   % (in deep normal form)\r
   \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.\r
   \item \textbf{Subterm at position $\boldsymbol\pi$:} TODO\r
   \item $\boldsymbol\sim_{\boldsymbol\pi}$\r
   \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.\r
  $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\r
  \begin{itemize}\r
    \item \emph{effective} for $D$, cioe' $\FstOf{\pi} \leq \DegOf{D}$;\r
    \item $\forall \tm\in D_\var$, $\tm_\pi \neq \Omega$;\r
    \item $\exists \tm\in C_\var$ s.t. $\tm \not\sim_\pi D$;\r
    \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.\r
  \end{itemize}\r
\r
\clearpage\r
  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  \texttt{ prove di nuove definizioni di ac:}\r
\r
  \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$\r
  \[\begin{array}{ll}\r
    \SubtmsOf{\var} & \defeq \{\var\} \\\r
    \SubtmsOf{\tm\,\tmtwo} & \defeq \SubtmsOf\tm \cup \SubtmsOf\tmtwo \cup \{\tm\,\tmtwo\} \\\r
    \SubtmsOf{\lambda \var.\, \vec\tm} & \defeq \{\tmtwo\{\Const/\var\} \mid \tmtwo \in\SubtmsOf{\vec\tm}\} \\\r
  \end{array}\]\r
  \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}\r
  \item \textbf{Subterm at position:}\r
  \[\begin{array}{ll}\r
    \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi\r
  \end{array}\]\r
  \AC{\r
   Given a path, one can retrieve from a term (if possible) the subterm at that position.\r
\r
   Since the path may go through abstractions, bound variables that become free\r
   are renamed to variables of the form $\NamedBoundVar\pi$\r
   (where $\pi$ is the path in the original inert leading to the abstraction binding that variable).\r
  }\r
  % \newcommand{\GetSubtm}[2]{\operatorname{GetSubtm}(#1\texttt{;}#2)}\r
  \newcommand{\GetSubtm}[2]{{#1}_{#2}}\r
  \[\begin{array}{ll}\r
    \GetSubtm\tm\pi & \defeq \GetSubtm\tm{\underline\pi} \\\r
    \GetSubtm\tm{\rho[\underline\PathEmpty]} & \defeq \tm \\\r
    \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline\PathHd]} & \defeq x \\\r
    \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline{\PathArg i \var \pi}]} & \defeq\r
      \GetSubtm{(t_i)}{\rho[\PathArg i \var {\underline\pi}]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
    \GetSubtm{(\lambda x.\, t)}{\rho[\underline {\PathAbs \pi}]} & \defeq\r
     \GetSubtm\tm{\rho(\PathAbs{\underline\pi})}\r
     \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
    \GetSubtm{\tm}{\rho(\underline{\PathAbs \pi})} &\r
     \defeq \GetSubtm{(\lambda \var.\, \tm\,\var)}{\rho(\PathAbs {\underline\pi})} \text{ (with } x \text{ fresh) (eta)}\\\r
    % \Omega_-^- & \defeq \Omega \\\r
  \end{array}\]\r
  \item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$\r
  \item \textbf{Telescopic garbage chain:} $\{\langle\tm_1,\pi_1\rangle,\ldots,\langle\tm_n,\pi_n\rangle\}$ is a $-$ if $\forall i$:\r
   \[\tm_{i+1} \in \SubtmsOf{\text{garbage of } \GetSubtm{(\tm_i)}{\pi_i}}\]\r
  \item \textbf{Distinction:} \underline{$S$ is $\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct} iff (one of the following three):\r
  \begin{itemize}\r
    \item $\OfHead S {\HeadOf \Div}$ is empty and $n=1$\r
  \end{itemize}\r
   OR: let $\Div\defeq\Div_1$ in:\r
 \begin{itemize}\r
   \item there exists a path $\pi$ s.t.\r
   \item (Effective) $\pi$ is \emph{effective} for all $\Div_i$ s.t. $\HeadOf{\Div_i} = \HeadOf{\Div}$\r
   \item $\forall \tm\in \OfHead{\SubtmsOf{\Div_i}}{\HeadOf\Div}$, $\tm_\pi \neq \Omega$;\r
   \item (Useful) $\exists s\in \OfHead S{\HeadOf\Div}$ s.t. $s \not\sim_\pi \Div$;\r
   \item $S\setminus\{s\in \OfHead S{\HeadOf\Div} \mid s \not\sim_\pi \Div\}$ is $D$--distinct.\r
 \end{itemize}\r
 OR:\r
\begin{itemize}\r
   \item $S'$ is $\{\langle\Div_2,\pi_2\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct, where:\r
    \[S' \defeq S \mathrel{\cup} \SubtmsOf{\{\text{garbage of } s \text{ along } \pi_1 \mid s\in \OfHead{S}{\HeadOf\Div}\}} \]\r
 \end{itemize}\r
\r
 \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable\r
  IFF there is $\Div_1$ (an $\Omega$--approximation of a subterm of $\Div$ with\r
  at most one garbage, and without stuck variables)\r
  and a telescopic garbage chain $D\defeq\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$ s.t.\r
  $\SubtmsOf\Conv$ is $D$--distinct.\r
\r
 \clearpage\r
 \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
\r
 \item \textbf{Unlockable variables.}\r
  We use the following contexts:\r
  $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
 A variable $\var$ is \emph{unlockable} in a context $E$ if:\r
  \begin{itemize}\r
    \item it is not bound in $E$, or\r
    \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
     and $\vartwo$ is unlockable in $E'$.\r
  \end{itemize}\r
\r
  Transformation removing an unlockable variable bound at position $\pi$:\r
  \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]\r
\r
  % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}\r
\r
\end{itemize}\r
\r
% \clearpage\r
% \section*{NP-hardness}\r
% \newcommand{\Pacman}{\Omega}\r
% \newcommand{\sep}{\cdot}\r
% \begin{example}[Graph 3-coloring]\label{example:3col}\r
% Let $G=(V,E)$ be a graph, with $N \defeq |V|$.\r
% We encode the problem of finding a 3-coloring of $G$ in the following problem of semi-$\sigma$-separation:\r
%  \[\begin{array}{cl}\r
%  \Uparrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots t_n^1\,t_n^2\,t_n^3 \\\r
%  \\\r
%  \Downarrow & x \sep \Pacman\,\Pacman\,\Pacman \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots t_n^1\,t_n^2\,t_n^3 \\\r
%  \Downarrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep \Pacman\,\Pacman\,\Pacman \sep \cdots t_n^1\,t_n^2\,t_n^3 \\\r
%  \vdots & \vdots \\\r
%  \Downarrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots \Pacman\,\Pacman\,\Pacman \\\r
%  \end{array}\]\r
%\r
% Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows:\r
%\r
% \begin{itemize}\r
%\r
%  \item $\begin{array}{ll}\r
%   a_1^1 \defeq & \lambda\_. \, x \sep y\bomb\bomb \sep\bomb\ldots \\\r
%   a_1^2 \defeq & \lambda\_. \, x \sep \bomb y\bomb \sep\bomb\ldots \\\r
%   a_1^3 \defeq & \lambda\_. \, x \sep \bomb\bomb y \sep\bomb\ldots \\\r
%  \end{array}$\r
%\r
%  \item $a_2^1 \defeq \begin{cases}\r
%   \lambda\_.\, x \sep \bomb \dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\\r
%   \lambda\_.\, x \sep \dummy\dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\\r
%  \end{cases}$\r
%\r
%  \item \ldots\r
%\r
% \end{itemize}\r
%\r
% \begin{definition}[Index notation]\r
%  Let $t = x \sep x_1^1 x_2^1 x_3^1 \sep x_1^2 x_2^2 x_3^2 \sep \ldots \sep x_1^m x_2^m x_3^m$. Then: \[t[\,_k^j] \defeq x_k^j.\]\r
%  \end{definition}\r
%\r
% Let $z_0$, $z_1$, $z_2$ be variables.\r
%\r
% Define:\r
% \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases}\r
%  \bomb & \text{if } j<j' \\\r
%  \begin{cases}\r
%   \bomb & \text{if } k\neq k' \\\r
%   y & \text{if } k = k' \\\r
%  \end{cases} & \text{if } j = j' \\\r
%  \begin{cases}\r
%   \bomb & \text{if } k = k' \\\r
%   \dummy & \text{if } k \neq k' \\\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
% Attenzione! Le $a$ vanno protette da lambda ($\lambda\_$)!\r
%\r
% % Dimensione del problema: circa $(3\times m^2)^2$.\r
%\r
% Intuitively, if $\sigma(x)$ ``uses'' $a_j^i$, then $\sigma$ colors $v_j$ with color $i$.\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
% % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
%\r
% \end{example}\r
\clearpage\r
\section{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\r
\newcommand{\perm}{\pi}\r
\newcommand{\Perm}[2]{\pi[#1,#2]}\r
\newcommand{\xK}{\kappa}\r
\newcommand{\xN}{n}\r
\newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
\newcommand{\LAMNK}{\LAM\xN\xK}\r
\newcommand{\Apply}[2]{(#1\mapsto#2)}\r
\newcommand{\kn}{$(\kappa,n)$}\r
\newcommand{\knnf}{\kn{}-nf}\r
\newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
\newcommand{\Args}[1]{\operatorname{args}(#1)}\r
\newcommand{\Head}[1]{\operatorname{head}(#1)}\r
\begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]\r
  \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]\r
  \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]\r
  \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]\r
\end{definition}\r
\r
\begin{definition}[\kn{}-normal forms]\r
  First recall that terms in normal form have the shape\r
  $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.\r
  \r
  We define inductively the set of \knnf s (for $\xK,\xN$ natural numbers):\r
  $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
  $|\vec\var|\leq\xK$, $|\vec\tm|\leq\xN$, and every term in $\vec\tm$ is a \knnf{}.\r
\end{definition}\r
\r
\begin{definition}[Permutator $\Perm\cdot\cdot$]~\r
  \[\Perm i j \defeq \lambda\vec\var\vartwo.\,\vartwo\, \vec\alpha\,\vec\var\,\vartwo\]\r
  where $\vec\var$, $\vec\alpha$ and $\vartwo$ are fresh variables,\r
  with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
\end{definition}\r
\r
\begin{definition}{$\Apply\cdot\cdot$}\r
  We denote by $\tmtwo\Apply\var\tm$ the normal form of $\tmtwo\Subst\var\tm$ in normal form --\r
  if it has one.\r
\end{definition}\r
\r
\begin{lemma}\r
  Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
  If $A\leq \Args\tm$ and $B \geq \xK + A + 1$,\r
  let $\tmtwo\defeq\tm\Apply\var{\Perm{A}{B}}$ in:\r
  $\Lams\tm=\Lams\tmtwo$ and $\tmtwo\in\LAM ? ?$\r
\end{lemma}\r
\begin{proof}\r
  By induction on the normal form structure of $\tm$.\r
  Let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$:\r
  \begin{itemize}\r
    \item if $\vartwo=\var$, then\r
    $\tm\Apply\var\perm = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
    \item if $\vartwo\neq\var$, then $\tm\Apply\var\perm = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
    where $\vec\tmthree\defeq \vec\tmtwo\Apply\var\perm$.\r
    Conclude by inductive hypothesis.\r
  \end{itemize}\r
\end{proof}\r
\begin{corollary}\r
  Let $\tm \defeq \var\,f_1\cdots f_m$ a \knnf.\r
  If $A\leq m$ and $B \geq A + \xK$,\r
  then $\tm\Apply\var{\Perm{A}{B}}$ is an inert.\r
\end{corollary}\r
\r
\begin{lemma}\r
  For every $\tm,\tmtwo$ be \knnf{s},\r
  every fresh variable $\var$,\r
  $\perm\defeq\Perm{i}{i+k+1}$ permutator,\r
  $\tm\EtaEq\tmtwo$ iff $\tm\Apply\var\perm\EtaEq\tmtwo\Apply\var\perm$.\r
\end{lemma}\r
\r
\end{document}\r