X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=notes.tex;h=264e827a00f9dda3ab29415e7654e6a6a5778b5d;hb=7b8e2259f217ba34f4d8871eca4fc7b79791d13a;hp=084c9e2aefe5ad807d3211f60d6a11c21e394833;hpb=f76bc047c47f6b3aa36b579cb762cd46b2d8f083;p=fireball-separation.git

diff --git a/notes.tex b/notes.tex
index 084c9e2..264e827 100644
--- a/notes.tex
+++ b/notes.tex
@@ -1,16 +1,8 @@
 \documentclass[12pt]{article}
-\usepackage{blindtext}
-\usepackage{enumerate}
-\usepackage{hyperref, bookmark}
-\usepackage{amsmath, amsfonts, amssymb, amsthm}
-\usepackage{xcolor}
-
 \title{Strong Separation}
 % \author{---}
 \date{\vspace{-2em}\today{}}
-
 \input{macros}
-\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
 
 \begin{document}
 
@@ -43,10 +35,24 @@
 
 \clearpage
 \section*{Separation}
+% Paths:
+\newcommand{\PathEmpty}{\epsilon}
+\newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}
+\newcommand{\PathArg}[3]{\mathtt{arg}_{#2}^{#1}(#3)}
+\newcommand{\PathHd}{\mathtt{hd}}
+
+\newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}
 \newcommand{\HeadOf}[1]{\operatorname{head}(#1)}
 \newcommand{\FstOf}[1]{\operatorname{fst}(#1)}
 \newcommand{\DegOf}[1]{\operatorname{deg}(#1)}
 \newcommand{\SubtmOf}[2]{#1\preceq #2}
+\newcommand{\OfHead}[2]{#1_{{\mid}#2}}
+\newcommand{\SubtmsOf}[1]{\operatorname{Sub}(#1)}
+\newcommand{\Div}{\mathtt{d}}
+\newcommand{\Conv}{\mathtt{c}}
+\newcommand{\Const}{\mathtt{K}}
+\newcommand{\NamedBoundVar}[1]{\texttt{bvar(}#1\texttt{)}}
+\newcommand{\AC}[1]{{\color{violet}#1}}
 \begin{itemize}
   % \item \textbf{$\boldsymbol\sigma$-separation.}
   %  \textcolor{red}{come definirlo? con le variabili? con i termini?
@@ -60,6 +66,7 @@
    % (in deep normal form)
    \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.
    \item \textbf{Subterm at position $\boldsymbol\pi$:} TODO
+   \item $\boldsymbol\sim_{\boldsymbol\pi}$
    \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.
   $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:
   \begin{itemize}
@@ -69,6 +76,73 @@
     \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.
   \end{itemize}
 
+\clearpage
+  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
+  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
+  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
+  \texttt{ prove di nuove definizioni di ac:}
+
+  \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$
+  \[\begin{array}{ll}
+    \SubtmsOf{\var} & \defeq \{\var\} \\
+    \SubtmsOf{\tm\,\tmtwo} & \defeq \SubtmsOf\tm \cup \SubtmsOf\tmtwo \cup \{\tm\,\tmtwo\} \\
+    \SubtmsOf{\lambda \var.\, \vec\tm} & \defeq \{\tmtwo\{\Const/\var\} \mid \tmtwo \in\SubtmsOf{\vec\tm}\} \\
+  \end{array}\]
+  \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}
+  \item \textbf{Subterm at position:}
+  \[\begin{array}{ll}
+    \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi
+  \end{array}\]
+  \AC{
+   Given a path, one can retrieve from a term (if possible) the subterm at that position.
+
+   Since the path may go through abstractions, bound variables that become free
+   are renamed to variables of the form $\NamedBoundVar\pi$
+   (where $\pi$ is the path in the original inert leading to the abstraction binding that variable).
+  }
+  % \newcommand{\GetSubtm}[2]{\operatorname{GetSubtm}(#1\texttt{;}#2)}
+  \newcommand{\GetSubtm}[2]{{#1}_{#2}}
+  \[\begin{array}{ll}
+    \GetSubtm\tm\pi & \defeq \GetSubtm\tm{\underline\pi} \\
+    \GetSubtm\tm{\rho[\underline\PathEmpty]} & \defeq \tm \\
+    \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline\PathHd]} & \defeq x \\
+    \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline{\PathArg i \var \pi}]} & \defeq
+      \GetSubtm{(t_i)}{\rho[\PathArg i \var {\underline\pi}]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\
+    \GetSubtm{(\lambda x.\, t)}{\rho[\underline {\PathAbs \pi}]} & \defeq
+     \GetSubtm\tm{\rho(\PathAbs{\underline\pi})}
+     \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\
+    \GetSubtm{\tm}{\rho(\underline{\PathAbs \pi})} &
+     \defeq \GetSubtm{(\lambda \var.\, \tm\,\var)}{\rho(\PathAbs {\underline\pi})} \text{ (with } x \text{ fresh) (eta)}\\
+    % \Omega_-^- & \defeq \Omega \\
+  \end{array}\]
+  \item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$
+  \item \textbf{Telescopic garbage chain:} $\{\langle\tm_1,\pi_1\rangle,\ldots,\langle\tm_n,\pi_n\rangle\}$ is a $-$ if $\forall i$:
+   \[\tm_{i+1} \in \SubtmsOf{\text{garbage of } \GetSubtm{(\tm_i)}{\pi_i}}\]
+  \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):
+  \begin{itemize}
+    \item $\OfHead S {\HeadOf \Div}$ is empty and $n=1$
+  \end{itemize}
+   OR: let $\Div\defeq\Div_1$ in:
+ \begin{itemize}
+   \item there exists a path $\pi$ s.t.
+   \item (Effective) $\pi$ is \emph{effective} for all $\Div_i$ s.t. $\HeadOf{\Div_i} = \HeadOf{\Div}$
+   \item $\forall \tm\in \OfHead{\SubtmsOf{\Div_i}}{\HeadOf\Div}$, $\tm_\pi \neq \Omega$;
+   \item (Useful) $\exists s\in \OfHead S{\HeadOf\Div}$ s.t. $s \not\sim_\pi \Div$;
+   \item $S\setminus\{s\in \OfHead S{\HeadOf\Div} \mid s \not\sim_\pi \Div\}$ is $D$--distinct.
+ \end{itemize}
+ OR:
+\begin{itemize}
+   \item $S'$ is $\{\langle\Div_2,\pi_2\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct, where:
+    \[S' \defeq S \mathrel{\cup} \SubtmsOf{\{\text{garbage of } s \text{ along } \pi_1 \mid s\in \OfHead{S}{\HeadOf\Div}\}} \]
+ \end{itemize}
+
+ \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable
+  IFF there is $\Div_1$ (an $\Omega$--approximation of a subterm of $\Div$ with
+  at most one garbage, and without stuck variables)
+  and a telescopic garbage chain $D\defeq\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$ s.t.
+  $\SubtmsOf\Conv$ is $D$--distinct.
+
+ \clearpage
  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
@@ -165,5 +239,195 @@
 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.
 %
 % \end{example}
+\clearpage
+\section[Tentativi X-separability]{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}
+\newcommand{\perm}{p}
+\newcommand{\Perm}[2]{\operatorname{P}[#1,#2]}
+\newcommand{\xK}{\kappa}
+\newcommand{\xN}{n}
+\newcommand{\LAM}[2]{\Lambda_{#2,#1}}
+\newcommand{\LAMNK}{\LAM\xN\xK}
+% \newcommand{\kn}{$(\kappa,n)$}
+\newcommand{\knnf}{$\xK{}$-nf}
+\newcommand{\Lams}[1]{\operatorname{lams}(#1)}
+\newcommand{\Args}[1]{\operatorname{args}(#1)}
+\newcommand{\Head}[1]{\operatorname{head}(#1)}
+\newcommand{\nf}[1]{#1{\downarrow}}
+\newcommand{\Nat}{\mathbb{N}}
+\begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]
+  \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]
+  \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]
+  \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]
+\end{definition}
+
+\begin{definition}[$\xK$-normal forms]
+  First recall that terms in normal form have the shape
+  $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.
+  
+  We define inductively the set of \knnf s (where $\xK$ is a natural number):
+  $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff 
+  $|\vec\var|\leq\xK$%
+  %, $|\vec\tm|\leq\xN$
+  , and every term in $\vec\tm$ is a \knnf{} as well.
+\end{definition}
+
+\begin{definition}[Normal form $\nf\cdot$]
+  
+\end{definition}
+
+\begin{definition}[Permutator $\Perm\cdot\cdot$]~
+  \[\Perm i j \defeq \lambda\vec\var\vartwo.\,\vartwo\, \vec\alpha\,\vec\var\,\vartwo\]
+  where $\vec\var$, $\vec\alpha$ and $\vartwo$ are fresh variables,
+  with $|\vec\var| = i$ and $|\vec\alpha| = j$.
+\end{definition}
+
+{\color{yellow}\begin{definition}[Good permutation]
+  Let $\tm$ a \knnf.
+  $\Perm i j$ is \emph{good} for $\tm$ if
+  $i<\Args\tm$ and $j \geq \xK + i + 1$.
+\end{definition}}
+
+% \begin{lemma}
+%   Let $\tm$ in nf.
+%   Let $\vec\alpha$ fresh variables.
+%   If $|\vec\alpha|\geq \lams\tm$,
+%   then the normal form of $\tm\,\vec\alpha$ is inert.
+% \end{lemma}
+
+\begin{lemma}[Monotonicity]\label{l:k-nf-mono}
+  If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf
+  for every $\xK' \geq \xK{}$.
+\end{lemma}
+
+\begin{lemma}\label{l:k-prime-nf}
+  Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$.
+  Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.
+\end{lemma}
+\begin{proof}
+  By (course-of-value) structural induction on $\tm$.
+  Let $\tm=\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo$ and $\sigma\defeq\Subst\var{\Perm i j}$.
+  By cases:
+  \begin{itemize}
+    \item Case $\varthree\neq\var$: $\nf{(\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo)\sigma} = \lambda\vec\vartwo.\,\varthree\,\vec{(\nf{\tmtwo\sigma})}$.
+    By \ih{} each term in $\vec{(\nf{\tmtwo\sigma})}$ is a $\xK'$-nf.
+    We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.
+    \item Case $\varthree=\var$ and $i<|\vec\tmtwo|$:
+     $\tm\sigma \to^* \lambda\vec\vartwo.\, (\tmtwo_i\sigma)\vec\alpha \vec{(\tmtwo\sigma)} $.
+     Now, by \ih{} $\nf{\tmtwo_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,
+     $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert (\textcolor{red}{Serve lemma?}).
+     Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \vec{(\nf{\tmtwo\sigma})}$,
+     and again by \ih{} it is also a $\xK'$-nf.
+    \item Case $\varthree=\var$ and $i \geq |\vec\tmtwo|$:
+    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for 
+    $|\vec\varthree| = i - |\vec\tmtwo|$.
+    Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.
+  \end{itemize}
+  
+\end{proof}
+
+% \begin{lemma}
+%   Let $\tm$ a \knnf, and $\Head\tm=\var$.
+%   If $i<\Args\tm$ and $j \geq \xK + i + 1$,
+%   then $\tmtwo\defeq\nf{\tm\Subst\var{\Perm i j}}$ is defined;
+%   $\Lams\tm=\Lams{\tmtwo}$; $\tmtwo$ is a $(j,\xN + j)$-nf.
+% \end{lemma}
+% \begin{proof}\color{red}\TODO{}
+%   By induction on the normal form structure of $\tm$:
+%   let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$.
+%   By \ih{}, $\nf{\tmtwo\Subst\var\perm}$ are $(j,\xN+j)$-nfs.
+%   \begin{itemize}
+%     \item if $\vartwo=\var$, then
+%     $\nf{\tm\Subst\var\perm} = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$
+%     \item if $\vartwo\neq\var$, then $\nf{\tm\Subst\var\perm} = \lambda\vec\var.\,\vartwo\,\vec\tmthree$
+%     where $\vec\tmthree\defeq \nf{\vec\tmtwo\Subst\var\perm}$.
+%     Conclude by inductive hypothesis.
+%   \end{itemize}
+% \end{proof}
+
+
+\begin{lemma}
+  For every \knnf s $\tm$,
+  every fresh variable $\var$,
+  every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:
+  $\nf{\tm\Subst\var\perm\vec\alpha} \EtaNeq \alpha_j$.
+\end{lemma}
+\begin{proof}
+  First of all note that by \reflemma{k-prime-nf}
+  $\nf{\tm\Subst\var\perm}$ is a $\xK'$-nf for $\xK' \defeq \xK+i+1$, therefore
+  $\nf{\tm\Subst\var\perm\vec\alpha}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.
+  
+  By structural induction on $\tm$.
+  Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.
+  \TODO{}
+\end{proof}
+
+% TODO: $\xK$-standard proof of $\eta$.
+
+\begin{lemma}
+  For every \knnf s $\tm$ and $\tmtwo$,
+  every fresh variable $\var$,
+  $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$,
+  $\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.
+\end{lemma}
+\begin{proof}
+  Let $\sigma \defeq \Subst\var\perm$.
+  First of all, note that by \reflemma{k-prime-nf}
+  $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and
+  are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$.
+  
+  If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$.
+  Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that
+  $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.
+  Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and 
+  $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,
+  with $|\vec\vartwo| = \xK$.
+  By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,
+  and by cases on the definition of eta-difference:
+  \begin{itemize}
+    \item $h_1 \neq h_2$: we distinguish three subcases.
+    \begin{itemize}
+      \item $h_1,h_2\neq \var$:
+       it follows that $\nf{\tm\sigma} = \nf{(\lambda\vec\vartwo.\,h_1\,\vec a)\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$
+       and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,
+       and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because
+       their head variables are different.
+      \item $h_1=\var$ and $h_2\neq \var$: \TODO
+      \item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.
+    \end{itemize}
+    \item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:
+     if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$
+     and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,
+     and we conclude because the two terms have a different number of arguments.
+     
+     We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:
+     \begin{itemize}
+       \item Both $|\vec a|,|\vec b|\leq i$: \TODO
+       \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO
+       \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above
+       plus another one. Reason on the numebr of arguments
+       $\Args{\nf{a_i\sigma\vec\alpha}}$ vs  
+       $\Args{\nf{b_i\sigma\vec\alpha}}$.
+       If equal conclude, otherwise conclude by lemma above.
+     \end{itemize}
+    \item 
+    $h_1 = h_2$ and $|\vec a| = |\vec b|$
+    but $a_n \EtaNeq b_n$ for some $n$.
+    If $h_1=h_2\neq\var$, then again
+    $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =%
+    \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,
+    and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that 
+    $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.
+    {\color{red}[Can we use the \ih{} here?]}
+    
+    We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:
+    \begin{itemize}
+      \item $|\vec a| = |\vec b| \leq i$: \TODO easy 
+      \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok
+      \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO
+       by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$
+       and conclude by appending the $\vec a$ and $\vec b$.
+    \end{itemize}
+  \end{itemize}
+\end{proof}
 
 \end{document}