\documentclass[12pt]{article}\r
-\usepackage{blindtext}\r
-\usepackage{enumerate}\r
-\usepackage{hyperref, bookmark}\r
-\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
-\usepackage{xcolor}\r
-\r
\title{Strong Separation}\r
% \author{---}\r
\date{\vspace{-2em}\today{}}\r
-\r
\input{macros}\r
-\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
\r
\begin{document}\r
\r
\r
\clearpage\r
\section*{Separation}\r
+% Paths:\r
+\newcommand{\PathEmpty}{\epsilon}\r
+\newcommand{\PathAbs}[1]{\mathtt{abs}(#1)}\r
+\newcommand{\PathArg}[3]{\mathtt{arg}_{#2}^{#1}(#3)}\r
+\newcommand{\PathHd}{\mathtt{hd}}\r
+\r
+\newcommand{\GarbageOf}[1]{\operatorname{Garb}(#1)}\r
\newcommand{\HeadOf}[1]{\operatorname{head}(#1)}\r
\newcommand{\FstOf}[1]{\operatorname{fst}(#1)}\r
\newcommand{\DegOf}[1]{\operatorname{deg}(#1)}\r
\newcommand{\SubtmOf}[2]{#1\preceq #2}\r
+\newcommand{\OfHead}[2]{#1_{{\mid}#2}}\r
+\newcommand{\SubtmsOf}[1]{\operatorname{Sub}(#1)}\r
+\newcommand{\Div}{\mathtt{d}}\r
+\newcommand{\Conv}{\mathtt{c}}\r
+\newcommand{\Const}{\mathtt{K}}\r
+\newcommand{\NamedBoundVar}[1]{\texttt{bvar(}#1\texttt{)}}\r
+\newcommand{\AC}[1]{{\color{violet}#1}}\r
\begin{itemize}\r
% \item \textbf{$\boldsymbol\sigma$-separation.}\r
% \textcolor{red}{come definirlo? con le variabili? con i termini?\r
% \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms\r
% (in deep normal form)\r
\item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$.\r
+ \item \textbf{Subterm at position $\boldsymbol\pi$:} TODO\r
+ \item $\boldsymbol\sim_{\boldsymbol\pi}$\r
\item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$.\r
$C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.:\r
\begin{itemize}\r
\item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct.\r
\end{itemize}\r
\r
- % \item \textbf{Unlockable variables.}\r
- % We use the following contexts:\r
- % $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
- % A variable $\var$ is \emph{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
+\clearpage\r
+ \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ \texttt{ prove di nuove definizioni di ac:}\r
+\r
+ \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$\r
+ \[\begin{array}{ll}\r
+ \SubtmsOf{\var} & \defeq \{\var\} \\\r
+ \SubtmsOf{\tm\,\tmtwo} & \defeq \SubtmsOf\tm \cup \SubtmsOf\tmtwo \cup \{\tm\,\tmtwo\} \\\r
+ \SubtmsOf{\lambda \var.\, \vec\tm} & \defeq \{\tmtwo\{\Const/\var\} \mid \tmtwo \in\SubtmsOf{\vec\tm}\} \\\r
+ \end{array}\]\r
+ \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}\r
+ \item \textbf{Subterm at position:}\r
+ \[\begin{array}{ll}\r
+ \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi\r
+ \end{array}\]\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 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
+ \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{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 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 $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
+ 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
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+\r
+ \item \textbf{Unlockable variables.}\r
+ We use the following contexts:\r
+ $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $.\r
+ A variable $\var$ is \emph{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
+\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
+\r
+ % \textcolor{red}{For every term there exists an equivalent term with no unlockable variables}\r
\r
\end{itemize}\r
\r
% % Where $\Pacman \equiv \lambda\_.\,\Pacman$.\r
%\r
% \end{example}\r
+\clearpage\r
+\section[Tentativi X-separability]{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{\kn}{$(\kappa,n)$}\r
+\newcommand{\knnf}{$\xK{}$-nf}\r
+\newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
+\newcommand{\Args}[1]{\operatorname{args}(#1)}\r
+\newcommand{\Head}[1]{\operatorname{head}(#1)}\r
+\newcommand{\nf}[1]{#1{\downarrow}}\r
+\newcommand{\Nat}{\mathbb{N}}\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}[$\xK$-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 (where $\xK$ is a natural number):\r
+ $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
+ $|\vec\var|\leq\xK$%\r
+ %, $|\vec\tm|\leq\xN$\r
+ , and every term in $\vec\tm$ is a \knnf{} as well.\r
+\end{definition}\r
+\r
+\begin{definition}[Normal form $\nf\cdot$]\r
+ \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
+{\color{yellow}\begin{definition}[Good permutation]\r
+ Let $\tm$ a \knnf.\r
+ $\Perm i j$ is \emph{good} for $\tm$ if\r
+ $i<\Args\tm$ and $j \geq \xK + i + 1$.\r
+\end{definition}}\r
+\r
+% \begin{lemma}\r
+% Let $\tm$ in nf.\r
+% Let $\vec\alpha$ fresh variables.\r
+% If $|\vec\alpha|\geq \lams\tm$,\r
+% then the normal form of $\tm\,\vec\alpha$ is inert.\r
+% \end{lemma}\r
+\r
+\begin{lemma}[Monotonicity]\label{l:k-nf-mono}\r
+ If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf\r
+ for every $\xK' \geq \xK{}$.\r
+\end{lemma}\r
+\r
+\begin{lemma}\r
+ Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$.\r
+ Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.\r
+\end{lemma}\r
+\begin{proof}\r
+ By (course-of-value) structural induction on $\tm$.\r
+ Let $\tm=\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo$ and $\sigma\defeq\Subst\var{\Perm i j}$.\r
+ By cases:\r
+ \begin{itemize}\r
+ \item Case $\varthree\neq\var$: $\nf{(\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo)\sigma} = \lambda\vec\vartwo.\,\varthree\,\vec{(\nf{\tmtwo\sigma})}$.\r
+ By \ih{} each term in $\vec\tmtwo\sigma$ is a $\xK'$-nf.\r
+ We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.\r
+\r
+ \item Case $\varthree=\var$ and $i<|\vec\tmtwo|$:\r
+ $\tm\sigma \to^* \lambda\vec\vartwo.\, (\tmtwo_i\sigma)\vec\alpha \vec{(\tmtwo\sigma)} $.\r
+ Now, by \ih{} $\nf{\tmtwo_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,\r
+ $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert (\textcolor{red}{Serve lemma?}).\r
+ Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \nf{\vec{(\tmtwo\sigma)}}$,\r
+ and again by \ih{} it is also a $\xK'$-nf.\r
+ \item Case $\varthree=\var$ and $|\vec\tmtwo|\leq i$:\r
+ $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree.\, \varthree\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for some $\varthree\in\vec\varthree$\r
+ and $|\vec\varthree| = i + 1 - |\vec\tmtwo|$.\r
+ Conclude by \ih{} and because $|\vec\vartwo\vec\varthree| \leq \xK{} + i + 1 - |\vec\tmtwo| \leq \xK{} + i + 1 = \xK'$.\r
+ \end{itemize}\r
+ \r
+\end{proof}\r
+\r
+% \begin{lemma}\r
+% Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
+% If $i<\Args\tm$ and $j \geq \xK + i + 1$,\r
+% then $\tmtwo\defeq\nf{\tm\Subst\var{\Perm i j}}$ is defined;\r
+% $\Lams\tm=\Lams{\tmtwo}$; $\tmtwo$ is a $(j,\xN + j)$-nf.\r
+% \end{lemma}\r
+% \begin{proof}\color{red}\TODO{}\r
+% By induction on the normal form structure of $\tm$:\r
+% let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$.\r
+% By \ih{}, $\nf{\tmtwo\Subst\var\perm}$ are $(j,\xN+j)$-nfs.\r
+% \begin{itemize}\r
+% \item if $\vartwo=\var$, then\r
+% $\nf{\tm\Subst\var\perm} = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
+% \item if $\vartwo\neq\var$, then $\nf{\tm\Subst\var\perm} = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
+% where $\vec\tmthree\defeq \nf{\vec\tmtwo\Subst\var\perm}$.\r
+% Conclude by inductive hypothesis.\r
+% \end{itemize}\r
+% \end{proof}\r
+\r
+\begin{lemma}\r
+ For every \knnf{s} $\tm,\tmtwo$,\r
+ every fresh variable $\var$,\r
+ $\perm\defeq\Perm{i}{i+k+1}$ permutator,\r
+ $\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.\r
+\end{lemma}\r
+\begin{proof}\r
+ The implication from left to right is trivial.\r
+ We now prove that if $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$\r
+ then also $\tm\EtaEq\tmtwo$.\r
+\end{proof}\r
\r
\end{document}\r
projects / fireball-separation.git / blobdiff