Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every context-free language has an equivalent grammar in Greibach normal form

Statement

Every context-free grammar has an equivalent context-free grammar in Greibach normal form.

Facts & Assumptions

Given: A context-free grammar G.

[L1]

By Every context-free language has an equivalent grammar in Chomsky normal form, we may first replace G by an equivalent grammar in Chomsky normal form.

[L2]

If a production AuBv is replaced by the family Auw1v,,Auwmv formed from all productions of B, then the generated language is preserved, by Substituting a variable's productions into a leading variable occurrence preserves the language.

[L3]

Eliminating immediate left recursion preserves the generated language, by Eliminating immediate left recursion preserves the language.

[L4]

Greibach normal form means that every nonexceptional production has the form Aaα with leading terminal a, by Greibach normal form.

Proof

technique · direct
1.1

Replace G by an equivalent CNF grammar G1 as in [L1], and order its original variables as A1,,An. In a forward pass through this list, fix Ai and repeatedly use [L2] to remove every production of the form AiAjα with j<i. When that is done, use [L3] to eliminate the remaining immediate left-recursive productions AiAiβ, introducing an auxiliary variable Bi if needed. After stage i, every production of Ai begins either with a terminal or with an original variable Ak satisfying k>i, and every new production of Bi begins either with a terminal or with an original variable.

L1L2L3construct
2.1

In particular, after the forward pass the productions of An already begin with terminals, because there is no index k>n. Now argue downward on i=n1,n2,,1. Assume the productions of Ai+1,,An already begin with terminals. Every production of Ai begins either with a terminal or with some Ak having k>i by step 1.1, so repeated use of [L2] substitutes the full terminal-leading production family of each such Ak into the leading occurrence. Thus every production of Ai can also be made terminal-leading without changing the language.

L2step 1.1induction
3.1

The same downward substitutions clean every auxiliary variable introduced during the left-recursion eliminations. By step 1.1, each production of such a Bi already begins either with a terminal or with an original variable Ak. Once the productions of each Ak are terminal-leading by step 2.1, repeated use of [L2] removes that leading variable from the productions of Bi as well. Therefore, after finitely many substitutions, every production in the whole grammar begins with a terminal, except possibly the start-symbol rule Sε.

L2step 1.1step 2.1
4.1

Because the construction started from CNF, the symbols after the first terminal in any rewritten production are variables, and the optional start-symbol rule Sε is preserved only in the exceptional case allowed by [L4]. Hence the final grammar is in Greibach normal form, and [L2] and [L3] preserved equivalence throughout.

L4step 1.1step 2.1step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources