From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 12 Jun 2018 10:27:25 +0000 (+0200)
Subject: New ac's attempt at defining distinction with garbage
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22d8d52f5b9a6fa95ab31d585423af6a0b0a9e8c;p=fireball-separation.git

New ac's attempt at defining distinction with garbage
---

diff --git a/notes.tex b/notes.tex
index 084c9e2..4c1dd4f 100644
--- a/notes.tex
+++ b/notes.tex
@@ -43,10 +43,24 @@
 
 \clearpage
 \section*{Separation}
+% Paths:
+\newcommand{\PathEmpty}{\epsilon}
+\newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}
+\newcommand{\PathArg}[3]{\mathtt{arg}_{#1}^{#2}(#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 +74,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 +84,63 @@
     \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 abstraction, 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).
+  }
+  \[\begin{array}{ll}
+    \tm_\pi & \defeq \tm_\pi^{\Box} \\
+    t_{\PathEmpty}^{-} & \defeq t \\
+    (x\,t_1\cdots t_n)_{\PathHd}^{-} & \defeq x \\
+    (x\,t_1\cdots t_n)_{\PathArg i \var \pi}^{\rho} & \defeq
+      (t_i)_\pi^{\rho[\PathArg i \var \Box]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\
+    (\lambda x.\, t)_{\PathAbs \pi}^{\rho} & \defeq t_\pi^{\rho[\PathAbs\Box]} \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\
+    (t)_{\PathAbs \pi}^{\rho} & \defeq (\lambda x.\, t\, x)_{\PathAbs \pi}^{\rho} \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{Distinction:} \underline{$S,R$ is $\Div$--distinct} iff:
+   $S$ is empty, or there exists a path $\pi$ \emph{effective} for $\{\Div\}\cup \OfHead{\GarbageOf\Div}{\HeadOf\Div}$, s.t. EITHER:
+ \begin{itemize}
+   \item $\forall \tm\in \OfHead{\SubtmsOf{\Div}}{\HeadOf\Div}$, $\tm_\pi$ is defined;
+   % \item 1. $\exists s\in S$ s.t. $s \not\sim_\pi \Div$;
+   \item $\{s\in S \mid s \sim_\pi \Div\},R$ is $\Div$--distinct.
+ \end{itemize}
+ OR:
+\begin{itemize}
+   \item $\Div_\pi = \lambda\var.\, -, g$
+    (note that $\Div$ has recursively only one garbage);
+   % \item $\Div_\pi \neq \Omega$
+   \item there is $\Div'\in\SubtmsOf g$ s.t.
+    $S',R'$ is $\Div'$--distinct, where:
+    $R'\defeq R\cup \bigcup\{\text{subtms of } s \text{ along } \pi \mid s\in S\}$ and
+    $S' \defeq \OfHead{R'}{\HeadOf{\Div'}}$.
+ \end{itemize}
+
+ \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable
+  IF $\OfHead{\SubtmsOf{\Conv}}{\HeadOf{\Div'}}, \SubtmsOf{\Conv}$ is $\Div'$--distinct for some $\Div'\in\SubtmsOf\Div$.
+
+ \clearpage
  \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
  $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$