From f76bc047c47f6b3aa36b579cb762cd46b2d8f083 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 7 Jun 2018 16:58:59 +0200
Subject: [PATCH] Tentative definition of unlockable variable

---
 notes.tex | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/notes.tex b/notes.tex
index 1f3f2e5..084c9e2 100644
--- a/notes.tex
+++ b/notes.tex
@@ -59,6 +59,7 @@
   % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms
    % (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 \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}
@@ -68,15 +69,24 @@
     \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.
   \end{itemize}
 
- % \item \textbf{Unlockable variables.}
- %  We use the following contexts:
- %  $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.
- % A variable $\var$ is \emph{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}
+ \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$
+
+ \item \textbf{Unlockable variables.}
+  We use the following contexts:
+  $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.
+ A variable $\var$ is \emph{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}
+
+  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])\]
+
+  % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}
 
 \end{itemize}
 
-- 
2.39.2