% Paths:\r
\newcommand{\PathEmpty}{\epsilon}\r
\newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}\r
-\newcommand{\PathArg}[3]{\mathtt{arg}_{#1}^{#2}(#3)}\r
+\newcommand{\PathArg}[3]{\mathtt{arg}_{#2}^{#1}(#3)}\r
\newcommand{\PathHd}{\mathtt{hd}}\r
\r
\newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}\r
\AC{\r
Given a path, one can retrieve from a term (if possible) the subterm at that position.\r
\r
- Since the path may go through abstraction, bound variables that become free\r
+ Since the path may go through abstractions, bound variables that become free\r
are renamed to variables of the form $\NamedBoundVar\pi$\r
(where $\pi$ is the path in the original inert leading to the abstraction binding that variable).\r
}\r
+ % \newcommand{\GetSubtm}[2]{\operatorname{GetSubtm}(#1\texttt{;}#2)}\r
+ \newcommand{\GetSubtm}[2]{{#1}_{#2}}\r
\[\begin{array}{ll}\r
- \tm_\pi & \defeq \tm_\pi^{\Box} \\\r
- t_{\PathEmpty}^{-} & \defeq t \\\r
- (x\,t_1\cdots t_n)_{\PathHd}^{-} & \defeq x \\\r
- (x\,t_1\cdots t_n)_{\PathArg i \var \pi}^{\rho} & \defeq\r
- (t_i)_\pi^{\rho[\PathArg i \var \Box]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
- (\lambda x.\, t)_{\PathAbs \pi}^{\rho} & \defeq t_\pi^{\rho[\PathAbs\Box]} \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
- (t)_{\PathAbs \pi}^{\rho} & \defeq (\lambda x.\, t\, x)_{\PathAbs \pi}^{\rho} \text{ (with } x \text{ fresh) (eta)}\\\r
+ \GetSubtm\tm\pi & \defeq \GetSubtm\tm{\underline\pi} \\\r
+ \GetSubtm\tm{\rho[\underline\PathEmpty]} & \defeq \tm \\\r
+ \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline\PathHd]} & \defeq x \\\r
+ \GetSubtm{(x\,t_1\cdots t_n)}{\rho[\underline{\PathArg i \var \pi}]} & \defeq\r
+ \GetSubtm{(t_i)}{\rho[\PathArg i \var {\underline\pi}]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
+ \GetSubtm{(\lambda x.\, t)}{\rho[\underline {\PathAbs \pi}]} & \defeq\r
+ \GetSubtm\tm{\rho(\PathAbs{\underline\pi})}\r
+ \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
+ \GetSubtm{\tm}{\rho(\underline{\PathAbs \pi})} &\r
+ \defeq \GetSubtm{(\lambda \var.\, \tm\,\var)}{\rho(\PathAbs {\underline\pi})} \text{ (with } x \text{ fresh) (eta)}\\\r
% \Omega_-^- & \defeq \Omega \\\r
\end{array}\]\r
\item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$\r
- \item \textbf{Distinction:} \underline{$S,R$ is $\Div$--distinct} iff:\r
- $S$ is empty, or there exists a path $\pi$ \emph{effective} for $\{\Div\}\cup \OfHead{\GarbageOf\Div}{\HeadOf\Div}$, s.t. EITHER:\r
+ \item \textbf{Telescopic garbage chain:} $\{\langle\tm_1,\pi_1\rangle,\ldots,\langle\tm_n,\pi_n\rangle\}$ is a $-$ if $\forall i$:\r
+ \[\tm_{i+1} \in \SubtmsOf{\text{garbage of } \GetSubtm{(\tm_i)}{\pi_i}}\]\r
+ \item \textbf{Distinction:} \underline{$S$ is $\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct} iff (one of the following three):\r
+ \begin{itemize}\r
+ \item $\OfHead S {\HeadOf \Div}$ is empty and $n=1$\r
+ \end{itemize}\r
+ OR: let $\Div\defeq\Div_1$ in:\r
\begin{itemize}\r
- \item $\forall \tm\in \OfHead{\SubtmsOf{\Div}}{\HeadOf\Div}$, $\tm_\pi$ is defined;\r
- % \item 1. $\exists s\in S$ s.t. $s \not\sim_\pi \Div$;\r
- \item $\{s\in S \mid s \sim_\pi \Div\},R$ is $\Div$--distinct.\r
+ \item there exists a path $\pi$ s.t.\r
+ \item (Effective) $\pi$ is \emph{effective} for all $\Div_i$ s.t. $\HeadOf{\Div_i} = \HeadOf{\Div}$\r
+ \item $\forall \tm\in \OfHead{\SubtmsOf{\Div_i}}{\HeadOf\Div}$, $\tm_\pi \neq \Omega$;\r
+ \item (Useful) $\exists s\in \OfHead S{\HeadOf\Div}$ s.t. $s \not\sim_\pi \Div$;\r
+ \item $S\setminus\{s\in \OfHead S{\HeadOf\Div} \mid s \not\sim_\pi \Div\}$ is $D$--distinct.\r
\end{itemize}\r
OR:\r
\begin{itemize}\r
- \item $\Div_\pi = \lambda\var.\, -, g$\r
- (note that $\Div$ has recursively only one garbage);\r
- % \item $\Div_\pi \neq \Omega$\r
- \item there is $\Div'\in\SubtmsOf g$ s.t.\r
- $S',R'$ is $\Div'$--distinct, where:\r
- $R'\defeq R\cup \bigcup\{\text{subtms of } s \text{ along } \pi \mid s\in S\}$ and\r
- $S' \defeq \OfHead{R'}{\HeadOf{\Div'}}$.\r
+ \item $S'$ is $\{\langle\Div_2,\pi_2\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$--distinct, where:\r
+ \[S' \defeq S \mathrel{\cup} \SubtmsOf{\{\text{garbage of } s \text{ along } \pi_1 \mid s\in \OfHead{S}{\HeadOf\Div}\}} \]\r
\end{itemize}\r
\r
\item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable\r
- IF $\OfHead{\SubtmsOf{\Conv}}{\HeadOf{\Div'}}, \SubtmsOf{\Conv}$ is $\Div'$--distinct for some $\Div'\in\SubtmsOf\Div$.\r
+ IFF there is $\Div_1$ (an $\Omega$--approximation of a subterm of $\Div$ with\r
+ at most one garbage, and without stuck variables)\r
+ and a telescopic garbage chain $D\defeq\{\langle\Div_1,\pi_1\rangle,\ldots,\langle\Div_n,\pi_n\rangle\}$ s.t.\r
+ $\SubtmsOf\Conv$ is $D$--distinct.\r
\r
\clearpage\r
\item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
% % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
%\r
% \end{example}\r
+\clearpage\r
+\section{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\r
+\newcommand{\perm}{\pi}\r
+\newcommand{\Perm}[2]{\pi[#1,#2]}\r
+\newcommand{\xK}{\kappa}\r
+\newcommand{\xN}{n}\r
+\newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
+\newcommand{\LAMNK}{\LAM\xN\xK}\r
+\newcommand{\Apply}[2]{(#1\mapsto#2)}\r
+\newcommand{\kn}{$(\kappa,n)$}\r
+\newcommand{\knnf}{\kn{}-nf}\r
+\newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
+\newcommand{\Args}[1]{\operatorname{args}(#1)}\r
+\newcommand{\Head}[1]{\operatorname{head}(#1)}\r
+\begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]\r
+ \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]\r
+ \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]\r
+ \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]\r
+\end{definition}\r
+\r
+\begin{definition}[\kn{}-normal forms]\r
+ First recall that terms in normal form have the shape\r
+ $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.\r
+ \r
+ We define inductively the set of \knnf s (for $\xK,\xN$ natural numbers):\r
+ $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
+ $|\vec\var|\leq\xK$, $|\vec\tm|\leq\xN$, and every term in $\vec\tm$ is a \knnf{}.\r
+\end{definition}\r
+\r
+\begin{definition}[Permutator $\Perm\cdot\cdot$]~\r
+ \[\Perm i j \defeq \lambda\vec\var\vartwo.\,\vartwo\, \vec\alpha\,\vec\var\,\vartwo\]\r
+ where $\vec\var$, $\vec\alpha$ and $\vartwo$ are fresh variables,\r
+ with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
+\end{definition}\r
+\r
+\begin{definition}{$\Apply\cdot\cdot$}\r
+ We denote by $\tmtwo\Apply\var\tm$ the normal form of $\tmtwo\Subst\var\tm$ in normal form --\r
+ if it has one.\r
+\end{definition}\r
+\r
+\begin{lemma}\r
+ Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
+ If $A\leq \Args\tm$ and $B \geq \xK + A + 1$,\r
+ let $\tmtwo\defeq\tm\Apply\var{\Perm{A}{B}}$ in:\r
+ $\Lams\tm=\Lams\tmtwo$ and $\tmtwo\in\LAM ? ?$\r
+\end{lemma}\r
+\begin{proof}\r
+ By induction on the normal form structure of $\tm$.\r
+ Let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$:\r
+ \begin{itemize}\r
+ \item if $\vartwo=\var$, then\r
+ $\tm\Apply\var\perm = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
+ \item if $\vartwo\neq\var$, then $\tm\Apply\var\perm = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
+ where $\vec\tmthree\defeq \vec\tmtwo\Apply\var\perm$.\r
+ Conclude by inductive hypothesis.\r
+ \end{itemize}\r
+\end{proof}\r
+\begin{corollary}\r
+ Let $\tm \defeq \var\,f_1\cdots f_m$ a \knnf.\r
+ If $A\leq m$ and $B \geq A + \xK$,\r
+ then $\tm\Apply\var{\Perm{A}{B}}$ is an inert.\r
+\end{corollary}\r
+\r
+\begin{lemma}\r
+ For every $\tm,\tmtwo$ be \knnf{s},\r
+ every fresh variable $\var$,\r
+ $\perm\defeq\Perm{i}{i+k+1}$ permutator,\r
+ $\tm\EtaEq\tmtwo$ iff $\tm\Apply\var\perm\EtaEq\tmtwo\Apply\var\perm$.\r
+\end{lemma}\r
\r
\end{document}\r
projects / fireball-separation.git / blobdiff