Prime definizioni, verso prova correttezza nostro algoritmo

diff --git a/macros.tex b/macros.tex
index d647af67476a2bfd61f963778cc5f090651b88be..b9ac79db7aa8a76f8fc98d17e807f0a5a6c616af 100644 (file)
--- a/macros.tex
+++ b/macros.tex
@@ -4,7 +4,7 @@
 \newtheorem{theorem}{Theorem}\r
 \newtheorem{lemma}{Lemma}\r
 % \newtheorem{prop}[thm]{Proposition}\r
-% \newtheorem*{cor}{Corollary}\r
+\newtheorem{corollary}{Corollary}\r
 \r
 \theoremstyle{definition}\r
 \newtheorem{definition}{Definition}\r

diff --git a/notes.tex b/notes.tex
index 489869f7e450c2afb956655ea94c8a1887343ac5..142ea4dfab5ea2181b134f19829434398608d0ac 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -247,5 +247,74 @@
 % % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
 %\r
 % \end{example}\r
+\clearpage\r
+\section{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\r
+\newcommand{\perm}{\pi}\r
+\newcommand{\Perm}[2]{\pi[#1,#2]}\r
+\newcommand{\xK}{\kappa}\r
+\newcommand{\xN}{n}\r
+\newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
+\newcommand{\LAMNK}{\LAM\xN\xK}\r
+\newcommand{\Apply}[2]{(#1\mapsto#2)}\r
+\newcommand{\kn}{$(\kappa,n)$}\r
+\newcommand{\knnf}{\kn{}-nf}\r
+\newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
+\newcommand{\Args}[1]{\operatorname{args}(#1)}\r
+\newcommand{\Head}[1]{\operatorname{head}(#1)}\r
+\begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]\r
+  \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]\r
+  \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]\r
+  \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]\r
+\end{definition}\r
+\r
+\begin{definition}[\kn{}-normal forms]\r
+  First recall that terms in normal form have the shape\r
+  $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.\r
+  \r
+  We define inductively the set of \knnf s (for $\xK,\xN$ natural numbers):\r
+  $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
+  $|\vec\var|\leq\xK$, $|\vec\tm|\leq\xN$, and every term in $\vec\tm$ is a \knnf{}.\r
+\end{definition}\r
+\r
+\begin{definition}[Permutator $\Perm\cdot\cdot$]~\r
+  \[\Perm i j \defeq \lambda\vec\var\vartwo.\,\vartwo\, \vec\alpha\,\vec\var\,\vartwo\]\r
+  where $\vec\var$, $\vec\alpha$ and $\vartwo$ are fresh variables,\r
+  with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
+\end{definition}\r
+\r
+\begin{definition}{$\Apply\cdot\cdot$}\r
+  We denote by $\tmtwo\Apply\var\tm$ the normal form of $\tmtwo\Subst\var\tm$ in normal form --\r
+  if it has one.\r
+\end{definition}\r
+\r
+\begin{lemma}\r
+  Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
+  If $A\leq \Args\tm$ and $B \geq \xK + A + 1$,\r
+  let $\tmtwo\defeq\tm\Apply\var{\Perm{A}{B}}$ in:\r
+  $\Lams\tm=\Lams\tmtwo$ and $\tmtwo\in\LAM ? ?$\r
+\end{lemma}\r
+\begin{proof}\r
+  By induction on the normal form structure of $\tm$.\r
+  Let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$:\r
+  \begin{itemize}\r
+    \item if $\vartwo=\var$, then\r
+    $\tm\Apply\var\perm = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
+    \item if $\vartwo\neq\var$, then $\tm\Apply\var\perm = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
+    where $\vec\tmthree\defeq \vec\tmtwo\Apply\var\perm$.\r
+    Conclude by inductive hypothesis.\r
+  \end{itemize}\r
+\end{proof}\r
+\begin{corollary}\r
+  Let $\tm \defeq \var\,f_1\cdots f_m$ a \knnf.\r
+  If $A\leq m$ and $B \geq A + \xK$,\r
+  then $\tm\Apply\var{\Perm{A}{B}}$ is an inert.\r
+\end{corollary}\r
+\r
+\begin{lemma}\r
+  For every $\tm,\tmtwo$ be \knnf{s},\r
+  every fresh variable $\var$,\r
+  $\perm\defeq\Perm{i}{i+k+1}$ permutator,\r
+  $\tm\EtaEq\tmtwo$ iff $\tm\Apply\var\perm\EtaEq\tmtwo\Apply\var\perm$.\r
+\end{lemma}\r
 \r
 \end{document}\r