ac_notes.tex

   1 \documentclass[12pt]{article}\r
   2 \usepackage{blindtext}\r
   3 \usepackage{enumerate}\r
   4 \usepackage{hyperref, bookmark}\r
   5 \usepackage{amsmath, amsfonts, amssymb, amsthm}\r
   6 \usepackage{xcolor}\r
   7 \r
   8 \title{Ideas on Strong Separation}\r
   9 \author{Anonymous}\r
  10 \r
  11 \input{macros}\r
  12 \begin{document}\r
  13 \r
  14 \maketitle\r
  15 \r
  16 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
  17 \r
  18 \subparagraph{Syntax}\r
  19 \[\begin{array}{lll}\r
  20   \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\\r
  21   n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\\r
  22   \\\r
  23   C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
  24   P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
  25 \end{array}\]\r
  26 \r
  27 \subparagraph{Reduction}\r
  28 \[\begin{array}{lll}\r
  29   P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &\r
  30    P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\\r
  31    P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &\r
  32     P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\\r
  33 \end{array}\]\r
  34 \r
  35 \subparagraph{Properties of the calculus:}\r
  36 \begin{itemize}\r
  37   \item Every term is normalizing iff it is strongly normalizing.\r
  38   \item Ogni strategia e' perpetua!\r
  39 \end{itemize}\r
  40 \r
  41 \clearpage\r
  42 \r
  43 \[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]\r
  44 \r
  45 \begin{definition}{Path of a hole}\r
  46   \[\begin{array}{ll}\r
  47     \pi_\Box & \defeq \langle\rangle \\\r
  48     \pi_{\Lam{\vec\var}{\vec i \Comma y \, }y\, \vec t E \vec s} & \defeq \\\r
  49   \end{array}\]\r
  50 \end{definition}\r
  51 \r
  52 \newcommand{\NameOf}[2]{\operatorname{name}_{#2}(#1)}\r
  53 \begin{definition}[Name of a variable]~\r
  54   \begin{itemize}\r
  55     \item If $\var$ is free in $\tm$, then $\NameOf\var\tm = ``\var"$;\r
  56     \item {\color{red} If $x$ is bound at the outer layer of a garbage, then\r
  57      $\NameOf\var\tm = \Omega$;}\r
  58     \item\r
  59     If $ x\, \vec s \, (\lambda \vec y.\, \ldots) \preceq t$, then\r
  60     $ \NameOf{\vartwo_i}{\tm} \defeq \NameOf\var\tm ; (|\vec s|, i) $.\r
  61   \end{itemize}\r
  62 \end{definition}\r
  63 \r
  64 \begin{example}\r
  65   \[\begin{array}{ll}\r
  66   D & x \, a \, (\Lam\vartwo {y \Comma y\, b} ) \\\r
  67   C & x \, a \, (\Lam\vartwo{y \Comma y \,b'}) \\\r
  68   C & x \, a' \, (\Lam\vartwo{y \Comma y \,b }) \\\r
  69   \end{array}\]\r
  70 \r
  71   \[\begin{array}{ll}\r
  72   D & y^{[x \, a \, \Omega]} \, b \\\r
  73   C & y^{[x \, a \, \Omega]} \, b' \\\r
  74   C & y^{[x \, a' \, \Omega]} \, b \\\r
  75   \end{array}\]\r
  76 \end{example}\r
  77 \r
  78 \r
  79 \r
  80 \clearpage\r
  81 \[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]\r
  82 \r
  83 \begin{definition}[Unlockable variable]\r
  84   A variable $\var$ is unlockable in a context $E$ if:\r
  85   \begin{itemize}\r
  86     \item it is not bound in $E$, or\r
  87     \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$\r
  88      and $\vartwo$ is unlockable in $E'$.\r
  89   \end{itemize}\r
  90 \end{definition}\r
  91 \r
  92 \begin{lemma}[Elimination of unlockable variables]\r
  93   For every set of terms $\tm_1, \ldots, \tm_n$\r
  94   there exist terms $\tm'_1, \ldots, \tm'_n$\r
  95   without unlockable variables and\r
  96   such that $\tm_i$ is unseparable from $\tm'_i$.\r
  97 \end{lemma}\r
  98 \r
  99 {\color{red}\r
 100  Non esattamente!\r
 101  I termini hanno gli stessi path, e le variabili unlockable\r
 102  del secondo sono iin path virtuali nel primo\r
 103 \r
 104  Piu' esattamente, hai portato il garbage che vuoi far divergere\r
 105   al top level.\r
 106 }\r
 107 \r
 108 \begin{definition}\r
 109   Transformation removing an unlockable variable bound at position $\pi$:\r
 110   \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]\r
 111 \end{definition}\r
 112 \r
 113 {\color{red}\r
 114 Warning! It creates unlockable variables, but in positions whose paths were\r
 115 previously virtual}\r
 116 \r
 117 \begin{lemma}\r
 118   For every semi-$\sigma$-separable $\tm$ and $\tmtwo$,\r
 119    there exist $\sigma$ s.t $\tm\sigma = \ldots \Comma C[i] \Comma \ldots$\r
 120    and $i \not\preceq \tmtwo\sigma$ (and therefore, $\tm\sigma$ and $\tmtwo\sigma$\r
 121    are semi-$\sigma$-separable by ???).\r
 122 \end{lemma}\r
 123 \r
 124 \begin{theorem}\r
 125   $\tm$ and $\tmtwo$ are semi-$\sigma$-separable if \ldots\r
 126 \end{theorem}\r
 127 \r
 128 \clearpage\r
 129 \newcommand{\HeadOf}[1]{\operatorname{hd}(#1)}\r
 130 \newcommand{\ArityOf}[1]{\operatorname{len}(#1)}\r
 131 \begin{itemize}\r
 132   \item \textbf{A sufficient condition for separability:}\r
 133   \item \textbf{Goal.} semi-$\sigma$-separating $\tm$ from $\tmtwo$ (both inerts with pacmans/$\Omega$).\r
 134   \item Let $U \defeq \{\tmtwo' \mid \tmtwo'\preceq\tmtwo \land \HeadOf{\tmtwo'}=\HeadOf{\tm}\r
 135   \land \ArityOf{\tmtwo'} \leq \ArityOf{\tm}\} = \{u_1, \ldots, u_N\}$.\r
 136   \item \textbf{Theorem.} The problem is separable if there exist $\pi_1\ldots\pi_N$\r
 137   $\eta$-difference paths between\r
 138   $\tm$ and $\tmtwo_1\ldots\tmtwo_N$ that are pairwise compatible on $\tm$ (note: also between themselves).\r
 139   \item \textbf{Definition ($\eta$-difference path).}\r
 140   \item \textbf{Definition ($\sqsubset$).} Initial fragments of paths\r
 141    \item \textbf{Definition (Compatible paths).} ``$\pi_j$ is compatible with $\pi_i$ on $\tm$'' iff:\r
 142     \[\forall\pi_i'\sqsubseteq\pi_i\text{ s.t. }\HeadOf{\pi_i'[t]} = \HeadOf{t}\r
 143     \text{, then }\pi_j[\pi_i'[t]] \neq \Omega.\]\r
 144   \item Resta da dimostrare che esista un modo di pre-processare i termini nostri\r
 145    e ottenere degli inerti scelti.\r
 146 \end{itemize}\r
 147 \r
 148 \r
 149 \r
 150 \r
 151 \clearpage\r
 152 \section*{Syntactic Condition}\r
 153 \r
 154 \begin{definition}[Separable]\r
 155   Let $t$, $s$ normal terms.\r
 156 \r
 157   They are (semi?) separable iff\r
 158   there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$\r
 159   S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,\r
 160   $t'' <> s''$.\r
 161 \end{definition}\r
 162 \r
 163 An occurrence of a bound variable is usable if its head is not stuck.\r
 164 \r
 165 A head is stuck\r
 166 \r
 167 \begin{verbatim}\r
 168   Ctx[] is stuck (unappicable) if:\r
 169    - it is an application and the head variable is stuck\r
 170    - it is a garbage\r
 171    -\r
 172 \r
 173 \end{verbatim}\r
 174 \r
 175 \end{document}\r