X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ac_notes.tex;h=c214efe0d64c891643bbb083956f46c299db14ea;hb=afac35ce3b2f0240a762f51c3379ff4048233a0d;hp=d8ff891551cc1c7b5efa502e00e23dc437ab69cb;hpb=455ac21aa68fe367865c41c1883ae594c0c04b78;p=fireball-separation.git

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