Prove that the equal-length concatenation of regular languages is context free

Question

If A and B are regular, then prove that $A@B = \{xy \mid x \in A \text{ and } y \in B \text{ and } |x|=|y|\}$ is always context free.

So I'm trying to come up with the proof that looks something like this. Knowing that $A$ and $B$ are regular, we can conclude that there exists NFA for $A$ and $B$ respectively. Then, we can work out these NFA into two separate PDA: one PDA that would accept $x$ from $A$ and another PDA that would accept $y$ from $B$. Then we need to somehow merge two PDAs into one modifying it so that it controls the length of $x$ and $y$ too and accepts only in the case when $x=y$.

I am just trying to come up with the set of legitimate steps that would follow through this, and that these steps would always work so that given $A$ and $B$ are regular final the PDA will always accept $A@B$.

Answer 1

To expand a bit on @babou's comment, let $M_A$ and $M_B$ be the FAs for $A, B$ respectively. Make a PDA that acts like this:

(1) repeat
      read the input, using MAs transition rules.
      For each character read, push a marker on the stack.
    until MA enters a final state or no input remains
(2) if no input remains and MA is in a final state, go to (3)
    else if no input remains and MA is in a non-final state, halt and reject
    else nondeterministically go to (1) and (3) [guessing that we're done with the first half]
(3) repeat
      run the PDA on any remaining input, using MBs transition rules
      For each character read, pop the stack
    until the stack is empty or no input remains
(4) if MB is in an accept state, no input remains, and the stack is empty, halt and accept
    else halt and reject

(I apologize in advance for any missing details/programming errors, but the intent, I hope, is clear: process the first part of the input, guess that we're in the middle and process the second part.)

Answer 2

You can prove that $A@B$ is context free using closure properties:

• $L_1 = \{a^n\$b^n | n \geq 0\}$ is context free (generated by $S \rightarrow \$ \ |\ aSb$)
• Define $f: \{a,b\} \rightarrow \Sigma$. Context free languages are closed under homomorphism, so $L_2 = f(L_1) = \{u\$v\ |\ u,v \in \Sigma^* , |u|=|v| \}$ is context free
• Regular languages are closed under concatinations, so $L_3 = A\$B$ is also regular
• The intersection of context free language with regular language is context free, so $L_4 = L_3 \cap L_2$ is context free.
• $L_4 = \{ x\$y \ | \ x \in A, y \in B, |x| = |y| \}$
• Define $h: \Sigma \cup \{\$\} \rightarrow \Sigma^*$ as follow. $h(\sigma) = \sigma, h(\$) = \epsilon$
• Context free languages are close under homomorphism, so $h(L_3)$ is context free.
• $h(L_4) = \{ xy \ | \ x \in A, y \in B, |x| = |y| \} = A@B$

Therefore, $A@B$ is context free.