Greibach's theorem

Definitions

Given a set Σ, often called "alphabet", the (infinite) set of all strings built from members of Σ is denoted by Σ^*. A formal language is a subset of Σ^*. If L₁ and L₂ are formal languages, their product L₁L₂ is defined as the set { w₁w₂ : w₁ ∈ L₁, w₂ ∈ L₂ } of all concatenations of a string w₁ from L₁ with a string w₂ from L₂. If L is a formal language and a is a symbol from Σ, their quotient L/a is defined as the set { w : wa ∈ L } of all strings that can be made members of L by appending an a. Various approaches are known from formal language theory to denote a formal language by a finite description, such as a formal grammar or a finite-state machine.

For example, using an alphabet Σ = { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 }, the set Σ^* consists of all (decimal representations of) natural numbers, with leading zeroes allowed, and the empty string, denoted as ε. The set L_div3 of all naturals divisible by 3 is an infinite formal language over Σ; it can be finitely described by the following regular grammar with start symbol S₀:

Examples for finite languages are {ε,1,2} and {0,2,4,6,8}; their product {ε,1,2}{0,2,4,6,8} yields the even numbers up to 28. The quotient of the set of prime numbers up to 100 by the symbol 7, 4, and 2 yields the language {ε,1,3,4,6,9}, {}, and {ε}, respectively.

Formal statement of the theorem

Greibach's theorem is independent of a particular approach to describe a formal language. It just considers a set C of formal languages over an alphabet Σ∪{#} such that

each language in C has a finite description,

each regular language over Σ∪{#} is in C,

given descriptions of languages L₁, L₂ ∈ C and of a regular language R ∈ C, a description of the products L₁R and RL₁, and of the union L₁∪L₂ can be effectively computed, and

it is undecidable for any member language L ∈ C with L ⊆ Σ^* whether L = Σ^*.

Let P be any nontrivial subset of C that contains all regular sets over Σ∪{#} and is closed under quotient by each single symbol in Σ∪{#}. Then the question whether L ∈ P for a given description of a language L ∈ C is undecidable.

Proof

Let M ⊆ Σ^*, such that M ∈ C, but M ∉ P. For any L ∈ C with L ⊆ Σ^*, define φ(L) = (M#Σ^*) ∪ (Σ^*#L). From a description of L, a description of φ(L) can be effectively computed.

Then L = Σ^* if and only if φ(L) ∈ P:

If L = Σ^*, then φ(L) = Σ^*#Σ^* is a regular language, and hence in P.

Else, some w ∈ Σ^* L exists, and the quotient φ(L)/(#w) equals M. Therefore, by repeated application of the quotient-closure property, φ(L) ∈ P would imply M = φ(L)/(#w) ∈ P, contradicting the definition of M.

Hence, if membership in P would be decidable for φ(L) from its description, so would be L’s equality to Σ^* from its description, which contradicts the definition of C.

Applications

Using Greibach's theorem, it can be shown that the following problems are undecidable:

Given a context-free grammar, does it describe a regular language?

Proof: The class of context-free languages, and the set of regular languages, satisfies the above properties of C, and P, respectively.

Given a context-free language, is it inherently ambiguous?

Proof: The class of context-free languages, and the set of context-free languages that aren't inherently ambiguous, satisfies the above properties of C, and P, respectively.

Given a context-sensitive grammar, does it describe a context-free language?

See also Context-free grammar#Being in a lower or higher level of the Chomsky hierarchy.