From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 8 Jun 2018 21:41:12 +0000 (+0200)
Subject: Tentative definitions of variable names and variable paths
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f71a3f5d3a1e74f6b28d63362c6aef3ba543ab6b;p=fireball-separation.git

Tentative definitions of variable names and variable paths
---

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} \]