app-product.tex

% !TEX root = main.tex
%
% Proof of Proposition product swVPA
%
We prove the closure under~$\otimes$
- the case of~$\oplus$ is similar.
% 
Let $A_1 = \< Q_1, P_1, \init_1, \bar\wei_1, \final_1 >$
and $A_2 = \< Q_2, P_2, \init_2, \bar\wei_2, \final_2 >$.
The \SWVPA $A_1 \otimes A_2$ is built by a 
classical product construction.
%
It has a state set $Q = Q_1 \times Q_2$
and a auxiliary set of stack symbols $P = P_1 \times P_2$:
$A_1 \otimes A_2 = \< Q, P, \init_{1, \otimes}, 
         \bar\wei_{\otimes}, \final_{\otimes} >$.
The weight entering and leaving functions         
$\init_{\otimes}$, $\final_{\otimes}$
and the sextuplet of transition functions $\bar\wei_{\otimes}$
are defined 
using the label-theory operators of Section~\ref{section:symbols} as follows, 
%
for all $\< q_1, q_2>, \< q'_1, q'_2> \in Q$ 
and $\< p_1, p_2>, \< p'_1, p'_2> \in P$:
\[
\begin{array}{rcl}
\init_{\otimes}\bigl(\< q_1, q_2>\bigr) = \init_{1}(q_1) \otimes \init_{2}(q_2) & &
\final_{\otimes}\bigl(\< q_1, q_2>\bigr) = \final_{1}(q_1) \otimes \final_{2}(q_2)\\
%
\wei_{\mathsf{i}, \otimes}\bigl(\< q_1, q_2>, \<p_1, p_2>, \<q'_1, q'_2>\bigr) & = &
\wei_{\mathsf{i}, 1}(q_1, p_1, q'_1) \otimes \wei_{\mathsf{i}, 2}(q_2, p_2, q'_2)\\
%
\weie[\mathsf{i}, \otimes]\bigl(\< q_1, q_2>, \<q'_1, q'_2>\bigr) & = &
\weie[\mathsf{i}, 1](q_1, q'_1) \otimes \weie[\mathsf{i}, 2](q_2, q'_2)\\
%
\wei_{\mathsf{c}, \otimes}\bigl(\< q_1, q_2>, \<p_1, p_2>, \<q'_1, q'_2>, \<p'_1, p'_2>\bigr) & = &
\wei_{\mathsf{c}, 1}(q_1, p_1, q'_1, p'_1) \otimes \wei_{\mathsf{c}, 2}(q_2, p_2, q'_2, p'_2)\\
%
\weie[\mathsf{c}, \otimes]\bigl(\< q_1, q_2>, \<p_1, p_2>, \<q'_1, q'_2>\bigr) & = &
\weie[\mathsf{c}, 1](q_1, p_1, q'_1) \otimes \weie[\mathsf{i}, 2](q_2, p_2, q'_2)\\
%
\wei_{\mathsf{r}, \otimes}\bigl(\< q_1, q_2>, \<p_1, p_2>, \<q'_1, q'_2>\bigr) & = &
\wei_{\mathsf{r}, 1}(q_1, p_1, q'_1) \otimes \wei_{\mathsf{r}, 2}(q_2, p_2, q'_2)\\
%
\weie[\mathsf{r}, \otimes]\bigl(\< q_1, q_2>, \<q'_1, q'_2>\bigr) & = &
\weie[\mathsf{r}, 1](q_1, q'_1) \otimes \weie[\mathsf{i}, 2](q_2, q'_2)\\
\end{array}
\]
With these functions, $A$ simulate the synchronized behaviour of~$A_1$ and~$A_2$.
\florent{complete proof.}