RE Closure Under Terminal Bijection

This file proves closure of recursively enumerable languages under bijective renaming of terminals.

The key construction is bijection_grammar, which maps terminals in all rule components via an equivalence π : T₁ ≃ T₂. The main result bijection_grammar_language shows that this grammar generates exactly the π-image of the original language. This is then used by the context-free and context-sensitive bijection proofs via commutativity with their respective embeddings.

Main declarations

• map_symbol
• map_symbol_fn
• bijection_grule
• bijection_grammar
• map_grammar
• bijection_grammar_language
• map_grammar_language_of_leftInverse
• RE_of_map_injective_RE
• RE_of_bijemap_RE

def map_symbol {T₁ T₂ N : Type} (π : T₁ ≃ T₂) : symbol T₁ N → symbol T₂ N

Map a symbol along a terminal equivalence, leaving nonterminals unchanged.

Equations

• map_symbol π (symbol.terminal t) = symbol.terminal (π t)
• map_symbol π (symbol.nonterminal n) = symbol.nonterminal n

def map_symbol_inv {T₁ T₂ N : Type} (π : T₁ ≃ T₂) : symbol T₂ N → symbol T₁ N

Map a symbol back along the inverse equivalence.

Equations

• map_symbol_inv π (symbol.terminal t) = symbol.terminal (π.symm t)
• map_symbol_inv π (symbol.nonterminal n) = symbol.nonterminal n

def map_symbol_fn {T₁ T₂ N : Type} (f : T₁ → T₂) : symbol T₁ N → symbol T₂ N

Map terminals along an arbitrary function, leaving nonterminals unchanged.

Equations

• map_symbol_fn f (symbol.terminal t) = symbol.terminal (f t)
• map_symbol_fn f (symbol.nonterminal n) = symbol.nonterminal n

@[simp]

theorem map_symbol_fn_comp {T₁ T₂ N : Type} (f : T₁ → T₂) (g : T₂ → T₁) (s : symbol T₁ N) : map_symbol_fn g (map_symbol_fn f s) = map_symbol_fn (g ∘ f) s

@[simp]

theorem map_symbol_fn_leftInverse {T₁ T₂ N : Type} {f : T₁ → T₂} {g : T₂ → T₁} (hfg : Function.LeftInverse g f) (s : symbol T₁ N) : map_symbol_fn g (map_symbol_fn f s) = s

@[simp]

theorem map_symbol_inv_map_symbol {T₁ T₂ N : Type} (π : T₁ ≃ T₂) (s : symbol T₁ N) : map_symbol_inv π (map_symbol π s) = s

@[simp]

theorem map_symbol_map_symbol_inv {T₁ T₂ N : Type} (π : T₁ ≃ T₂) (s : symbol T₂ N) : map_symbol π (map_symbol_inv π s) = s

def bijection_grule {T₁ T₂ N : Type} (π : T₁ ≃ T₂) (r : grule T₁ N) : grule T₂ N

Map an unrestricted grammar rule along a terminal equivalence.

Equations

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

def bijection_grammar {T₁ T₂ : Type} (g : grammar T₁) (π : T₁ ≃ T₂) : grammar T₂

Map an unrestricted grammar along a terminal equivalence.

Equations

• bijection_grammar g π = { nt := g.nt, initial := g.initial, rules := List.map (bijection_grule π) g.rules }

def map_grammar {T₁ T₂ : Type} (g : grammar T₁) (f : T₁ → T₂) : grammar T₂

Map an unrestricted grammar along an arbitrary terminal map.

Equations

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

theorem bijection_grammar_language {T₁ T₂ : Type} (g : grammar T₁) (π : T₁ ≃ T₂) : grammar_language (bijection_grammar g π) = (grammar_language g).bijemapLang π

The bijection grammar generates exactly the π-image of the original language. This is the core result from which all class-specific bijection closure theorems are derived.

theorem map_grammar_language_of_leftInverse {T₁ T₂ : Type} (g : grammar T₁) {f : T₁ → T₂} {g' : T₂ → T₁} (hfg : Function.LeftInverse g' f) : grammar_language (map_grammar g f) = (Language.map f) (grammar_language g)

If g is a left inverse of f, mapping an unrestricted grammar along f generates exactly the Language.map f image of the original language.

theorem RE_of_map_injective_RE {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) : is_RE L → is_RE ((Language.map f) L)

RE languages are closed under injective terminal maps.

theorem RE_of_bijemap_RE {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_RE L → is_RE (L.bijemapLang π)

The class of RE languages is closed under bijective terminal renaming.

theorem RE_of_bijemap_RE_rev {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_RE (L.bijemapLang π) → is_RE L

The converse direction.

@[simp]

theorem RE_bijemap_iff_RE {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_RE (L.bijemapLang π) ↔ is_RE L

A language is RE iff its image under a bijection of terminal alphabets is RE.