In mathematics, the Muller–Schupp theorem states that a finitely generated group G has context-free word problem if and only if G is virtually free. The theorem was proved by David Muller and Paul Schupp in 1983. Word problem for groups Let G be a finitely generated group with a finite marked generating set X, that is a set X together with the map such that the subset generates G. Let be the group alphabet and let be the free monoid on that is is the set of all words (including the empty word) over the alphabet . The map extends to a surjective monoid homomorphism, still denoted by , . The word problem of G with respect to X is defined as where is the identity element of G. That is, if G is given by a presentation with X finite, then consists of all words over the alphabet that are equal to in G. Virtually free groups A group G is said to be virtually free if there exists a subgroup of finite index H in G such that H is isomorphic to a free group. If G is a finitely generated virtually free group and H is a free subgroup of finite index in G then H itself is finitely generated, so that H is free of finite rank. The trivial group is viewed as the free group of rank 0, and thus all finite groups are virtually free. A basic result in Bass–Serre theory says that a finitely generated group G is virtually free if and only if G splits as the fundamental group of a finite graph of finite groups. Precise statement of the Muller–Schupp theorem The modern formulation of the Muller–Schupp theorem is as follows: Let G be a finitely generated group with a finite marked generating set X. Then G is virtually free if and only if is a context-free language. Sketch of the proof The exposition in this section follows the original 1983 proof of Muller and Schupp. Suppose G is a finitely generated group with a finite generating set X such that the word problem is a context-free language. One first observes that for every finitely generated subgroup H of G is finitely presentable and that for every finite marked generating set Y of H the word problem is also context-free. In particular, for a finitely generated group the property of having