Langlib

Langlib.Classes.RecursivelyEnumerable.Closure.Intersection

RE Closure Under Intersection #

This file proves the search-level closure theorem for recursively enumerable languages under intersection. The key result is RE_of_RE_i_RE: after replacing both grammar witnesses by finite-nonterminal equivalents, a single computable test checks both derivation witnesses and the existing search-to-TM compiler turns that test back into an RE witness.

Main declarations #

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

Search test for membership in the intersection of two grammar languages.

Equations
Instances For
    source
    theorem reIntersectionTest_computable₂ {T : Type} [DecidableEq T] (g₁ g₂ : grammar T) [DecidableEq g₁.nt] [DecidableEq g₂.nt] [Primcodable T] [Primcodable g₁.nt] [Primcodable g₂.nt] :
    Computable₂ (reIntersectionTest g₁ g₂)

    The two-witness intersection search test is computable.

    source
    theorem RE_of_RE_i_RE {T : Type} [DecidableEq T] [Fintype T] (L₁ L₂ : Language T) :
    is_RE L₁ ∧ is_RE L₂ → is_RE (L₁ ⊓ L₂)

    Recursively enumerable languages over a finite alphabet are closed under intersection.

    source
    theorem RE_closedUnderIntersection {T : Type} [DecidableEq T] [Fintype T] :
    ClosedUnderIntersection is_RE

    The class of recursively enumerable languages is closed under intersection.

    source
    theorem RE_of_RE_i_regular {T : Type} [DecidableEq T] [Fintype T] (L R : Language T) :
    is_RE L → R.IsRegular → is_RE (L ⊓ R)

    RE languages are closed under intersection with a Mathlib-regular language.

    source
    theorem RE_closedUnderIntersectionWithRegular {T : Type} [DecidableEq T] [Fintype T] :
    ClosedUnderIntersectionWithRegular is_RE

    The class of RE languages is closed under intersection with regular languages.