RE Closure Under Right Quotient

This file proves that recursively enumerable languages over finite alphabets are closed under right quotient, both by another RE language and by a regular language. The key result is RE_of_RE_rightQuotient_RE: a search witness consists of a suffix v, a derivation sequence for w ++ v in the grammar for L, and a derivation sequence for v in the grammar for R.

Main declarations

• reRightQuotientTest
• reRightQuotientTest_computable₂
• RE_of_RE_rightQuotient_RE
• RE_closedUnderRightQuotient
• reRightQuotientRegularTest
• reRightQuotientRegularTest_computable₂
• RE_of_RE_rightQuotient_regular
• RE_closedUnderRightQuotientWithRegular

def reRightQuotientTest {T : Type} [DecidableEq T] (g₁ g₂ : grammar T) [DecidableEq g₁.nt] [DecidableEq g₂.nt] (p : List T × List (ℕ × ℕ) × List (ℕ × ℕ)) (w : List T) : Bool

Search test for membership in the right quotient of two grammar languages.

Equations

• reRightQuotientTest g₁ g₂ p w = (grammarTest g₁ p.2.1 (w ++ p.1) && grammarTest g₂ p.2.2 p.1)

theorem reRightQuotientTest_computable₂ {T : Type} [DecidableEq T] [Primcodable T] (g₁ g₂ : grammar T) [DecidableEq g₁.nt] [DecidableEq g₂.nt] [Primcodable g₁.nt] [Primcodable g₂.nt] : Computable₂ (reRightQuotientTest g₁ g₂)

The suffix-and-two-derivations search test for right quotient is computable.

theorem RE_of_RE_rightQuotient_RE {T : Type} [DecidableEq T] [Fintype T] (L R : Language T) (hL : is_RE L) (hR : is_RE R) : is_RE (L / R)

RE languages are closed under right quotient with RE languages.

theorem RE_closedUnderRightQuotient {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderRightQuotient is_RE

The class of RE languages is closed under right quotient.

def reRightQuotientRegularTest {T σ : Type} [DecidableEq T] (g : grammar T) [DecidableEq g.nt] (M : DFA T σ) [DecidablePred fun (x : σ) => x ∈ M.accept] (p : List T × List (ℕ × ℕ)) (w : List T) : Bool

Search test for membership in the right quotient of a grammar language by a DFA language.

Equations

• reRightQuotientRegularTest g M p w = (grammarTest g p.2 (w ++ p.1) && decide (M.eval p.1 ∈ M.accept))

theorem reRightQuotientRegularTest_computable₂ {T σ : Type} [DecidableEq T] [Primcodable T] [Primcodable σ] [Finite T] [Finite σ] (g : grammar T) [DecidableEq g.nt] [Primcodable g.nt] (M : DFA T σ) [DecidablePred fun (x : σ) => x ∈ M.accept] : Computable₂ (reRightQuotientRegularTest g M)

The suffix-and-derivation search test for right quotient by a DFA language is computable.

theorem RE_of_RE_rightQuotient_regular {T : Type} [DecidableEq T] [Fintype T] (L R : Language T) (hL : is_RE L) (hR : R.IsRegular) : is_RE (L / R)

RE languages are closed under right quotient with regular languages.

theorem RE_closedUnderRightQuotientWithRegular {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderRightQuotientWithRegular is_RE

The class of RE languages is closed under right quotient with regular languages.