Pushdown automaton accepting $\{a,b\}^*$ with twice as many $a$s as $b$s

Question

Design a pushdown automaton that can accept

$$\{w|w\in\{a,b\}^*\text{ and $w$ has twice as many $a$s as $b$s}\} \, .$$

I have a solution as the following. The notation seems to follow "An Introduction to Formal Languages and Automaton" by Peter Linz, where $\delta$ is the transition function with three arguments: current state, input, current stack top; $\lambda$ as the second argument of $\delta$ means empty string $\epsilon$ in some other textbooks, and $\lambda$ as the third argument of $\delta$ means the transition ignores the current stack top. The $\lambda$ on the right hand side means "pop the top element of the stack".

I have several confusions,

1) I am not sure what the right-hand side notation means. For example, does the right hand side of $\delta(q_1,a,A)=\{[q_2，A]\}$ means pushing an $A$ into the stack? Or it means the stack top stays $A$ without a new $A$ pushed to it?

If this means "push", then what about $\delta(q_1,a,C)=\{[q_2，C]\}$? $C$ seems to mark the bottom of the stack. We push another $C$ to the stack when there is already a $C$ in it?

2) I think the solution might be wrong. I don't see why it accepts $aab$. Tracing this string, I think the transition is the following based on the design (if the big letter at the right-hand side means pushing a new symbol),

$q_0,\lambda \to_\lambda q_1,C\to_a q_2,CC \to_\lambda q_1,ACC \to_a q_2,AACC \to_\lambda q_1,AAACC \to_b q_1,AACC$

It is very strange and I feel very confused. Hope someone can help! Thank you!

Answer 1

When in doubt, one should always consult the definitions.

In this case, this is Definition 7.1 of the book by Peter Linz.

It states that $$\delta : Q \times (\Sigma \cup \{ \lambda \}) \times \Gamma \rightarrow \textrm{finite subsets of } Q \times \Gamma^*$$ Thus, $\delta(q,a,A) = \{[q_1,w_1], \ldots, [q_k,w_k\}$ means that when a pushdown automaton is in state $q$ and sees an $a$ on input (where $a$ may be an input or the empty string $\lambda$), then it can enter any one of the states $q_1$ to $q_k$ and replace $A$ by the corresponding string of stack symbols $w_i$.

Therefore, a pushdown automaton can push a string $w$ to the stack by reading $\lambda$ and replacing it by $w$. Or it can pop the top symbol $b$ by seeing $b$ on the stack and replacing it by $\lambda$.