helm/ocaml/tactics/doc/main.tex

   1 \documentclass[a4paper]{article}
   2
   3 \usepackage{a4wide}
   4 \usepackage{pifont}
   5 \usepackage{semantic}
   6 \usepackage{stmaryrd}
   7
   8 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
   9
  10 \title{Continuationals semantics for \MATITA}
  11 \author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
  12 \small Department of Computer Science, University of Bologna \\
  13 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
  14 \small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
  15
  16 \newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}}
  17 \newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}}
  18
  19 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
  20 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
  21 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
  22 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
  23 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
  24 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
  25 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
  26 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
  27 \newcommand{\SKIP}{\MATHTT{skip}}
  28 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
  29
  30 \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
  31
  32 \newcommand{\GOAL}{\MATHIT{goal}}
  33 \newcommand{\SWITCH}{\MATHIT{switch}}
  34 \newcommand{\LIST}{\MATHTT{list}}
  35 \newcommand{\INT}{\MATHTT{int}}
  36 \newcommand{\OPEN}{\MATHTT{Open}}
  37 \newcommand{\CLOSED}{\MATHTT{Closed}}
  38
  39 \newcommand{\SEMOP}[1]{|[#1|]}
  40 \newcommand{\TSEMOP}[1]{{}_t|[#1|]}
  41 \newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}}
  42 \newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle}
  43 \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
  44
  45 \newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}}
  46
  47 \newcommand{\ZEROPOS}{\MATHIT{zero\_pos}}
  48 \newcommand{\INITPOS}{\MATHIT{init\_pos}}
  49 \newcommand{\ISFRESH}{\MATHIT{is\_fresh}}
  50 \newcommand{\FILTER}{\MATHIT{filter}}
  51 \newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
  52 \newcommand{\ISOPEN}{\MATHIT{is\_open}}
  53 \newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
  54 \newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
  55 \newcommand{\GOALS}{\MATHIT{open\_goals}}
  56
  57 \newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
  58 \newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}
  59
  60 \newlength{\sidecondlen}
  61 \setlength{\sidecondlen}{2cm}
  62
  63 \begin{document}
  64 \maketitle
  65
  66 \section{Semantics}
  67
  68 \subsection{Language}
  69
  70 \[
  71 \begin{array}{rcll}
  72  S & ::= & & \mbox{(\textbf{continuationals})}\\
  73    &     & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
  74    &  |  & \DOT & \mbox{(dot)} \\
  75    &  |  & \SEMICOLON & \mbox{(semicolon)} \\
  76    &  |  & \BRANCH & \mbox{(branch)} \\
  77    &  |  & \SHIFT & \mbox{(shift)} \\
  78    &  |  & \POS{i} & \mbox{(relative positioning)} \\
  79    &  |  & \MERGE & \mbox{(merge)} \\[2ex]
  80    &  |  & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
  81    &  |  & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
  82    &  |  & S ~ S & \mbox{(sequential composition)} \\[2ex]
  83    T & : := & & \mbox{(\textbf{tactics})}\\
  84      &   & \SKIP & \mbox{(skip)} \\
  85      & | & \mathtt{reflexivity} & \\
  86      & | & \mathtt{apply}~t & \\
  87      & | & \dots &
  88 \end{array}
  89 \]
  90
  91 \subsection{Status}
  92
  93 \[
  94 \begin{array}{rcll}
  95  \xi & & & \mbox{(proof status)} \\
  96  \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]
  97
  98  \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
  99  \mathit{locator} & = & \INT\times\SWITCH & \\
 100  \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]
 101
 102  \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
 103  \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
 104  \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]
 105
 106  \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
 107  \\[2ex]
 108
 109  \mathit{status} & = & \xi\times\mathit{stack} \\
 110 \end{array}
 111 \]
 112
 113 \paragraph{Utilities}
 114 \begin{itemize}
 115  \item $\ZEROPOS([g_1;\cdots;g_n]) =
 116   [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
 117  \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
 118   [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$
 119  \item $\ISFRESH(s) =
 120   \left\{
 121   \begin{array}{ll}
 122    \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
 123    \mathit{false} & \mathrm{otherwise} \\
 124   \end{array}
 125   \right.$
 126  \item $\FILTEROPEN(\mathit{locs})=
 127   \left\{
 128   \begin{array}{ll}
 129    [] & \mathrm{if}~\mathit{locs} = [] \\
 130    \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
 131    & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
 132    \FILTEROPEN(\mathit{tl})
 133    & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
 134   \end{array}
 135   \right.$
 136  \item $\REMOVEGOALS(G,\mathit{locs}) =
 137   \left\{
 138   \begin{array}{ll}
 139    [] & \mathrm{if}~\mathit{locs} = [] \\
 140    \REMOVEGOALS(G,\mathit{tl})
 141    & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
 142      \land g\in G\\
 143    hd :: \REMOVEGOALS(G,\mathit{tl})
 144    & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
 145   \end{array}
 146   \right.$
 147  \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
 148   it returns a new stack $S'$ identical to the given one with the exceptions
 149   that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
 150   components and removed from $\tau$ and $\kappa$ components.
 151  \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
 152   on a given stack $S$, appearing in an \OPEN{} switch.
 153 \end{itemize}
 154
 155 \paragraph{Invariants}
 156 \begin{itemize}
 157  \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
 158   \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
 159   $\tau$ and $\kappa$ components has an \OPEN~switch).
 160  \item Unless \FOCUS{} is used the stack contains no duplicate goals.
 161  \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the
 162   top-level $\Gamma$)}, \ISFRESH(l)$.
 163 \end{itemize}
 164
 165 \subsection{Semantics}
 166
 167 \[
 168 \begin{array}{rcll}
 169  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
 170   \mbox{(continuationals semantics)} \\
 171  \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
 172   \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
 173 \end{array}
 174 \]
 175
 176 \[
 177 \begin{array}{rcl}
 178  \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
 179   \xi\times\GOAL~\LIST\times\GOAL~\LIST
 180 \end{array}
 181 \]
 182
 183 \[
 184 \begin{array}{rlcc}
 185  \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
 186  \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
 187 \end{array}
 188 \]
 189
 190 \[
 191 \begin{array}{rcl}
 192
 193  \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 194  & =
 195  & \langle
 196    \xi_n,
 197    \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
 198 %    \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
 199    :: \DEEPCLOSE(G^c_n,S)
 200    \rangle
 201  \\[1ex]
 202  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
 203  \\[1ex]
 204  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
 205   \Gamma' = \ZEROPOS(G^o_n)
 206   \land \tau' = \REMOVEGOALS(G^c_n,\tau)
 207   \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
 208  }
 209  \\[1ex]
 210  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
 211  \left\{
 212  \begin{array}{rcll}
 213   \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\
 214   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
 215   & =
 216   & \langle\xi_i, G^o_i, G^c_i\rangle
 217   & l_{i+1}\in G^c_i \\
 218   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
 219   & =
 220   & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle
 221   & l_{i+1}\not\in G^c_i \\[1ex]
 222   & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
 223  \end{array}
 224  \right.
 225  }
 226  \\[6ex]
 227
 228  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
 229  & =
 230  & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
 231  \\[1ex]
 232  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
 233  \\[2ex]
 234
 235  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
 236  & =
 237  & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
 238  \\[1ex]
 239  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
 240  \\[2ex]
 241
 242  \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]
 243
 244  \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 245  \quad
 246  & =
 247  & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
 248    ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
 249  \\[1ex]
 250  & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
 251  \\[2ex]
 252
 253  \SEM{~\SHIFT~}
 254   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'}
 255   ::S}
 256  & =
 257  & \langle
 258    \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
 259         ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
 260    \rangle
 261  \\[1ex]
 262  & & \mathrm{where} ~ n\geq 1
 263  \\[2ex]
 264
 265  \SEM{~\POS{i}~}
 266   {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 267  & =
 268  & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
 269    ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
 270  \\[1ex]
 271  & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
 272  \\[2ex]
 273
 274  \SEM{~\POS{i}~}
 275   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
 276   ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 277  & =
 278  & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
 279  ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
 280    \rangle
 281  \\[1ex]
 282  & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
 283  \\[2ex]
 284
 285  \SEM{~\MERGE~}
 286   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
 287   ::S}
 288  & =
 289  & \langle \xi,
 290    \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
 291    :: S
 292    \rangle
 293  \\[2ex]
 294
 295  \SEM{\FOCUS{g_1,\dots,g_n}}{S}
 296  & =
 297  & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG}
 298    ::\DEEPCLOSE(S)
 299    \rangle
 300  \\[1ex]
 301  & & \mathrm{where} ~
 302  \forall i=1,\dots,n,~g_i\in\GOALS(S)
 303  \\[2ex]
 304
 305  \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
 306  & =
 307  & \langle \xi, S\rangle \\[2ex]
 308
 309 \end{array}
 310 \]
 311
 312 \end{document}
 313