a^n b^n as a Linear Language

This file constructs a linear grammar for {a^n b^n} and proves that the language is linear.

Main results

• linear_grammar_anbn_language — the grammar generates exactly anbn
• anbn_is_Linear — {a^n b^n} is linear

def linear_grammar_anbn : grammar Bool

An unrestricted grammar for the language {aⁿbⁿ | n ∈ ℕ} with linear rules. Rules: S → aSb (i.e., [] S [] → [a, S, b]) S → ε (i.e., [] S [] → [])

Equations

• One or more equations did not get rendered due to their size.

theorem linear_grammar_anbn_is_linear : grammar_linear linear_grammar_anbn

The grammar linear_grammar_anbn is linear.

theorem linear_grammar_anbn_derives_n (n : ℕ) : grammar_derives linear_grammar_anbn [symbol.nonterminal ()] (List.replicate n (symbol.terminal false) ++ [symbol.nonterminal ()] ++ List.replicate n (symbol.terminal true))

Derivation in linear_grammar_anbn can produce aⁿSbⁿ.

theorem linear_grammar_anbn_derives_final (n : ℕ) : grammar_derives linear_grammar_anbn (List.replicate n (symbol.terminal false) ++ [symbol.nonterminal ()] ++ List.replicate n (symbol.terminal true)) (List.replicate n (symbol.terminal false) ++ List.replicate n (symbol.terminal true))

Derivation in linear_grammar_anbn: apply ε-rule to get aⁿbⁿ.

theorem anbn_sub_linear_grammar_anbn_language (w : List Bool) : w ∈ anbn → w ∈ grammar_language linear_grammar_anbn

Every word in anbn is generated by linear_grammar_anbn.

theorem linear_grammar_anbn_language_sub_anbn (w : List Bool) : w ∈ grammar_language linear_grammar_anbn → w ∈ anbn

Every word generated by linear_grammar_anbn is in anbn.

theorem linear_grammar_anbn_language : grammar_language linear_grammar_anbn = anbn

The grammar linear_grammar_anbn generates exactly {aⁿbⁿ}.

theorem anbn_is_Linear : is_Linear anbn

The language {aⁿbⁿ} is linear.