notes.tex

   1 \documentclass[12pt]{article}\r
   2 \title{Strong Separation}\r
   3 % \author{---}\r
   4 \date{\vspace{-2em}\today{}}\r
   5 \input{macros}\r
   6 \r
   7 \begin{document}\r
   8 \r
   9 \maketitle\r
  10 \r
  11 \section*{The Calculus}\r
  12 \subparagraph{Syntax}\r
  13 \[\begin{array}{lll}\r
  14   \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\\r
  15   n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\\r
  16   \\\r
  17   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
  18   P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
  19 \end{array}\]\r
  20 \r
  21 \subparagraph{Reduction rules}\r
  22 \[\begin{array}{lll}\r
  23   P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &\r
  24    P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
  25    P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &\r
  26     P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
  27 \end{array}\]\r
  28 \r
  29 \subparagraph{Properties}\r
  30 \begin{itemize}\r
  31   \item Every term is normalizing iff it is strongly normalizing.\r
  32   \item Ogni strategia e' perpetua!\r
  33   \item \ldots\r
  34 \end{itemize}\r
  35 \r
  36 \clearpage\r
  37 \section*{Separation}\r
  38 % Paths:\r
  39 \newcommand{\PathEmpty}{\epsilon}\r
  40 \newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}\r
  41 \newcommand{\PathArg}[3]{\mathtt{arg}_{#2}^{#1}(#3)}\r
  42 \newcommand{\PathHd}{\mathtt{hd}}\r
  43 \r
  44 \newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}\r
  45 \newcommand{\HeadOf}[1]{\operatorname{head}(#1)}\r
  46 \newcommand{\FstOf}[1]{\operatorname{fst}(#1)}\r
  47 \newcommand{\DegOf}[1]{\operatorname{deg}(#1)}\r
  48 \newcommand{\SubtmOf}[2]{#1\preceq #2}\r
  49 \newcommand{\OfHead}[2]{#1_{{\mid}#2}}\r
  50 \newcommand{\SubtmsOf}[1]{\operatorname{Sub}(#1)}\r
  51 \newcommand{\Div}{\mathtt{d}}\r
  52 \newcommand{\Conv}{\mathtt{c}}\r
  53 \newcommand{\Const}{\mathtt{K}}\r
  54 \newcommand{\NamedBoundVar}[1]{\texttt{bvar(}#1\texttt{)}}\r
  55 \newcommand{\AC}[1]{{\color{violet}#1}}\r
  56 \begin{itemize}\r
  57   % \item \textbf{$\boldsymbol\sigma$-separation.}\r
  58   %  \textcolor{red}{come definirlo? con le variabili? con i termini?\r
  59   %   problematico in cbv}\r
  60   %  Two terms are $\sigma$-separable iff there exists a substitution\r
  61   %   $\sigma$ such that \textcolor{red}{???}\r
  62   % \item \textbf{Semi-$\boldsymbol\sigma$-separation.}\r
  63   %  Two terms are semi-$\sigma$-separable iff there exists a substitution\r
  64   %   $\sigma$ such that -- in short -- it makes one diverge and the other one converge.\r
  65   % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms\r
  66    % (in deep normal form)\r
  67    \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.\r
  68    \item \textbf{Subterm at position $\boldsymbol\pi$:} TODO\r
  69    \item $\boldsymbol\sim_{\boldsymbol\pi}$\r
  70    \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.\r
  71   $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\r
  72   \begin{itemize}\r
  73     \item \emph{effective} for $D$, cioe' $\FstOf{\pi} \leq \DegOf{D}$;\r
  74     \item $\forall \tm\in D_\var$, $\tm_\pi \neq \Omega$;\r
  75     \item $\exists \tm\in C_\var$ s.t. $\tm \not\sim_\pi D$;\r
  76     \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.\r
  77   \end{itemize}\r
  78 \r
  79 \clearpage\r
  80   \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  81   $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  82   $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
  83   \texttt{ prove di nuove definizioni di ac:}\r
  84 \r
  85   \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$\r
  86   \[\begin{array}{ll}\r
  87     \SubtmsOf{\var} & \defeq \{\var\} \\\r
  88     \SubtmsOf{\tm\,\tmtwo} & \defeq \SubtmsOf\tm \cup \SubtmsOf\tmtwo \cup \{\tm\,\tmtwo\} \\\r
  89     \SubtmsOf{\lambda \var.\, \vec\tm} & \defeq \{\tmtwo\{\Const/\var\} \mid \tmtwo \in\SubtmsOf{\vec\tm}\} \\\r
  90   \end{array}\]\r
  91   \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}\r
  92   \item \textbf{Subterm at position:}\r
  93   \[\begin{array}{ll}\r
  94     \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi\r
  95   \end{array}\]\r
  96   \AC{\r
  97    Given a path, one can retrieve from a term (if possible) the subterm at that position.\r
  98 \r
  99    Since the path may go through abstractions, bound variables that become free\r
 100    are renamed to variables of the form $\NamedBoundVar\pi$\r
 101    (where $\pi$ is the path in the original inert leading to the abstraction binding that variable).\r
 102   }\r
 103   % \newcommand{\GetSubtm}[2]{\operatorname{GetSubtm}(#1\texttt{;}#2)}\r
 104   \newcommand{\GetSubtm}[2]{{#1}_{#2}}\r
 105   \[\begin{array}{ll}\r
 106     \GetSubtm\tm\pi & \defeq \GetSubtm\tm{\underline\pi} \\\r
 107     \GetSubtm\tm{\rho[\underline\PathEmpty]} & \defeq \tm \\\r
 108     \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline\PathHd]} & \defeq x \\\r
 109     \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline{\PathArg i \var \pi}]} & \defeq\r
 110       \GetSubtm{(t_i)}{\rho[\PathArg i \var {\underline\pi}]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
 111     \GetSubtm{(\lambda x.\, t)}{\rho[\underline {\PathAbs \pi}]} & \defeq\r
 112      \GetSubtm\tm{\rho(\PathAbs{\underline\pi})}\r
 113      \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
 114     \GetSubtm{\tm}{\rho(\underline{\PathAbs \pi})} &\r
 115      \defeq \GetSubtm{(\lambda \var.\, \tm\,\var)}{\rho(\PathAbs {\underline\pi})} \text{ (with } x \text{ fresh) (eta)}\\\r
 116     % \Omega_-^- & \defeq \Omega \\\r
 117   \end{array}\]\r
 118   \item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$\r
 119   \item \textbf{Telescopic garbage chain:} $\{\langle\tm_1,\pi_1\rangle,\ldots,\langle\tm_n,\pi_n\rangle\}$ is a $-$ if $\forall i$:\r
 120    \[\tm_{i+1} \in \SubtmsOf{\text{garbage of } \GetSubtm{(\tm_i)}{\pi_i}}\]\r
 121   \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
 122   \begin{itemize}\r
 123     \item $\OfHead S {\HeadOf \Div}$ is empty and $n=1$\r
 124   \end{itemize}\r
 125    OR: let $\Div\defeq\Div_1$ in:\r
 126  \begin{itemize}\r
 127    \item there exists a path $\pi$ s.t.\r
 128    \item (Effective) $\pi$ is \emph{effective} for all $\Div_i$ s.t. $\HeadOf{\Div_i} = \HeadOf{\Div}$\r
 129    \item $\forall \tm\in \OfHead{\SubtmsOf{\Div_i}}{\HeadOf\Div}$, $\tm_\pi \neq \Omega$;\r
 130    \item (Useful) $\exists s\in \OfHead S{\HeadOf\Div}$ s.t. $s \not\sim_\pi \Div$;\r
 131    \item $S\setminus\{s\in \OfHead S{\HeadOf\Div} \mid s \not\sim_\pi \Div\}$ is $D$--distinct.\r
 132  \end{itemize}\r
 133  OR:\r
 134 \begin{itemize}\r
 135    \item $S'$ is $\{\langle\Div_2,\pi_2\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct, where:\r
 136     \[S' \defeq S \mathrel{\cup} \SubtmsOf{\{\text{garbage of } s \text{ along } \pi_1 \mid s\in \OfHead{S}{\HeadOf\Div}\}} \]\r
 137  \end{itemize}\r
 138 \r
 139  \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable\r
 140   IFF there is $\Div_1$ (an $\Omega$--approximation of a subterm of $\Div$ with\r
 141   at most one garbage, and without stuck variables)\r
 142   and a telescopic garbage chain $D\defeq\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$ s.t.\r
 143   $\SubtmsOf\Conv$ is $D$--distinct.\r
 144 \r
 145  \clearpage\r
 146  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 147  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 148  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
 149 \r
 150  \item \textbf{Unlockable variables.}\r
 151   We use the following contexts:\r
 152   $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
 153  A variable $\var$ is \emph{unlockable} in a context $E$ if:\r
 154   \begin{itemize}\r
 155     \item it is not bound in $E$, or\r
 156     \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
 157      and $\vartwo$ is unlockable in $E'$.\r
 158   \end{itemize}\r
 159 \r
 160   Transformation removing an unlockable variable bound at position $\pi$:\r
 161   \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]\r
 162 \r
 163   % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}\r
 164 \r
 165 \end{itemize}\r
 166 \r
 167 % \clearpage\r
 168 % \section*{NP-hardness}\r
 169 % \newcommand{\Pacman}{\Omega}\r
 170 % \newcommand{\sep}{\cdot}\r
 171 % \begin{example}[Graph 3-coloring]\label{example:3col}\r
 172 % Let $G=(V,E)$ be a graph, with $N \defeq |V|$.\r
 173 % We encode the problem of finding a 3-coloring of $G$ in the following problem of semi-$\sigma$-separation:\r
 174 %  \[\begin{array}{cl}\r
 175 %  \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
 176 %  \\\r
 177 %  \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
 178 %  \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
 179 %  \vdots & \vdots \\\r
 180 %  \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
 181 %  \end{array}\]\r
 182 %\r
 183 % Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows:\r
 184 %\r
 185 % \begin{itemize}\r
 186 %\r
 187 %  \item $\begin{array}{ll}\r
 188 %   a_1^1 \defeq & \lambda\_. \, x \sep y\bomb\bomb \sep\bomb\ldots \\\r
 189 %   a_1^2 \defeq & \lambda\_. \, x \sep \bomb y\bomb \sep\bomb\ldots \\\r
 190 %   a_1^3 \defeq & \lambda\_. \, x \sep \bomb\bomb y \sep\bomb\ldots \\\r
 191 %  \end{array}$\r
 192 %\r
 193 %  \item $a_2^1 \defeq \begin{cases}\r
 194 %   \lambda\_.\, x \sep \bomb \dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\\r
 195 %   \lambda\_.\, x \sep \dummy\dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\\r
 196 %  \end{cases}$\r
 197 %\r
 198 %  \item \ldots\r
 199 %\r
 200 % \end{itemize}\r
 201 %\r
 202 % \begin{definition}[Index notation]\r
 203 %  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
 204 %  \end{definition}\r
 205 %\r
 206 % Let $z_0$, $z_1$, $z_2$ be variables.\r
 207 %\r
 208 % Define:\r
 209 % \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases}\r
 210 %  \bomb & \text{if } j<j' \\\r
 211 %  \begin{cases}\r
 212 %   \bomb & \text{if } k\neq k' \\\r
 213 %   y & \text{if } k = k' \\\r
 214 %  \end{cases} & \text{if } j = j' \\\r
 215 %  \begin{cases}\r
 216 %   \bomb & \text{if } k = k' \\\r
 217 %   \dummy & \text{if } k \neq k' \\\r
 218 %  \end{cases} & \text{if } (v_j,v_{j'}) \in E \\\r
 219 %  \dummy & \text{if } (v_j,v_{j'}) \not\in E\r
 220 % \end{cases}\]\r
 221 %\r
 222 % Attenzione! Le $a$ vanno protette da lambda ($\lambda\_$)!\r
 223 %\r
 224 % % Dimensione del problema: circa $(3\times m^2)^2$.\r
 225 %\r
 226 % Intuitively, if $\sigma(x)$ ``uses'' $a_j^i$, then $\sigma$ colors $v_j$ with color $i$.\r
 227 %\r
 228 % \begin{lemma}[Extraction of the coloring]\r
 229 %  Let $\sigma$ be a substitution which is a solution for the semi-separation problem. Then for example:\r
 230 %\r
 231 % \begin{itemize}\r
 232 %  \item $\operatorname{color}(v_1) = 2$ iff\r
 233 %   \[(x \sep \Pacman\,\bomb\,\Pacman \sep \bomb\,\bomb\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 234 %  \item $\operatorname{color}(v_2) = 3$ iff:\r
 235 %   \[(x \sep \dummy\,\dummy\,\dummy \sep \Pacman\,\Pacman\,\bomb \,\sep \bomb\,\bomb\,\bomb \,\sep \cdots \sep \bomb\,\bomb\,\bomb)\,\sigma \to \bot\]\r
 236 % \end{itemize}\r
 237 % \end{lemma}\r
 238 %\r
 239 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
 240 %\r
 241 % \end{example}\r
 242 \clearpage\r
 243 \section[Tentativi X-separability]{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\r
 244 \newcommand{\perm}{p}\r
 245 \newcommand{\Perm}[2]{\operatorname{P}[#1,#2]}\r
 246 \newcommand{\xK}{\kappa}\r
 247 \newcommand{\xN}{n}\r
 248 \newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
 249 \newcommand{\LAMNK}{\LAM\xN\xK}\r
 250 % \newcommand{\kn}{$(\kappa,n)$}\r
 251 \newcommand{\knnf}{$\xK{}$-nf}\r
 252 \newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
 253 \newcommand{\Args}[1]{\operatorname{args}(#1)}\r
 254 \newcommand{\Head}[1]{\operatorname{head}(#1)}\r
 255 \newcommand{\nf}[1]{#1{\downarrow}}\r
 256 \newcommand{\Nat}{\mathbb{N}}\r
 257 \begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]\r
 258   \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]\r
 259   \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]\r
 260   \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]\r
 261 \end{definition}\r
 262 \r
 263 \begin{definition}[$\xK$-normal forms]\r
 264   First recall that terms in normal form have the shape\r
 265   $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.\r
 266   \r
 267   We define inductively the set of \knnf s (where $\xK$ is a natural number):\r
 268   $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
 269   $|\vec\var|\leq\xK$%\r
 270   %, $|\vec\tm|\leq\xN$\r
 271   , and every term in $\vec\tm$ is a \knnf{} as well.\r
 272 \end{definition}\r
 273 \r
 274 \begin{definition}[Normal form $\nf\cdot$]\r
 275   \r
 276 \end{definition}\r
 277 \r
 278 \begin{definition}[Permutator $\Perm\cdot\cdot$]~\r
 279   \[\Perm i j \defeq \lambda\vec\var\vartwo.\,\vartwo\, \vec\alpha\,\vec\var\,\vartwo\]\r
 280   where $\vec\var$, $\vec\alpha$ and $\vartwo$ are fresh variables,\r
 281   with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
 282 \end{definition}\r
 283 \r
 284 \begin{lemma}[Monotonicity]\label{l:k-nf-mono}\r
 285   If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf\r
 286   for every $\xK' \geq \xK{}$.\r
 287 \end{lemma}\r
 288 \r
 289 \begin{lemma}\label{l:k-prime-nf}\r
 290   Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$.\r
 291   Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.\r
 292 \end{lemma}\r
 293 \begin{proof}\r
 294   By induction on $|\tm|$.\r
 295   Let $\tm=\lambda\vec\vartwo.\,\head\,\vec\args$ and $\sigma\defeq\Subst\var{\Perm i j}$.\r
 296   By cases:\r
 297   \begin{itemize}\r
 298     \item Case $\head\neq\var$: $\nf{\tm\sigma} = \lambda\vec\vartwo.\,\head\,\vec{(\nf{\args\sigma})}$.\r
 299     By \ih{} each term in $\vec{(\nf{\args\sigma})}$ is a $\xK'$-nf.\r
 300     We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.\r
 301     \item Case $\head=\var$ and $|\vec\args| \leq i$:\r
 302     $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $ for \r
 303     $|\vec\varthree| = i - |\vec\args|$.\r
 304     Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.\r
 305     \item Case $\head=\var$ and $i<|\vec\args|$:\r
 306      $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
 307      Now, by \ih{} $\nf{\args_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,\r
 308      $\nf{(\args_i\sigma\vec\alpha)}$ is inert.\r
 309      Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\args_i\sigma\vec\alpha)} \vec{(\nf{\args\sigma})}$,\r
 310      and again by \ih{} it is also a $\xK'$-nf.\r
 311   \end{itemize}\r
 312   \r
 313 \end{proof}\r
 314 \r
 315 \begin{lemma}[Admissible]\r
 316   Let $\tm$ an inert \knnf.\r
 317   If $i<\Args\tm$ and $j \geq \xK + i + 1$\r
 318   then $\nf{\tm\Subst{\HeadOf\tm}{\Perm i j}}$\r
 319   is inert.\r
 320 \end{lemma}\r
 321 \begin{proof}\r
 322   Let $\tm = \var\,\vec a$, $\perm \defeq \Perm i j$, and $\sigma\defeq\Subst\var\perm$.\r
 323   Then $\nf{\tm\Subst\var\perm} = \nf{(a_i\sigma\,\vec\alpha\,\vec {(a\sigma)})}$.\r
 324   By \reflemma{k-prime-nf} $\nf{a_i\sigma}$ is a $\xK'$-nf with $\xK'\defeq \xK+i+1$.\r
 325   Therefore $\nf{(a_i\sigma\vec\alpha)}$ is inert because $|\vec\alpha|=j\geq\xK'$.\r
 326 \end{proof}\r
 327 \r
 328 % \begin{lemma}\r
 329 %   Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
 330 %   If $i<\Args\tm$ and $j \geq \xK + i + 1$,\r
 331 %   then $\tmtwo\defeq\nf{\tm\Subst\var{\Perm i j}}$ is defined;\r
 332 %   $\Lams\tm=\Lams{\tmtwo}$; $\tmtwo$ is a $(j,\xN + j)$-nf.\r
 333 % \end{lemma}\r
 334 % \begin{proof}\color{red}\TODO{}\r
 335 %   By induction on the normal form structure of $\tm$:\r
 336 %   let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$.\r
 337 %   By \ih{}, $\nf{\tmtwo\Subst\var\perm}$ are $(j,\xN+j)$-nfs.\r
 338 %   \begin{itemize}\r
 339 %     \item if $\vartwo=\var$, then\r
 340 %     $\nf{\tm\Subst\var\perm} = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
 341 %     \item if $\vartwo\neq\var$, then $\nf{\tm\Subst\var\perm} = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
 342 %     where $\vec\tmthree\defeq \nf{\vec\tmtwo\Subst\var\perm}$.\r
 343 %     Conclude by inductive hypothesis.\r
 344 %   \end{itemize}\r
 345 % \end{proof}\r
 346 \r
 347 \r
 348 \begin{lemma}\label{l:aux1}\r
 349   For every \knnf s $\tm$,\r
 350   every fresh variable $\var$,\r
 351   every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
 352   $\nf{(\tm\Subst\var\perm\vec\alpha)} = \tmtwo \, \alpha_j$\r
 353   for some inert $\tmtwo$.\r
 354 \end{lemma}\r
 355 \begin{proof}\r
 356   First of all note that by \reflemma{k-prime-nf}\r
 357   $\nf{\tm\Subst\var\perm}$ is a $\xK'$-nf for $\xK' \defeq \xK+i+1$, therefore\r
 358   $\nf{(\tm\Subst\var\perm\vec\alpha)}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.\r
 359   \r
 360   More precisely, $\nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}$ is inert,\r
 361   and therefore $\nf{(\tm\Subst\var\perm\vec\alpha)} = \nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}\,\alpha_{\xK'+1}\cdots\alpha_j$,\r
 362   and we conclude.\r
 363 \end{proof}\r
 364 \r
 365 \begin{lemma}\label{l:aux2}\r
 366   For every \knnf s $\tm$,\r
 367   every fresh variable $\var$,\r
 368   every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
 369   $\nf{(\tm\Subst\var\perm)} \EtaNeq \alpha_j$.\r
 370 \end{lemma}\r
 371 \begin{proof}\r
 372   By induction on $|\tm|$.\r
 373   Let $\tm = \lambda\vec\vartwo.\,h\,\vec a$ and $\sigma\defeq\Subst\var\perm$:\r
 374   \begin{itemize}\r
 375     \item If $h \neq \var$, then $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h\,\vec {(\nf {a\sigma})}$,\r
 376     and we conclude since $h\neq \alpha_j$ by the hypothesis that $\alpha_j$ is\r
 377     a fresh variable.\r
 378     \item If $h=\var$ and $|\vec a| \leq i$, then\r
 379     $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $,\r
 380     and we conclude since the head $\varthree'$ is a bound variable,\r
 381     while $\alpha_j$ is free.\r
 382     \item If $h=\var$ and $|\vec a| > i$, then\r
 383     $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
 384     $\nf{(\args_i\sigma\,\vec\alpha)} = \tmtwo\,\alpha_j$ by \reflemma{aux1}\r
 385     for some inert $\tmtwo$. Clearly $\tmtwo\,\alpha_j \EtaNeq \alpha_j$.\r
 386   \end{itemize}\r
 387 \end{proof}\r
 388 \r
 389 \begin{theorem}\r
 390   For every \knnf s $\tm$ and $\tmtwo$,\r
 391   every fresh variable $\var$,\r
 392   $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$,\r
 393   $\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.\r
 394 \end{theorem}\r
 395 \begin{proof}\r
 396   Let $\sigma \defeq \Subst\var\perm$.\r
 397   First of all, note that by \reflemma{k-prime-nf}\r
 398   $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and\r
 399   are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$.\r
 400   \r
 401   If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$.\r
 402   Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that\r
 403   $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.\r
 404   Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and \r
 405   $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,\r
 406   with $|\vec a|,|\vec b| > i$ {\color{red}[Capire perche' si puo' $\eta$-espandere qui]}.\r
 407   By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,\r
 408   and by cases on the definition of eta-difference:\r
 409   \begin{itemize}\r
 410     \item $h_1 \neq h_2$: we distinguish three subcases.\r
 411     \begin{itemize}\r
 412       \item $h_1,h_2\neq \var$:\r
 413        it follows that $\nf{\tm\sigma} = \nf{(\lambda\vec\vartwo.\,h_1\,\vec a)\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
 414        and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
 415        and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because\r
 416        their head variables are different.\r
 417       \item $h_1=\var$ and $h_2\neq \var$: \TODO\r
 418        $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$\r
 419       \item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.\r
 420     \end{itemize}\r
 421     \item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:\r
 422      if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
 423      and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
 424      and we conclude because the two terms have a different number of arguments.\r
 425      \r
 426      We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
 427      {\color{red}[Usare \reflemma{aux2} nei punti seguenti]}\r
 428      \begin{itemize}\r
 429        \item $|\vec a|,|\vec b|\leq i$: \TODO\r
 430        \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
 431        \item $|\vec a|\leq i$ and $|\vec b|> i$: symmetric to the case above.\r
 432        \item $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
 433        plus another one. Reason on the numebr of arguments\r
 434        $\Args{\nf{a_i\sigma\vec\alpha}}$ vs  \r
 435        $\Args{\nf{b_i\sigma\vec\alpha}}$.\r
 436        If equal conclude, otherwise conclude by lemma above.\r
 437      \end{itemize}\r
 438     \item \r
 439     $h_1 = h_2$ and $|\vec a| = |\vec b|$\r
 440     but $a_n \EtaNeq b_n$ for some $n$.\r
 441     If $h_1=h_2\neq\var$, then again\r
 442     $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =%\r
 443     \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
 444     and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that \r
 445     $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.\r
 446     {\color{red}[Capire se possiamo davvero usare l'\ih{} qui]}\r
 447     \r
 448     We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
 449     \begin{itemize}\r
 450       \item $|\vec a| = |\vec b| \leq i$: \TODO easy \r
 451       \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok\r
 452       \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO\r
 453        by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$\r
 454        and conclude by appending the $\vec a$ and $\vec b$.\r
 455     \end{itemize}\r
 456   \end{itemize}\r
 457 \end{proof}\r
 458 \r
 459 \end{document}\r