Yet another attempt at defining distinction with garbage

diff --git a/notes.tex b/notes.tex
index 4c1dd4f3ad7280a64590306f25e22bca2577ef44..489869f7e450c2afb956655ea94c8a1887343ac5 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -46,7 +46,7 @@
 % Paths:\r
 \newcommand{\PathEmpty}{\epsilon}\r
 \newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}\r
-\newcommand{\PathArg}[3]{\mathtt{arg}_{#1}^{#2}(#3)}\r
+\newcommand{\PathArg}[3]{\mathtt{arg}_{#2}^{#1}(#3)}\r
 \newcommand{\PathHd}{\mathtt{hd}}\r
 \r
 \newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}\r
@@ -104,41 +104,51 @@
   \AC{\r
    Given a path, one can retrieve from a term (if possible) the subterm at that position.\r
 \r
-   Since the path may go through abstraction, bound variables that become free\r
+   Since the path may go through abstractions, bound variables that become free\r
    are renamed to variables of the form $\NamedBoundVar\pi$\r
    (where $\pi$ is the path in the original inert leading to the abstraction binding that variable).\r
   }\r
+  % \newcommand{\GetSubtm}[2]{\operatorname{GetSubtm}(#1\texttt{;}#2)}\r
+  \newcommand{\GetSubtm}[2]{{#1}_{#2}}\r
   \[\begin{array}{ll}\r
-    \tm_\pi & \defeq \tm_\pi^{\Box} \\\r
-    t_{\PathEmpty}^{-} & \defeq t \\\r
-    (x\,t_1\cdots t_n)_{\PathHd}^{-} & \defeq x \\\r
-    (x\,t_1\cdots t_n)_{\PathArg i \var \pi}^{\rho} & \defeq\r
-      (t_i)_\pi^{\rho[\PathArg i \var \Box]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
-    (\lambda x.\, t)_{\PathAbs \pi}^{\rho} & \defeq t_\pi^{\rho[\PathAbs\Box]} \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
-    (t)_{\PathAbs \pi}^{\rho} & \defeq (\lambda x.\, t\, x)_{\PathAbs \pi}^{\rho} \text{ (with } x \text{ fresh) (eta)}\\\r
+    \GetSubtm\tm\pi & \defeq \GetSubtm\tm{\underline\pi} \\\r
+    \GetSubtm\tm{\rho[\underline\PathEmpty]} & \defeq \tm \\\r
+    \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline\PathHd]} & \defeq x \\\r
+    \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline{\PathArg i \var \pi}]} & \defeq\r
+      \GetSubtm{(t_i)}{\rho[\PathArg i \var {\underline\pi}]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
+    \GetSubtm{(\lambda x.\, t)}{\rho[\underline {\PathAbs \pi}]} & \defeq\r
+     \GetSubtm\tm{\rho(\PathAbs{\underline\pi})}\r
+     \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
+    \GetSubtm{\tm}{\rho(\underline{\PathAbs \pi})} &\r
+     \defeq \GetSubtm{(\lambda \var.\, \tm\,\var)}{\rho(\PathAbs {\underline\pi})} \text{ (with } x \text{ fresh) (eta)}\\\r
     % \Omega_-^- & \defeq \Omega \\\r
   \end{array}\]\r
   \item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$\r
-  \item \textbf{Distinction:} \underline{$S,R$ is $\Div$--distinct} iff:\r
-   $S$ is empty, or there exists a path $\pi$ \emph{effective} for $\{\Div\}\cup \OfHead{\GarbageOf\Div}{\HeadOf\Div}$, s.t. EITHER:\r
+  \item \textbf{Telescopic garbage chain:} $\{\langle\tm_1,\pi_1\rangle,\ldots,\langle\tm_n,\pi_n\rangle\}$ is a $-$ if $\forall i$:\r
+   \[\tm_{i+1} \in \SubtmsOf{\text{garbage of } \GetSubtm{(\tm_i)}{\pi_i}}\]\r
+  \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
+  \begin{itemize}\r
+    \item $\OfHead S {\HeadOf \Div}$ is empty and $n=1$\r
+  \end{itemize}\r
+   OR: let $\Div\defeq\Div_1$ in:\r
  \begin{itemize}\r
-   \item $\forall \tm\in \OfHead{\SubtmsOf{\Div}}{\HeadOf\Div}$, $\tm_\pi$ is defined;\r
-   % \item 1. $\exists s\in S$ s.t. $s \not\sim_\pi \Div$;\r
-   \item $\{s\in S \mid s \sim_\pi \Div\},R$ is $\Div$--distinct.\r
+   \item there exists a path $\pi$ s.t.\r
+   \item (Effective) $\pi$ is \emph{effective} for all $\Div_i$ s.t. $\HeadOf{\Div_i} = \HeadOf{\Div}$\r
+   \item $\forall \tm\in \OfHead{\SubtmsOf{\Div_i}}{\HeadOf\Div}$, $\tm_\pi \neq \Omega$;\r
+   \item (Useful) $\exists s\in \OfHead S{\HeadOf\Div}$ s.t. $s \not\sim_\pi \Div$;\r
+   \item $S\setminus\{s\in \OfHead S{\HeadOf\Div} \mid s \not\sim_\pi \Div\}$ is $D$--distinct.\r
  \end{itemize}\r
  OR:\r
 \begin{itemize}\r
-   \item $\Div_\pi = \lambda\var.\, -, g$\r
-    (note that $\Div$ has recursively only one garbage);\r
-   % \item $\Div_\pi \neq \Omega$\r
-   \item there is $\Div'\in\SubtmsOf g$ s.t.\r
-    $S',R'$ is $\Div'$--distinct, where:\r
-    $R'\defeq R\cup \bigcup\{\text{subtms of } s \text{ along } \pi \mid s\in S\}$ and\r
-    $S' \defeq \OfHead{R'}{\HeadOf{\Div'}}$.\r
+   \item $S'$ is $\{\langle\Div_2,\pi_2\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct, where:\r
+    \[S' \defeq S \mathrel{\cup} \SubtmsOf{\{\text{garbage of } s \text{ along } \pi_1 \mid s\in \OfHead{S}{\HeadOf\Div}\}} \]\r
  \end{itemize}\r
 \r
  \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable\r
-  IF $\OfHead{\SubtmsOf{\Conv}}{\HeadOf{\Div'}}, \SubtmsOf{\Conv}$ is $\Div'$--distinct for some $\Div'\in\SubtmsOf\Div$.\r
+  IFF there is $\Div_1$ (an $\Omega$--approximation of a subterm of $\Div$ with\r
+  at most one garbage, and without stuck variables)\r
+  and a telescopic garbage chain $D\defeq\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$ s.t.\r
+  $\SubtmsOf\Conv$ is $D$--distinct.\r
 \r
  \clearpage\r
  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r