From: Stefano Zacchiroli Date: Mon, 24 Oct 2005 12:08:50 +0000 (+0000) Subject: new semantics, should be the basis for the (re-)implementation X-Git-Tag: V_0_7_2_3~205 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d5c86473cd2549335e7ee99600b0aaf499ca651;p=helm.git new semantics, should be the basis for the (re-)implementation --- diff --git a/helm/ocaml/tactics/doc/Makefile b/helm/ocaml/tactics/doc/Makefile index 4db53fdf0..b7d8fb45c 100644 --- a/helm/ocaml/tactics/doc/Makefile +++ b/helm/ocaml/tactics/doc/Makefile @@ -5,7 +5,7 @@ # Author: Stefano Zacchiroli # # Created: Sun, 29 Jun 2003 12:00:55 +0200 zack -# Last-Modified: Tue, 05 Apr 2005 10:25:38 +0200 zack +# Last-Modified: Mon, 10 Oct 2005 15:37:12 +0200 zack # ######################################################################## @@ -44,9 +44,10 @@ GZIP = gzip HEVEA = hevea ISPELL = ispell LATEX = latex +PDFLATEX = pdflatex +PRINT = lpr XDVI = xdvi XPDF = xpdf -PDFLATEX = pdflatex ALL_FORMATS = $(BUILD_FORMATS) WORLD_FORMATS = $(AVAILABLE_FORMATS) @@ -79,6 +80,9 @@ showps.gz: showpsgz showhtml: $(HTMLS) $(BROWSER) $< +print: $(PSS) + $(PRINT) $^ + clean: rm -f \ $(TEXS:.tex=.dvi) $(TEXS:.tex=.ps) $(TEXS:.tex=.ps.gz) \ diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index 72639efb9..15091f009 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -13,71 +13,75 @@ \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\ \small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}} -\newcommand{\DOT}{\mbox{\textbf{.}}} -\newcommand{\SEMICOLON}{\mbox{\textbf{;}}} -\newcommand{\BRANCH}{\mbox{\textbf{[}}} -\newcommand{\SHIFT}{\mbox{\textbf{\textbar}}} -\newcommand{\MERGE}{\mbox{\textbf{]}}} +\newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}} +\newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}} + +\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}} +\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}} +\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}} +\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}} +\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}} +\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}} +\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}} +\newcommand{\ENDFOCUS}{\ensuremath{\mathtt{unfocus}}} +\newcommand{\SKIP}{\MATHTT{skip}} +\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}} + \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}} -\newcommand{\SKIP}{\ensuremath{\mathtt{skip}}} -\newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}} -\newcommand{\OLDTACTICAL}[1]{\ensuremath{\mathtt{old\_tactical}~\mathit{#1}}} -\newcommand{\SELECT}[1]{\ensuremath{\mathtt{select} ~ #1}} -\newcommand{\ENDSELECT}[1]{\ensuremath{\mathtt{end}}} - -\newcommand{\GOAL}{\ensuremath{\mathit{goal}}} -\newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}} -\newcommand{\LIST}{\ensuremath{\mathtt{list}}} -\newcommand{\BOOL}{\ensuremath{\mathtt{bool}}} -\newcommand{\STACK}{\ensuremath{\mathtt{stack}}} -\newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}} -\newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#1}} + +\newcommand{\GOAL}{\MATHIT{goal}} +\newcommand{\SWITCH}{\MATHIT{switch}} +\newcommand{\LIST}{\MATHTT{list}} +\newcommand{\INT}{\MATHTT{int}} +\newcommand{\OPEN}{\MATHTT{Open}} +\newcommand{\CLOSED}{\MATHTT{Closed}} \newcommand{\SEMOP}[1]{|[#1|]} \newcommand{\TSEMOP}[1]{{}_t|[#1|]} -\newcommand{\SEM}[5]{\SEMOP{#1}_{#2,#3,#4,#5}} +\newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}} +\newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle} \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}} -\newcommand{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}} -\newcommand{\FILTERFUN}[2]{\FUN{filter}{#1,#2}} -\newcommand{\MAPFUN}[2]{\FUN{map}{#1,#2}} -\newcommand{\DEEPMAPFUN}[2]{\FUN{deep\_map}{#1,#2}} -\newcommand{\ISOPENFUN}{\ensuremath{\mathit{is\_open}}} -\newcommand{\CLOSEFUN}{\ensuremath{\mathit{close}}} -\newcommand{\GOALOFFUN}{\ensuremath{\mathit{goal\_of}}} -\newcommand{\DEEPCLOSEFUN}[2]{\FUN{deep\_close}{#1,#2}} +\newcommand{\GIN}[1][1]{\ensuremath{[s_{#1};\cdots;s_n]}} + +\newcommand{\ZEROPOS}{\MATHIT{zero\_pos}} +\newcommand{\INITPOS}{\MATHIT{init\_pos}} +\newcommand{\ISFRESH}{\MATHIT{is\_fresh}} +\newcommand{\FILTER}{\MATHIT{filter}} +\newcommand{\FILTEROPEN}{\MATHIT{filter\_open}} +\newcommand{\ISOPEN}{\MATHIT{is\_open}} +\newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}} + +\newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}} +\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{S}}} + +\newlength{\sidecondlen} +\setlength{\sidecondlen}{2cm} \begin{document} \maketitle -\section{Foo} +\section{Semantics} \subsection{Language} \[ \begin{array}{rcll} - S & ::= & & \mbox{(\textbf{toplevel grammar})}\\ - & & \varepsilon & \\ - & | & T~ P~ S & \\[2ex] - - T & ::= & & \mbox{(\textbf{tactical})} \\ - & & \APPLY{tac} & \mbox{(tactic application)} \\ - & | & \SKIP & \mbox{(closed goal skipping)} \\ - & | & \OLDTACTICAL{tcl} & \mbox{(non step-by-step tactical)} \\ - & | & \SELECT{n_1,\dots,n_k}{S} & \mbox{(select)} \\[2ex] - - P & ::= & & \mbox{(\textbf{punctuation})} \\ - & & \DOT & \mbox{(dot)} \\ + S & ::= & & \mbox{(\textbf{continuationals})}\\ + & & \TACTIC{T} & \mbox{(tactic)}\\[2ex] + & | & \DOT & \mbox{(dot)} \\ & | & \SEMICOLON & \mbox{(semicolon)} \\ & | & \BRANCH & \mbox{(branch)} \\ & | & \SHIFT & \mbox{(shift)} \\ - & | & \MERGE ~ M & \mbox{(merge)} \\[2ex] - - M & ::= & & \mbox{(\textbf{merge-punctuation})} \\ - & & \varepsilon & \\ - & | & \MERGE ~ M& \mbox{(multi-merge)} \\ - & | & \DOT & \mbox{(merge and choose)} \\[2ex] - + & | & \POS{i} & \mbox{(relative positioning)} \\ + & | & \MERGE & \mbox{(merge)} \\[2ex] + & | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\ + & | & \ENDFOCUS & \mbox{(unfocus)} \\[2ex] + T & : := & & \mbox{(\textbf{tactics})}\\ + & & \SKIP & \mbox{(skip)} \\ + & | & \mathtt{reflexivity} & \\ + & | & \mathtt{apply}~t & \\ + & | & \dots & \end{array} \] @@ -85,180 +89,173 @@ \[ \begin{array}{rcll} - \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\ - \xi & = & \langle n,\alpha\rangle~\LIST& \mbox{(metasenv)} \\ - \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\ - \GOALSWITCH & = & \OPEN{n} \quad | \quad \CLOSED{n} & \\ - \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\ - \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\ + \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\ + \mathit{locator} & = & \INT\times\SWITCH & \\ + \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex] + + \xi & = & (\INT\times\alpha)~\LIST& \mbox{(metasenv)} \\ + \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\ + \tau & = & \SWITCH~\LIST & \mbox{(todo)} \\ + \kappa & = & \SWITCH~\LIST & \mbox{(dot's future)} \\[2ex] + + \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST + \\[2ex] + + \mathit{status} & = & \xi\times\mathit{stack} \\ \end{array} \] +\paragraph{Utilities} +\begin{itemize} + \item \ZEROPOS: map $g -> 0, \OPEN~g$ + \item \INITPOS: map $g -> i, \OPEN~g$ + \item \ISFRESH: $\OPEN~g, 0 -> true | \_ -> false$ + \item \FILTEROPEN: $G -> \FILTER(\ISOPEN,G)$ + \item \DEEPCLOSE: prende uno stack ed un insieme di goal da chiudere, traversa + lo stack rimuovendo le occorrenze dei goal da $\tau$ e $\kappa$ e marcandole + chiuse in $\Gamma$ +\end{itemize} + +\paragraph{Invariants} +\begin{itemize} + \item $\forall \ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s \in\tau\cup\kappa, + \exists g, s = \OPEN~g$ (i goal in $\tau$ e $\kappa$ sono aperti) + \item la lista dei goal nel metasenv contiene tutti e soli i goal presenti + sullo stack + \item lo stack puo' contenere goal duplicati nel caso di uso della select +\end{itemize} + \subsection{Semantics} \[ \begin{array}{rcll} \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} & \mbox{(continuationals semantics)} \\ - \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tacticals semantics)} \\ -\end{array} -\] - -\[ -\begin{array}{rcl} - \mathit{filter} & : & (\alpha->\BOOL)->\alpha~\LIST->\alpha~\LIST \\ - \mathit{map} & : & (\alpha->\beta)->\alpha~\LIST->\beta~\LIST \\ - \mathit{deep\_map} & : - & (\alpha->\beta)->\alpha~\LIST~\STACK->\beta~\LIST~\STACK \\ - \in & : & \alpha->\alpha~\LIST->\BOOL \\ - \cup & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\ - \setminus & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\ + \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH -> + \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\ \end{array} \] \[ \begin{array}{rcl} - \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST \\[1ex] -% \ISCLOSEDFUN & : & \GOALSWITCH -> \BOOL \\ - \ISOPENFUN & : & \GOALSWITCH -> \BOOL \\ - \CLOSEFUN & : & \GOALSWITCH -> \GOALSWITCH \\[1ex] -% \OPENFUN & : & \GOAL -> \GOALSWITCH \\[1ex] - \GOALOFFUN & : & \GOALSWITCH -> \GOAL \\[1ex] - \mathit{deep\_close} & : - & \GOAL~\LIST -> \GOALSWITCH~\STACK -> \GOALSWITCH~\STACK \\[1ex] -\end{array} -\] - -\[ -\begin{array}{rcl} - \DEEPCLOSEFUN{G}{\Gamma} - & = - & \MAPFUN{\mathit{fold} - (\lambda g.\lambda acc. - \mathit{if}~\GOALOFFUN(g)\in G~\land\ISOPENFUN(g)~ - \mathit{then}~[]~ - \mathit{else}~[g]\cup\mathit{acc}) - []}{\Gamma} + \mathit{apply\_tac} & : & T -> \xi -> \GOAL -> + \xi\times\GOAL~\LIST\times\GOAL~\LIST \end{array} \] \[ \begin{array}{rlcc} - \TSEM{\APPLY{tac}}{\xi}{\OPEN{n}} & = - & \mathit{apply\_tac}(\mathit{tac},\xi,n) & \\ - \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle \xi, [], [n]\rangle & \\ + \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\ + \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle & \end{array} \] \[ \begin{array}{rcl} - \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa} - \quad (n\geq 1) + + \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} & = - & \langle\xi_n, - \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPCLOSEFUN{G^C_n}{\Gamma}, - \tau\setminus G^C_n,\kappa\setminus G^O_n\rangle + & \langle + \xi_n, + \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t} + :: \DEEPCLOSE(G^c_n,S) + \rangle \\[1ex] - \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~ + \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ \left\{ \begin{array}{rcll} - \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\ - \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle + \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\ + \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle & = - & \langle\xi_i, G^O_i, G^C_i\rangle - & g_{i+1}\in G^C_i \\ - \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle + & \langle\xi_i, G^o_i, G^c_i\rangle + & s_{i+1}\in G^c_i \\ + \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle & = - & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle - & g_{i+1}\not\in G^C_i \\ - & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}} + & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle + & s_{i+1}\not\in G^c_i \\[1ex] + & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{s_{i+1}} \\ \end{array} \right. } \\[2ex] - \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa} + \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S} & = - & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'} + & \langle \xi, \ENTRY{s_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle \\[1ex] - - & & \mathit{where} ~ - \langle\xi',\Gamma',\tau',\kappa',\rangle = - \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa} + & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \\[2ex] - \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa} + \SEM{~\DOT~}{\ENTRY{[]}{\tau}{s::\kappa}{t}::S} & = - & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle - \\[1ex] + & \langle \xi, \ENTRY{\Gamma}{\tau}{\kappa}{t}::S \rangle + \\[2ex] - \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~ - \langle \xi',G::\Gamma',\tau',K::\kappa' \rangle - = \SEM{C}{\xi}{\Gamma}{\tau}{\kappa}} - \\[1ex] + \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex] - \multicolumn{3}{l}{\hspace{2em}\mathit{and} ~ - \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle = - \left\{ - \begin{array}{ll} - \langle \xi', [g]::\Gamma', \tau', (\MAPFUN{\GOALOFFUN}{G'}\cup K)::\kappa' - \rangle - & \FILTERFUN{\ISOPENFUN}{G} = g::G' - \\ - \langle \xi', [\mathtt{Open}~n]::\Gamma', \tau', K'::\kappa' \rangle - & \FILTERFUN{\ISOPENFUN}{G} = []~\land~K=n::K' - \end{array} - \right.} + \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} + \quad + & = + & \langle\xi, \ENTRY{s_1'}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{[s_2';\cdots;s_n']}{\tau}{\kappa}{t}::S + \\[1ex] + & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[s_1';\cdots;s_n'] \\[2ex] - \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa} - \quad (n\geq 2) + \SEM{~\SHIFT~} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t}::S} & = - & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle + & \langle + \xi, \ENTRY{s_1}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{\GIN[2]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t}::S + \rangle \\[2ex] - \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa} + \SEM{\POS{i}} + {\ENTRY{[s]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} & = - & \langle\xi, - [g_i]::[g_{i+1};\dots;g_n]::\Gamma, - \tau'::\tau, - []::\kappa\rangle + & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{s_i :: (\Gamma'\setminus [s_i])}{\tau'}{\kappa'}{t'}::S \rangle \\[1ex] - - & & \mathit{where} ~ - \tau' = T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K + & & \mathrm{where} ~ \langle i,s'\rangle = s_i\in \Gamma'~\land~\ISFRESH(s) \\[2ex] - \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa} + \SEM{\POS{i}} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG} + ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} & = - & \langle \xi, \Gamma'::\Gamma, \tau, \kappa \rangle + & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{\Gamma'\setminus [s_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S + \rangle \\[1ex] + & & \mathrm{where} ~ \langle i, s'\rangle = s_i\in \Gamma' + \\[2ex] - & & \mathit{where} ~ - \Gamma' = - T \cup\FILTERFUN{\ISOPENFUN}{G} - \cup[g_i;\dots;g_n] - \cup\MAPFUN{\mathtt{Open}}{K} + \SEM{~\MERGE~} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'} + ::S} + & = + & \langle \xi, + \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'} + :: S + \rangle \\[2ex] - \SEM{\SELECT{n_1,\dots,n_k}{C}}{\xi}{\Gamma}{\tau}{\kappa} + \SEM{\FOCUS{g_1,\dots,g_n}}{S} & = - & \langle \xi',\Gamma',\tau',\kappa' \rangle + & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}::S + \rangle \\[1ex] - - & & \mathit{where} ~ - \forall ~ i=1,\dots,k,~\exists ~ \alpha_i,~\langle n_i,\alpha_i\rangle \in \xi - \\[1ex] - - & & \mathit{and} ~ - \langle \xi', []::\Gamma', []::\tau', []::\kappa' \rangle - = \SEM{C}{\xi}{\MAPFUN{\mathtt{Open}}{[n_1;\dots;n_k]}::\Gamma}{[]::\tau}{[]::\kappa} + & & \mathrm{where} ~ + \forall ~ i=1,\dots,n,~\exists~\alpha_i,n_i,~\langle n_i,\alpha_i\rangle\in\xi \\[2ex] + \SEM{\ENDFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S} + & = + & \langle \xi, S\rangle \\[2ex] + \end{array} \]