1 \documentclass[12pt]{article}
\r
2 \title{Strong Separation}
\r
4 \date{\vspace{-2em}\today{}}
\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
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
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
29 \subparagraph{Properties}
\r
31 \item Every term is normalizing iff it is strongly normalizing.
\r
32 \item Ogni strategia e' perpetua!
\r
37 \section*{Separation}
\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
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
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
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
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
85 \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$
\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
91 \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}
\r
92 \item \textbf{Subterm at position:}
\r
94 \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi
\r
97 Given a path, one can retrieve from a term (if possible) the subterm at that position.
\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
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
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
123 \item $\OfHead S {\HeadOf \Div}$ is empty and $n=1$
\r
125 OR: let $\Div\defeq\Div_1$ in:
\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
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
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
146 \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
\r
147 $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
\r
148 $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
\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
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
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
163 % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}
\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
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
183 % Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows:
\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
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
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
206 % Let $z_0$, $z_1$, $z_2$ be variables.
\r
209 % \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases}
\r
210 % \bomb & \text{if } j<j' \\
\r
212 % \bomb & \text{if } k\neq k' \\
\r
213 % y & \text{if } k = k' \\
\r
214 % \end{cases} & \text{if } j = j' \\
\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
222 % Attenzione! Le $a$ vanno protette da lambda ($\lambda\_$)!
\r
224 % % Dimensione del problema: circa $(3\times m^2)^2$.
\r
226 % Intuitively, if $\sigma(x)$ ``uses'' $a_j^i$, then $\sigma$ colors $v_j$ with color $i$.
\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
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
239 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.
\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
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
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
274 \begin{definition}[Normal form $\nf\cdot$]
\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
284 {\color{yellow}\begin{definition}[Good permutation]
\r
286 $\Perm i j$ is \emph{good} for $\tm$ if
\r
287 $i<\Args\tm$ and $j \geq \xK + i + 1$.
\r
292 % Let $\vec\alpha$ fresh variables.
\r
293 % If $|\vec\alpha|\geq \lams\tm$,
\r
294 % then the normal form of $\tm\,\vec\alpha$ is inert.
\r
297 \begin{lemma}[Monotonicity]\label{l:k-nf-mono}
\r
298 If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf
\r
299 for every $\xK' \geq \xK{}$.
\r
302 \begin{lemma}\label{l:k-prime-nf}
\r
303 Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$.
\r
304 Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.
\r
307 By (course-of-value) structural induction on $\tm$.
\r
308 Let $\tm=\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo$ and $\sigma\defeq\Subst\var{\Perm i j}$.
\r
311 \item Case $\varthree\neq\var$: $\nf{(\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo)\sigma} = \lambda\vec\vartwo.\,\varthree\,\vec{(\nf{\tmtwo\sigma})}$.
\r
312 By \ih{} each term in $\vec{(\nf{\tmtwo\sigma})}$ is a $\xK'$-nf.
\r
313 We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.
\r
314 \item Case $\varthree=\var$ and $i<|\vec\tmtwo|$:
\r
315 $\tm\sigma \to^* \lambda\vec\vartwo.\, (\tmtwo_i\sigma)\vec\alpha \vec{(\tmtwo\sigma)} $.
\r
316 Now, by \ih{} $\nf{\tmtwo_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,
\r
317 $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert (\textcolor{red}{Serve lemma?}).
\r
318 Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \vec{(\nf{\tmtwo\sigma})}$,
\r
319 and again by \ih{} it is also a $\xK'$-nf.
\r
320 \item Case $\varthree=\var$ and $i \geq |\vec\tmtwo|$:
\r
321 $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for
\r
322 $|\vec\varthree| = i - |\vec\tmtwo|$.
\r
323 Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.
\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
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
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
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} \EtaNeq \alpha_j$.
\r
355 First of all note that by \reflemma{k-prime-nf}
\r
356 $\nf{\tm\Subst\var\perm}$ is a $\xK'$-nf for $\xK' \defeq \xK+i+1$, therefore
\r
357 $\nf{\tm\Subst\var\perm\vec\alpha}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.
\r
359 By structural induction on $\tm$.
\r
360 Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.
\r
364 % TODO: $\xK$-standard proof of $\eta$.
\r
367 For every \knnf s $\tm$ and $\tmtwo$,
\r
368 every fresh variable $\var$,
\r
369 $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$,
\r
370 $\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.
\r
373 Let $\sigma \defeq \Subst\var\perm$.
\r
374 First of all, note that by \reflemma{k-prime-nf}
\r
375 $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and
\r
376 are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$.
\r
378 If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$.
\r
379 Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that
\r
380 $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.
\r
381 Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and
\r
382 $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,
\r
383 with $|\vec\vartwo| = \xK$ {\color{red}[Capire perche' si puo' $\xK$-$\eta$-espandere qui]}.
\r
384 By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,
\r
385 and by cases on the definition of eta-difference:
\r
387 \item $h_1 \neq h_2$: we distinguish three subcases.
\r
389 \item $h_1,h_2\neq \var$:
\r
390 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
391 and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,
\r
392 and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because
\r
393 their head variables are different.
\r
394 \item $h_1=\var$ and $h_2\neq \var$: \TODO
\r
395 \item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.
\r
397 \item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:
\r
398 if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$
\r
399 and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,
\r
400 and we conclude because the two terms have a different number of arguments.
\r
402 We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:
\r
404 \item $|\vec a|,|\vec b|\leq i$: \TODO
\r
405 \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO
\r
406 \item $|\vec a|\leq i$ and $|\vec b|> i$: symmetric to the case above.
\r
407 \item $|\vec a|,|\vec b|> i$: \TODO use the lemma above
\r
408 plus another one. Reason on the numebr of arguments
\r
409 $\Args{\nf{a_i\sigma\vec\alpha}}$ vs
\r
410 $\Args{\nf{b_i\sigma\vec\alpha}}$.
\r
411 If equal conclude, otherwise conclude by lemma above.
\r
414 $h_1 = h_2$ and $|\vec a| = |\vec b|$
\r
415 but $a_n \EtaNeq b_n$ for some $n$.
\r
416 If $h_1=h_2\neq\var$, then again
\r
417 $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =%
\r
418 \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,
\r
419 and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that
\r
420 $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.
\r
421 {\color{red}[Capire se possiamo davvero usare l'\ih{} qui]}
\r
423 We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:
\r
425 \item $|\vec a| = |\vec b| \leq i$: \TODO easy
\r
426 \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok
\r
427 \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO
\r
428 by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$
\r
429 and conclude by appending the $\vec a$ and $\vec b$.
\r