From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 4 Jun 2018 23:31:39 +0000 (+0200)
Subject: Thoughts on sigma-separation and a good sufficient condition
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=455ac21aa68fe367865c41c1883ae594c0c04b78;p=fireball-separation.git

Thoughts on sigma-separation and a good sufficient condition
---

diff --git a/ac_notes.tex b/ac_notes.tex
index 498812e..d8ff891 100644
--- a/ac_notes.tex
+++ b/ac_notes.tex
@@ -13,12 +13,12 @@
 
 \maketitle
 
-\newcommand{\Prgm}[2]{[#1\Comma #2]}
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
 
 \subparagraph{Syntax}
 \[\begin{array}{lll}
-  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \Prgm{\tm}{\vec\tm} \\
-  n & \ddef & \Lam\var \Prgm{n}{\vec n} \mid \var\,\vec n \\
+  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\
+  n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\
   \\
   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
   P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\
@@ -26,9 +26,9 @@
 
 \subparagraph{Reduction}
 \[\begin{array}{lll}
-  P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\in \Prgm\tm{\vec\tm}} &
+  P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &
    P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\
-   P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\Prgm\tm{\vec\tm}} &
+   P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &
     P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\
 \end{array}\]
 
@@ -38,6 +38,77 @@
   \item Ogni strategia e' perpetua!
 \end{itemize}
 
+\clearpage
+\[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]
+
+\begin{definition}[Unlockable variable]
+  A variable $\var$ is unlockable in a context $E$ if:
+  \begin{itemize}
+    \item it is not bound in $E$, or
+    \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$
+     and $\vartwo$ is unlockable in $E'$.
+  \end{itemize}
+\end{definition}
+
+\begin{lemma}[Elimination of unlockable variables]
+  For every set of terms $\tm_1, \ldots, \tm_n$
+  there exist terms $\tm'_1, \ldots, \tm'_n$
+  without unlockable variables and
+  such that $\tm_i$ is unseparable from $\tm'_i$.
+\end{lemma}
+
+{\color{red}
+ Non esattamente!
+ I termini hanno gli stessi path, e le variabili unlockable
+ del secondo sono iin path virtuali nel primo
+
+ Piu' esattamente, hai portato il garbage che vuoi far divergere
+  al top level.
+}
+
+\begin{definition}
+  Transformation removing an unlockable variable bound at position $\pi$:
+  \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]
+\end{definition}
+
+{\color{red}
+Warning! It creates unlockable variables, but in positions whose paths were
+previously virtual}
+
+\begin{lemma}
+  For every semi-$\sigma$-separable $\tm$ and $\tmtwo$,
+   there exist $\sigma$ s.t $\tm\sigma = \ldots \Comma C[i] \Comma \ldots$
+   and $i \not\preceq \tmtwo\sigma$ (and therefore, $\tm\sigma$ and $\tmtwo\sigma$
+   are semi-$\sigma$-separable by ???).
+\end{lemma}
+
+\begin{theorem}
+  $\tm$ and $\tmtwo$ are semi-$\sigma$-separable if \ldots
+\end{theorem}
+
+\clearpage
+\newcommand{\HeadOf}[1]{\operatorname{hd}(#1)}
+\newcommand{\ArityOf}[1]{\operatorname{len}(#1)}
+\begin{itemize}
+  \item \textbf{A sufficient condition for separability:}
+  \item \textbf{Goal.} semi-$\sigma$-separating $\tm$ from $\tmtwo$ (both inerts with pacmans/$\Omega$).
+  \item Let $U \defeq \{\tmtwo' \mid \tmtwo'\preceq\tmtwo \land \HeadOf{\tmtwo'}=\HeadOf{\tm}
+  \land \ArityOf{\tmtwo'} \leq \ArityOf{\tm}\} = \{u_1, \ldots, u_N\}$.
+  \item \textbf{Theorem.} The problem is separable if there exist $\pi_1\ldots\pi_N$
+  $\eta$-difference paths between
+  $\tm$ and $\tmtwo_1\ldots\tmtwo_N$ that are pairwise compatible on $\tm$ (note: also between themselves).
+  \item \textbf{Definition ($\eta$-difference path).}
+  \item \textbf{Definition ($\sqsubset$).} Initial fragments of paths
+   \item \textbf{Definition (Compatible paths).} ``$\pi_j$ is compatible with $\pi_i$ on $\tm$'' iff:
+    \[\forall\pi_i'\sqsubseteq\pi_i\text{ s.t. }\HeadOf{\pi_i'[t]} = \HeadOf{t}
+    \text{, then }\pi_j[\pi_i'[t]] \neq \Omega.\]
+  \item Resta da dimostrare che esista un modo di pre-processare i termini nostri
+   e ottenere degli inerti scelti.
+\end{itemize}
+
+
+
+
 \clearpage
 \section*{Syntactic Condition}