Proof that CFL aren't closed under intersection using synchronous parallel (N)PDA composition

It is well known that the class of CFLs is not closed under intersection as follows e.g. from the following example:
$$L_1 \cap L_2 = \left\{ a^mb^mc^n \mid m,n \ge 1 \right\} \cap \left\{ a^mb^nc^n \mid m,n \ge 1 \right\} = \left\{ a^ib^ic^i \mid i \ge 1 \right\} \not \in \mathcal{L_2},$$
where $L_1,L_2 \in \mathcal{L2}$.

I was wondering if this could be proven using the synchronous parallel composition of two (non-deterministic) PDAs, or rather what is wrong with the following construction which seemingly comes to the opposite conclusion:


Let $PDA_1, PDA_2, PDA_{1,2}$ be, WOLOG, (non-deterministic) PDAs accepting by final state and with total transition functions:
$$ PDA_1 = \Big(Q_1, \Sigma_1, \Gamma_1, \delta_1, q^0_1, \gamma^0_1, F_1 \Big) \\
PDA_2 = \Big(Q_2, \Sigma_2, \Gamma_2, \delta_2, q^0_2, \gamma^0_2, F_2 \Big) \\
PDA_{1,2} = \Big(Q_1 \times Q_2 \cup \big(q_{\emptyset}, q_{\emptyset}\big), \Sigma_1 \cup \Sigma_2, \Gamma_1 \times \Gamma_2, \delta_{1,2}, \big(q^0_1, q^0_2 \big), \big(\gamma^0_1, \gamma^0_2 \big), F_1 \times F_2 \Big)$$
where $q_{\emptyset} \not\in Q_1 \cup Q_2$ and $\delta_{1,2}$ is defined as follows:
$$ \delta_{1,2} \Big(\big(q_1, q_2 \big), a, \big(\gamma_1, \gamma_2 \big) \Big) = \begin{cases}
\Big(\big(q'_1, q'_2 \big), \big(\gamma'_1, \gamma'_2 \big) \Big) & \big(q'_1, \gamma'_1 \big) \in \delta_1 \big(q_1, a, \gamma_1 \big) \land \\ & \big(q'_2, \gamma'_2 \big) \in \delta_2 \big(q_2, a, \gamma_2 \big) \\
& \text{(if such transitions are defined)} \\
\Big(\big(q_{\emptyset}, q_{\emptyset} \big), \big(\gamma_1, \gamma_2 \big)\Big) & \text{otherwise} \\
\end{cases} $$

Surely $PDA_{1,2}$ accepts only words from the intersection of languages $L(PDA_1)$ and $L(PDA_2)$. Why doesn't it accept all of them?

This doesn't work, because the stacks of the two PDAs aren't synchronized. You can get to a state where $\text{PDA}_1$ pushes a symbol but $\text{PDA}_2$ pops a symbol. What is $\text{PDA}_{1,2}$ supposed to do at that point? It's screwed.

The product construction would work if there was a guarantee that the length of the stack of $\text{PDA}_1$ was always the same as the length of the stack of $\text{PDA}_2$ -- but as explained, this is not guaranteed.

Another way to put it: Your definition of $\delta_{1,2}$ does not make any sense. The output is supposed to be an element of $Q \times \Gamma^$, where here $\Gamma = \Gamma_1 \times \Gamma_2$. However, a pair like $(\lambda'_1,\lambda'_2)$ is not an element of $(\Gamma_1 \times \Gamma_2)^$. If the length of $\lambda'_1$ was the same as the length of $\lambda'_2$, you could interpret $(\lambda'_1,\lambda'_2)$ as an element of $(\Gamma_1 \times \Gamma_2)^$: it is the string whose $i$th symbol is $(\lambda'_1[i],\lambda'_2[i])$. Unfortunately, when the length of $\lambda'_1$ is different from the length of $\lambda'_2$, there's no way to interpret $(\lambda'_1,\lambda'_2)$ as an element of $(\Gamma_1 \times \Gamma_2)^$. Consequently, your definition of $\delta_{1,2}$ is not well-formed: it does not have the proper type signature.

As you quite accurately summarize the situation: One stack can grow ad infinitum while the other not and in order to access the previous element from the shorter stack, the PDA would need to indestructibly go through the potentially infinitely long stack. This could be fixed if we had an automaton with two separate stacks; however, such an automaton would be computationally equivalent to a Turing machine and thus is more powerful than a PDA (which only has one stack).

StackExchange Computer Science Q#43697, answer score: 4