Abstract Closure Predicates for Language Classes

This file defines predicates capturing common closure properties of language classes.

A language class P : Language α → Prop is closed under an operation if applying the operation to languages in P yields another language in P.

For same-alphabet operations (union, intersection, complement, concatenation, Kleene star, reversal, intersection/quotient with regular), closedness is expressed as a property of P : Language α → Prop.

For cross-alphabet operations (string homomorphism, ε-free homomorphism), closedness is expressed as a property of an alphabet-indexed predicate isP : ∀ {α : Type*}, Language α → Prop.

Main definitions

• ClosedUnderUnion
• ClosedUnderIntersection
• ClosedUnderComplement
• ClosedUnderConcatenation
• ClosedUnderKleeneStar
• ClosedUnderReverse
• ClosedUnderIntersectionWithRegular
• ClosedUnderRightQuotient
• ClosedUnderRightQuotientWithRegular
• ClosedUnderHomomorphism
• ClosedUnderEpsFreeHomomorphism
• ClosedUnderInverseHomomorphism
• ClosedUnderSubstitution

def ClosedUnderUnion {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under union.

Equations

• ClosedUnderUnion P = ∀ (L₁ L₂ : Language α), P L₁ → P L₂ → P (L₁ + L₂)

def ClosedUnderIntersection {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under intersection.

Equations

• ClosedUnderIntersection P = ∀ (L₁ L₂ : Language α), P L₁ → P L₂ → P (L₁ ⊓ L₂)

def ClosedUnderComplement {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under complement.

Equations

• ClosedUnderComplement P = ∀ (L : Language α), P L → P Lᶜ

def ClosedUnderConcatenation {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under concatenation.

Equations

• ClosedUnderConcatenation P = ∀ (L₁ L₂ : Language α), P L₁ → P L₂ → P (L₁ * L₂)

def ClosedUnderKleeneStar {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under Kleene star.

Equations

• ClosedUnderKleeneStar P = ∀ (L : Language α), P L → P (KStar.kstar L)

def ClosedUnderReverse {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under language reversal.

Equations

• ClosedUnderReverse P = ∀ (L : Language α), P L → P L.reverse

def ClosedUnderIntersectionWithRegular {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under intersection with regular languages.

Equations

• ClosedUnderIntersectionWithRegular P = ∀ (L : Language α), P L → ∀ (R : Language α), R.IsRegular → P (L ⊓ R)

def ClosedUnderRightQuotient {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under right quotient (with any language from the same class).

Equations

• ClosedUnderRightQuotient P = ∀ (L₁ L₂ : Language α), P L₁ → P L₂ → P (L₁.rightQuotient L₂)

def ClosedUnderRightQuotientWithRegular {α : Type u_1} (P : Language α → Prop) : Prop

A language class is closed under right quotient with regular languages.

Equations

• ClosedUnderRightQuotientWithRegular P = ∀ (L : Language α), P L → ∀ (R : Language α), R.IsRegular → P (L.rightQuotient R)

def ClosedUnderHomomorphism (isP : {α : Type} → [Fintype α] → Language α → Prop) : Prop

A finite-alphabet-indexed language class is closed under string homomorphism.

Here isP is a predicate on languages that is uniform across finite alphabets. Note: Language.homomorphicImage works in universe Type, so isP ranges over Type.

Equations

• ClosedUnderHomomorphism isP = ∀ {α β : Type} [inst : Fintype α] [inst_1 : Fintype β] (L : Language α) (h : α → List β), isP L → isP (L.homomorphicImage h)

def ClosedUnderEpsFreeHomomorphism (isP : {α : Type} → [Fintype α] → Language α → Prop) : Prop

A finite-alphabet-indexed language class is closed under ε-free string homomorphism.

Equations

• ClosedUnderEpsFreeHomomorphism isP = ∀ {α β : Type} [inst : Fintype α] [inst_1 : Fintype β] (L : Language α) (h : α → List β), IsEpsFreeHomomorphism h → isP L → isP (L.homomorphicImage h)

def ClosedUnderInverseHomomorphism (isP : {α : Type} → [Fintype α] → Language α → Prop) : Prop

A finite-alphabet-indexed language class is closed under inverse string homomorphism.

The inverse homomorphic image of L : Language β under h : α → List β is { w : List α | w.flatMap h ∈ L }. Both alphabets are finite, matching the finite-alphabet convention used by the other cross-alphabet closure predicates.

Equations

• ClosedUnderInverseHomomorphism isP = ∀ {α β : Type} [inst : Fintype α] [inst_1 : Fintype β] (L : Language β) (h : α → List β), isP L → isP {w : List α | List.flatMap h w ∈ L}

def ClosedUnderSubstitution (isP : {α : Type} → [Fintype α] → Language α → Prop) : Prop

A finite-alphabet-indexed language class is closed under substitution.

Both alphabets are finite, matching the finite-alphabet convention used by the TM-recognizability bridge and the other cross-alphabet closure predicates.

Equations

• ClosedUnderSubstitution isP = ∀ {α β : Type} [inst : Fintype α] [inst_1 : Fintype β] (L : Language α) (f : α → Language β), isP L → (∀ (a : α), isP (f a)) → isP (L.subst f)

Strictness from property mismatch

theorem strict_subset_of_subset_different_property {α : Type u_1} {P Q : Language α → Prop} {X : (Language α → Prop) → Prop} (hsub : ∀ (L : Language α), P L → Q L) (hX_iff : ∀ {R S : Language α → Prop}, (∀ (L : Language α), R L ↔ S L) → X R → X S) (hPX : X P) (hQnotX : ¬X Q) : setOf P ⊂ setOf Q

If P ⊆ Q, P has a class property X, Q does not, and X is invariant under pointwise equivalence of language classes, then the inclusion P ⊆ Q is strict.

The invariance hypothesis is necessary: an arbitrary predicate transformer X : (Language α → Prop) → Prop need not be transportable from P to an extensionally equal class.