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{Strong Separation}
\r
10 \date{\vspace{-2em}\today{}}
\r
13 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
\r
19 \section*{The Calculus}
\r
20 \subparagraph{Syntax}
\r
21 \[\begin{array}{lll}
\r
22 \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\
\r
23 n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\
\r
25 C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
\r
26 P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\
\r
29 \subparagraph{Reduction rules}
\r
30 \[\begin{array}{lll}
\r
31 P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &
\r
32 P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\
\r
33 P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &
\r
34 P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\
\r
37 \subparagraph{Properties}
\r
39 \item Every term is normalizing iff it is strongly normalizing.
\r
40 \item Ogni strategia e' perpetua!
\r
45 \section*{Separation}
\r
46 \newcommand{\HeadOf}[1]{\operatorname{head}(#1)}
\r
47 \newcommand{\FstOf}[1]{\operatorname{fst}(#1)}
\r
48 \newcommand{\DegOf}[1]{\operatorname{deg}(#1)}
\r
49 \newcommand{\SubtmOf}[2]{#1\preceq #2}
\r
51 % \item \textbf{$\boldsymbol\sigma$-separation.}
\r
52 % \textcolor{red}{come definirlo? con le variabili? con i termini?
\r
53 % problematico in cbv}
\r
54 % Two terms are $\sigma$-separable iff there exists a substitution
\r
55 % $\sigma$ such that \textcolor{red}{???}
\r
56 % \item \textbf{Semi-$\boldsymbol\sigma$-separation.}
\r
57 % Two terms are semi-$\sigma$-separable iff there exists a substitution
\r
58 % $\sigma$ such that -- in short -- it makes one diverge and the other one converge.
\r
59 % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms
\r
60 % (in deep normal form)
\r
61 \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.
\r
62 \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.
\r
63 $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:
\r
65 \item \emph{effective} for $D$, cioe' $\FstOf{\pi} \leq \DegOf{D}$;
\r
66 \item $\forall \tm\in D_\var$, $\tm_\pi \neq \Omega$;
\r
67 \item $\exists \tm\in C_\var$ s.t. $\tm \not\sim_\pi D$;
\r
68 \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.
\r
71 % \item \textbf{Unlockable variables.}
\r
72 % We use the following contexts:
\r
73 % $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.
\r
74 % A variable $\var$ is \emph{unlockable} in a context $E$ if:
\r
76 % \item it is not bound in $E$, or
\r
77 % \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$
\r
78 % and $\vartwo$ is unlockable in $E'$.
\r
84 % \section*{NP-hardness}
\r
85 % \newcommand{\Pacman}{\Omega}
\r
86 % \newcommand{\sep}{\cdot}
\r
87 % \begin{example}[Graph 3-coloring]\label{example:3col}
\r
88 % Let $G=(V,E)$ be a graph, with $N \defeq |V|$.
\r
89 % We encode the problem of finding a 3-coloring of $G$ in the following problem of semi-$\sigma$-separation:
\r
90 % \[\begin{array}{cl}
\r
91 % \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
93 % \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
94 % \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
95 % \vdots & \vdots \\
\r
96 % \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
99 % Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows:
\r
103 % \item $\begin{array}{ll}
\r
104 % a_1^1 \defeq & \lambda\_. \, x \sep y\bomb\bomb \sep\bomb\ldots \\
\r
105 % a_1^2 \defeq & \lambda\_. \, x \sep \bomb y\bomb \sep\bomb\ldots \\
\r
106 % a_1^3 \defeq & \lambda\_. \, x \sep \bomb\bomb y \sep\bomb\ldots \\
\r
109 % \item $a_2^1 \defeq \begin{cases}
\r
110 % \lambda\_.\, x \sep \bomb \dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\
\r
111 % \lambda\_.\, x \sep \dummy\dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\
\r
118 % \begin{definition}[Index notation]
\r
119 % 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
122 % Let $z_0$, $z_1$, $z_2$ be variables.
\r
125 % \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases}
\r
126 % \bomb & \text{if } j<j' \\
\r
128 % \bomb & \text{if } k\neq k' \\
\r
129 % y & \text{if } k = k' \\
\r
130 % \end{cases} & \text{if } j = j' \\
\r
132 % \bomb & \text{if } k = k' \\
\r
133 % \dummy & \text{if } k \neq k' \\
\r
134 % \end{cases} & \text{if } (v_j,v_{j'}) \in E \\
\r
135 % \dummy & \text{if } (v_j,v_{j'}) \not\in E
\r
138 % Attenzione! Le $a$ vanno protette da lambda ($\lambda\_$)!
\r
140 % % Dimensione del problema: circa $(3\times m^2)^2$.
\r
142 % Intuitively, if $\sigma(x)$ ``uses'' $a_j^i$, then $\sigma$ colors $v_j$ with color $i$.
\r
144 % \begin{lemma}[Extraction of the coloring]
\r
145 % Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:
\r
148 % \item $\operatorname{color}(v_1) = 2$ iff
\r
149 % \[(x \sep \Pacman\,\bomb\,\Pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]
\r
150 % \item $\operatorname{color}(v_2) = 3$ iff:
\r
151 % \[(x \sep \dummy\,\dummy\,\dummy \sep \Pacman\,\Pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]
\r
155 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.
\r