Syntactic fixes to distinction + Some commented out definitions to be used in the...

diff --git a/notes.tex b/notes.tex
index 15a8851dd43d034d5fd89aef0713ece48195ab92..1f3f2e548a000fffe8ebacd0498732b73918164a 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -59,14 +59,101 @@
   % \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{Distinction:} Let $T_x \defeq \{t \preceq T \mid \HeadOf{t} = \HeadOf{D} \}$.\r
-  Now: $C_x$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\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 t\in D_x$, $t_\pi \neq \Omega$;\r
-    \item $\exists t\in C_x$ s.t. $t \not\sim_\pi D$;\r
-    \item $\{t\in C_x \mid t \sim_\pi D\}$ is $D$--distinct.\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
+ % \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
 \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
+\r
 \end{document}\r