\r
\maketitle\r
\r
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
+\r
\subparagraph{Syntax}\r
\[\begin{array}{lll}\r
- \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\\r
- n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\\r
+ \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\\r
+ n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\\r
\\\r
C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
- P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm \\\r
- \tilde P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\\r
+ P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\\r
\end{array}\]\r
\r
\subparagraph{Reduction}\r
\[\begin{array}{lll}\r
- P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} &\r
- P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\\r
- P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} &\r
- P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\\r
+ P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &\r
+ P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
+ P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &\r
+ P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
\end{array}\]\r
\r
\subparagraph{Properties of the calculus:}\r
\begin{itemize}\r
\item Every term is normalizing iff it is strongly normalizing.\r
+ \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
+\begin{definition}[Unlockable variable]\r
+ A variable $\var$ is 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
+\end{definition}\r
+\r
+\begin{lemma}[Elimination of unlockable variables]\r
+ For every set of terms $\tm_1, \ldots, \tm_n$\r
+ there exist terms $\tm'_1, \ldots, \tm'_n$\r
+ without unlockable variables and\r
+ such that $\tm_i$ is unseparable from $\tm'_i$.\r
+\end{lemma}\r
+\r
+{\color{red}\r
+ Non esattamente!\r
+ I termini hanno gli stessi path, e le variabili unlockable\r
+ del secondo sono iin path virtuali nel primo\r
+\r
+ Piu' esattamente, hai portato il garbage che vuoi far divergere\r
+ al top level.\r
+}\r
+\r
+\begin{definition}\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
+\end{definition}\r
+\r
+{\color{red}\r
+Warning! It creates unlockable variables, but in positions whose paths were\r
+previously virtual}\r
+\r
+\begin{lemma}\r
+ For every semi-$\sigma$-separable $\tm$ and $\tmtwo$,\r
+ there exist $\sigma$ s.t $\tm\sigma = \ldots \Comma C[i] \Comma \ldots$\r
+ and $i \not\preceq \tmtwo\sigma$ (and therefore, $\tm\sigma$ and $\tmtwo\sigma$\r
+ are semi-$\sigma$-separable by ???).\r
+\end{lemma}\r
+\r
+\begin{theorem}\r
+ $\tm$ and $\tmtwo$ are semi-$\sigma$-separable if \ldots\r
+\end{theorem}\r
+\r
+\clearpage\r
+\newcommand{\HeadOf}[1]{\operatorname{hd}(#1)}\r
+\newcommand{\ArityOf}[1]{\operatorname{len}(#1)}\r
+\begin{itemize}\r
+ \item \textbf{A sufficient condition for separability:}\r
+ \item \textbf{Goal.} semi-$\sigma$-separating $\tm$ from $\tmtwo$ (both inerts with pacmans/$\Omega$).\r
+ \item Let $U \defeq \{\tmtwo' \mid \tmtwo'\preceq\tmtwo \land \HeadOf{\tmtwo'}=\HeadOf{\tm}\r
+ \land \ArityOf{\tmtwo'} \leq \ArityOf{\tm}\} = \{u_1, \ldots, u_N\}$.\r
+ \item \textbf{Theorem.} The problem is separable if there exist $\pi_1\ldots\pi_N$\r
+ $\eta$-difference paths between\r
+ $\tm$ and $\tmtwo_1\ldots\tmtwo_N$ that are pairwise compatible on $\tm$ (note: also between themselves).\r
+ \item \textbf{Definition ($\eta$-difference path).}\r
+ \item \textbf{Definition ($\sqsubset$).} Initial fragments of paths\r
+ \item \textbf{Definition (Compatible paths).} ``$\pi_j$ is compatible with $\pi_i$ on $\tm$'' iff:\r
+ \[\forall\pi_i'\sqsubseteq\pi_i\text{ s.t. }\HeadOf{\pi_i'[t]} = \HeadOf{t}\r
+ \text{, then }\pi_j[\pi_i'[t]] \neq \Omega.\]\r
+ \item Resta da dimostrare che esista un modo di pre-processare i termini nostri\r
+ e ottenere degli inerti scelti.\r
+\end{itemize}\r
+\r
+\r
+\r
+\r
\clearpage\r
\section*{Syntactic Condition}\r
\r
projects / fireball-separation.git / blobdiff