Tentative definitions of variable names and variable paths

diff --git a/ac_notes.tex b/ac_notes.tex
index d8ff891551cc1c7b5efa502e00e23dc437ab69cb..c214efe0d64c891643bbb083956f46c299db14ea 100644 (file)
--- a/ac_notes.tex
+++ b/ac_notes.tex
@@ -38,6 +38,45 @@
   \item Ogni strategia e' perpetua!\r
 \end{itemize}\r
 \r
+\clearpage\r
+\r
+\[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]\r
+\r
+\begin{definition}{Path of a hole}\r
+  \[\begin{array}{ll}\r
+    \pi_\Box & \defeq \langle\rangle \\\r
+    \pi_{\Lam{\vec\var}{\vec i \Comma y \, }y\, \vec t E \vec s} & \defeq \\\r
+  \end{array}\]\r
+\end{definition}\r
+\r
+\newcommand{\NameOf}[2]{\operatorname{name}_{#2}(#1)}\r
+\begin{definition}[Name of a variable]~\r
+  \begin{itemize}\r
+    \item If $\var$ is free in $\tm$, then $\NameOf\var\tm = ``\var"$;\r
+    \item {\color{red} If $x$ is bound at the outer layer of a garbage, then\r
+     $\NameOf\var\tm = \Omega$;}\r
+    \item\r
+    If $ x\, \vec s \, (\lambda \vec y.\, \ldots) \preceq t$, then\r
+    $ \NameOf{\vartwo_i}{\tm} \defeq \NameOf\var\tm ; (|\vec s|, i) $.\r
+  \end{itemize}\r
+\end{definition}\r
+\r
+\begin{example}\r
+  \[\begin{array}{ll}\r
+  D & x \, a \, (\Lam\vartwo {y \Comma y\, b} ) \\\r
+  C & x \, a \, (\Lam\vartwo{y \Comma y \,b'}) \\\r
+  C & x \, a' \, (\Lam\vartwo{y \Comma y \,b }) \\\r
+  \end{array}\]\r
+\r
+  \[\begin{array}{ll}\r
+  D & y^{[x \, a \, \Omega]} \, b \\\r
+  C & y^{[x \, a \, \Omega]} \, b' \\\r
+  C & y^{[x \, a' \, \Omega]} \, b \\\r
+  \end{array}\]\r
+\end{example}\r
+\r
+\r
+\r
 \clearpage\r
 \[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]\r
 \r