Solution (source code)

= Solution

A <context-free grammar> with start symbol $P$, terminal <alphabet> $\{0,1\}$, and the following productions generates all binary <palindromes>:
$$
\boxed{P\longrightarrow\epsilon\mid0\mid1\mid0P0\mid1P1.}
$$
Each production preserves the <palindrome> property: it either supplies a central <string> of length zero or one, or wraps the same symbol around a shorter <palindrome>. This proves soundness by <structural induction> on the <parse tree>.

Conversely, any <palindrome> of length at least two has equal first and last symbols. Remove them to obtain a shorter <palindrome>, apply <mathematical induction> on length, and then use the corresponding wrapping production. The three base cases are $\epsilon$, $0$, and $1$, proving completeness.