From 20132867497f74bc0e2a2831fc7077b3678ae6a0 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 16 Jul 2018 10:19:07 +0100
Subject: [PATCH] Prime definizioni, verso prova correttezza nostro algoritmo

---
 macros.tex |  2 +-
 notes.tex  | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 70 insertions(+), 1 deletion(-)

diff --git a/macros.tex b/macros.tex
index d647af6..b9ac79d 100644
--- a/macros.tex
+++ b/macros.tex
@@ -4,7 +4,7 @@
 \newtheorem{theorem}{Theorem}
 \newtheorem{lemma}{Lemma}
 % \newtheorem{prop}[thm]{Proposition}
-% \newtheorem*{cor}{Corollary}
+\newtheorem{corollary}{Corollary}
 
 \theoremstyle{definition}
 \newtheorem{definition}{Definition}
diff --git a/notes.tex b/notes.tex
index 489869f..142ea4d 100644
--- a/notes.tex
+++ b/notes.tex
@@ -247,5 +247,74 @@
 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.
 %
 % \end{example}
+\clearpage
+\section{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}
+\newcommand{\perm}{\pi}
+\newcommand{\Perm}[2]{\pi[#1,#2]}
+\newcommand{\xK}{\kappa}
+\newcommand{\xN}{n}
+\newcommand{\LAM}[2]{\Lambda_{#2,#1}}
+\newcommand{\LAMNK}{\LAM\xN\xK}
+\newcommand{\Apply}[2]{(#1\mapsto#2)}
+\newcommand{\kn}{$(\kappa,n)$}
+\newcommand{\knnf}{\kn{}-nf}
+\newcommand{\Lams}[1]{\operatorname{lams}(#1)}
+\newcommand{\Args}[1]{\operatorname{args}(#1)}
+\newcommand{\Head}[1]{\operatorname{head}(#1)}
+\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}[\kn{}-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 (for $\xK,\xN$ natural numbers):
+  $\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{}.
+\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}
+
+\begin{definition}{$\Apply\cdot\cdot$}
+  We denote by $\tmtwo\Apply\var\tm$ the normal form of $\tmtwo\Subst\var\tm$ in normal form --
+  if it has one.
+\end{definition}
+
+\begin{lemma}
+  Let $\tm$ a \knnf, and $\Head\tm=\var$.
+  If $A\leq \Args\tm$ and $B \geq \xK + A + 1$,
+  let $\tmtwo\defeq\tm\Apply\var{\Perm{A}{B}}$ in:
+  $\Lams\tm=\Lams\tmtwo$ and $\tmtwo\in\LAM ? ?$
+\end{lemma}
+\begin{proof}
+  By induction on the normal form structure of $\tm$.
+  Let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$:
+  \begin{itemize}
+    \item if $\vartwo=\var$, then
+    $\tm\Apply\var\perm = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$
+    \item if $\vartwo\neq\var$, then $\tm\Apply\var\perm = \lambda\vec\var.\,\vartwo\,\vec\tmthree$
+    where $\vec\tmthree\defeq \vec\tmtwo\Apply\var\perm$.
+    Conclude by inductive hypothesis.
+  \end{itemize}
+\end{proof}
+\begin{corollary}
+  Let $\tm \defeq \var\,f_1\cdots f_m$ a \knnf.
+  If $A\leq m$ and $B \geq A + \xK$,
+  then $\tm\Apply\var{\Perm{A}{B}}$ is an inert.
+\end{corollary}
+
+\begin{lemma}
+  For every $\tm,\tmtwo$ be \knnf{s},
+  every fresh variable $\var$,
+  $\perm\defeq\Perm{i}{i+k+1}$ permutator,
+  $\tm\EtaEq\tmtwo$ iff $\tm\Apply\var\perm\EtaEq\tmtwo\Apply\var\perm$.
+\end{lemma}
 
 \end{document}
-- 
2.39.2