RE Closure Under Reversal

This file proves closure of recursively enumerable languages under reversal.

The key construction reversal_grammar reverses each rule of an unrestricted grammar. The central result grammar_language_reversal_grammar shows that the language of the reversed grammar equals the reversal of the original language. This fact is then reused by the context-free and context-sensitive reversal proofs, avoiding duplicated derivation arguments.

Main declarations

• reversal_grule — reverse a single unrestricted rule
• reversal_grammar — reverse every rule of an unrestricted grammar
• grammar_language_reversal_grammar — language of reversed grammar = reversed language
• RE_of_reverse_RE

def reversal_grule {T N : Type} (r : grule T N) : grule T N

Reverse a single unrestricted rule by swapping and reversing the left/right context and reversing the output string.

Equations

• reversal_grule r = { input_L := r.input_R.reverse, input_N := r.input_N, input_R := r.input_L.reverse, output_string := r.output_string.reverse }

theorem dual_of_reversal_grule {T N : Type} (r : grule T N) : reversal_grule (reversal_grule r) = r

theorem reversal_grule_reversal_grule {T N : Type} : reversal_grule ∘ reversal_grule = id

def reversal_grammar {T : Type} (g : grammar T) : grammar T

Reverse every rule of an unrestricted grammar.

Equations

• reversal_grammar g = { nt := g.nt, initial := g.initial, rules := List.map reversal_grule g.rules }

theorem dual_of_reversal_grammar {T : Type} (g : grammar T) : reversal_grammar (reversal_grammar g) = g

theorem grammar_language_reversal_grammar {T : Type} (g : grammar T) : grammar_language (reversal_grammar g) = (grammar_language g).reverse

The language of the reversed grammar is exactly the reversal of the original language.

This is the key lemma that is reused by the context-free and context-sensitive reversal closure proofs, so that the derivation-reversal argument need only be given once.

theorem RE_of_reverse_RE {T : Type} (L : Language T) : is_RE L → is_RE L.reverse

The class of recursively-enumerable languages is closed under reversal.

theorem RE_of_reverse_RE_rev {T : Type} (L : Language T) : is_RE L.reverse → is_RE L

The converse direction: if the reversal is RE then so is the original.

@[simp]

theorem RE_reverse_iff_RE {T : Type} (L : Language T) : is_RE L.reverse ↔ is_RE L

A language is RE iff its reversal is RE.

theorem RE_closedUnderReverse {T : Type} : ClosedUnderReverse is_RE

The class of recursively enumerable languages is closed under reversal.