[Solved]: Is it decidable whether a given context free grammar generates an infinite number of strings?

Let $G$ be a context free grammar, and let us assume that it is in Chomsky normal form. If it’s not, we’ll convert it first. An important property of this normal form is that the only way to derive the empty word is with the single rule $S_0to epsilon$ (where $S_0$ is the initial variable, which cannot be derived from other variables). Thus, any other derivation adds some non-trivial part to a word. Now, let $n$ be the number of variables in the grammar, and let $k$ be the maximal length on the right-side of a derivation rule. That is, $Ato B_1cdots B_k$ is the maximal length. We are going to show the following theorem:

$G$ generates an infinite word iff it generates a word of length at least $k^{n+2}$.

Consider some word $w$ generated by the grammar, and a derivation tree for it. The derivation tree has branching factor of at most $k$, and thus it needs to be of height at least $log_k |w|$ in order to derive $w$. Take a really long word $w$. Just how long? take $w$ of length $k^{n+2}$. Then, every derivation tree of $w$ requires at least height $log_k(k^{n+2})=n+2$. That means that there is some path in the tree of length $n+2$, and on this part there is some variable that repeats (since there are only $n$ variables). We can assume that the derivation from this variable derives other things besides itself, otherwise we can shorten the tree. Now, you can “pump” the word $w$ to infinitely many other words that are generated, by repeating the subtree of the variable that derives itself. If this sounds complicated, take a look at the pumping lemma, it’s the same idea. So now what? Well, take your grammar, and “remove” from it all words of length less than $k^{n+2}$ by intersecting it with a regular language of all words of length at least $k^{n+2}$, and check if the resulting grammar is non-empty. If it is, the original grammar generated an infinite language, and otherwise – a finite language.