Tentative definition of unlockable variable

diff --git a/notes.tex b/notes.tex
index 1f3f2e548a000fffe8ebacd0498732b73918164a..084c9e2aefe5ad807d3211f60d6a11c21e394833 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -59,6 +59,7 @@
   % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms\r
    % (in deep normal form)\r
    \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.\r
+   \item \textbf{Subterm at position $\boldsymbol\pi$:} TODO\r
    \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.\r
   $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\r
   \begin{itemize}\r
@@ -68,15 +69,24 @@
     \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.\r
   \end{itemize}\r
 \r
- % \item \textbf{Unlockable variables.}\r
- %  We use the following contexts:\r
- %  $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
- % A variable $\var$ is \emph{unlockable} in a context $E$ if:\r
- %  \begin{itemize}\r
- %    \item it is not bound in $E$, or\r
- %    \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
- %     and $\vartwo$ is unlockable in $E'$.\r
- %  \end{itemize}\r
+ \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+\r
+ \item \textbf{Unlockable variables.}\r
+  We use the following contexts:\r
+  $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
+ A variable $\var$ is \emph{unlockable} in a context $E$ if:\r
+  \begin{itemize}\r
+    \item it is not bound in $E$, or\r
+    \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
+     and $\vartwo$ is unlockable in $E'$.\r
+  \end{itemize}\r
+\r
+  Transformation removing an unlockable variable bound at position $\pi$:\r
+  \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]\r
+\r
+  % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}\r
 \r
 \end{itemize}\r
 \r