Multitier extensions of subregular classes

A tier projection erases the symbols off a tier T : α → Bool. The multitier closure IsBTC 𝒞 of a class 𝒞 : Language α → Prop is the Boolean algebra generated by the preimages of 𝒞-languages under tier projections.

Main definitions

• IsTierBased 𝒞: preimages of 𝒞-languages under a Boolean tier projection.
• IsBTC 𝒞: the multitier closure, the BooleanSubalgebra.closure of the tier-projected family.
• IsBTSL/IsBTSP/IsBTD/IsBTK/IsBTLI/IsBTN: its six specializations, to the strictly local, strictly piecewise, definite, reverse definite, generalized definite and finite-or-cofinite languages. Lambert calls the first the multitier locally testable languages.
• IsBTC.Indist: tier-indistinguishability, the congruence behind membership refutation.
• tierWord, tierPrefix, tierSuffix: the literals of a propositional logic over tier affixes.

Main results

• IsBTC.mono: monotonicity in the base class.
• isTierStrictlyLocal_iff_isTierBased: TSL_k is the tier-based closure of SL_k.
• IsBTC.mem_languageVariety: the multitier closure of a class lies in every variety of languages containing it, since a tier projection is a homomorphism of free monoids.
• IsBTC.isStarFree: its instance at the aperiodic monoids, so all six specializations are star-free over a finite alphabet.
• IsBTC.mem_iff_of_indist and not_isBTC_of_indist: membership respects tier-indistinguishability, yielding the standard non-membership argument.

Implementation notes

IsTierBased/IsBTC.Indist quantify over Bool tiers T : α → Bool, avoiding an ∃ T, ∃ _ : DecidablePred T, … witness. A Prop tier with [DecidablePred], as in TierStrictlyLocalGrammar, projects by the filter of its decide, which is already a Bool tier, so isTierStrictlyLocal_iff_isTierBased needs no conversion lemma.

References

• [Lam26]
• [HRT11]

Tier-based language families

def Language.IsTierBased {α : Type u_1} (𝒞 : Language α → Prop) (L : Language α) : Prop

A language is tier-based for a class 𝒞 when it is the preimage of a 𝒞-language under the projection to some Boolean tier.

Equations

• Language.IsTierBased 𝒞 L = ∃ (T : α → Bool) (L' : Language α), L = {w : List α | List.filter T w ∈ L'} ∧ 𝒞 L'

theorem Language.IsTierBased.of_class {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : 𝒞 L) : IsTierBased 𝒞 L

Every 𝒞-language is tier-based for 𝒞 via the universal tier, which erases no symbol.

theorem Language.IsTierBased.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} {L : Language α} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) (hL : IsTierBased 𝒞 L) : IsTierBased 𝒟 L

Monotonicity in the base class.

The multitier closure

def Language.IsBTC {α : Type u_1} (𝒞 : Language α → Prop) (L : Language α) : Prop

The multitier closure of a class 𝒞 is the Boolean subalgebra of Language α generated by the tier-projected family IsTierBased 𝒞.

Equations

• Language.IsBTC 𝒞 L = (L ∈ BooleanSubalgebra.closure {L' : Language α | Language.IsTierBased 𝒞 L'})

theorem Language.IsBTC.base {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : IsTierBased 𝒞 L) : IsBTC 𝒞 L

A tier-based language lies in the closure.

theorem Language.IsBTC.inter {α : Type u_1} {𝒞 : Language α → Prop} {L₁ L₂ : Language α} (h₁ : IsBTC 𝒞 L₁) (h₂ : IsBTC 𝒞 L₂) : IsBTC 𝒞 (L₁ ⊓ L₂)

Closure under intersection.

theorem Language.IsBTC.union {α : Type u_1} {𝒞 : Language α → Prop} {L₁ L₂ : Language α} (h₁ : IsBTC 𝒞 L₁) (h₂ : IsBTC 𝒞 L₂) : IsBTC 𝒞 (L₁ ⊔ L₂)

Closure under union.

theorem Language.IsBTC.compl {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : IsBTC 𝒞 L) : IsBTC 𝒞 Lᶜ

Closure under complement.

theorem Language.IsBTC.of_class {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h : 𝒞 L) : IsBTC 𝒞 L

Every 𝒞-language is in IsBTC 𝒞, via the universal tier.

theorem Language.IsBTC.mono {α : Type u_1} {𝒞 𝒟 : Language α → Prop} {L : Language α} (h : ∀ (L : Language α), 𝒞 L → 𝒟 L) (hL : IsBTC 𝒞 L) : IsBTC 𝒟 L

Monotonicity of multitier closure in the base class.

Specializations

Each class of the paper is the multitier closure of a base class, so it is closed under the Boolean operations by IsBTC.inter, IsBTC.union and IsBTC.compl and contains the base class by IsBTC.of_class.

def Language.IsBTSL {α : Type u_1} (k : ℕ) : Language α → Prop

The multitier locally testable languages (BTSL) are the Boolean closure of the tier-projected SL_k languages.

Equations

• Language.IsBTSL k = Language.IsBTC fun (x : Language α) => x.IsStrictlyLocal k

def Language.IsBTSP {α : Type u_1} (k : ℕ) : Language α → Prop

The multitier strictly piecewise languages (BTSP) are the Boolean closure of the tier-projected SP_k languages.

Equations

• Language.IsBTSP k = Language.IsBTC fun (x : Language α) => x.IsStrictlyPiecewise k

def Language.IsBTD {α : Type u_1} (k : ℕ) : Language α → Prop

The multitier definite languages (BTD) are the Boolean closure of the tier-projected D_k languages.

Equations

• Language.IsBTD k = Language.IsBTC fun (x : Language α) => x.IsDefinite k

def Language.IsBTK {α : Type u_1} (k : ℕ) : Language α → Prop

The multitier reverse definite languages (BTK) are the Boolean closure of the tier-projected RD_k languages.

Equations

• Language.IsBTK k = Language.IsBTC fun (x : Language α) => x.IsReverseDefinite k

def Language.IsBTLI {α : Type u_1} (k : ℕ) : Language α → Prop

The multitier generalized definite languages (BTLI) are the Boolean closure of the tier-projected ℒℐ_k languages.

Equations

• Language.IsBTLI k = Language.IsBTC fun (x : Language α) => x.IsGeneralizedDefinite k

def Language.IsBTN {α : Type u_1} : Language α → Prop

The multitier finite-or-cofinite languages (BTN) are the Boolean closure of the tier-projected co/finite languages.

Equations

• Language.IsBTN = Language.IsBTC Language.IsFiniteOrCofinite

Cross-class inclusions

An inclusion of base classes lifts to their multitier closures by IsBTC.mono.

theorem Language.IsBTD.toIsBTLI {α : Type u_1} {L : Language α} {k : ℕ} (h : IsBTD k L) : IsBTLI k L

The inclusion D_k ⊆ ℒℐ_k lifts to BTD_k ⊆ BTLI_k.

theorem Language.IsBTK.toIsBTLI {α : Type u_1} {L : Language α} {k : ℕ} (h : IsBTK k L) : IsBTLI k L

The inclusion RD_k ⊆ ℒℐ_k lifts to BTK_k ⊆ BTLI_k.

Tier literals

The literals of a propositional logic over tier affixes: the words whose projection to a tier T is exactly xs, begins with xs, or ends in xs. Each lies in the multitier extension of the class its affix belongs to, with a window at least the length of the affix (strictly more for a whole tier word).

def Language.tierWord {α : Type u_1} (T : α → Bool) (xs : List α) : Language α

The tier word [⋊xs⋉]_T is the set of words whose projection to the tier T is xs.

Equations

• Language.tierWord T xs = {w : List α | List.filter T w ∈ {xs}}

def Language.tierPrefix {α : Type u_1} (T : α → Bool) (xs : List α) : Language α

The tier prefix [⋊xs]_T is the set of words whose projection to T begins with xs.

Equations

• Language.tierPrefix T xs = {w : List α | List.filter T w ∈ Language.ofPrefix xs}

def Language.tierSuffix {α : Type u_1} (T : α → Bool) (xs : List α) : Language α

The tier suffix [xs⋉]_T is the set of words whose projection to T ends in xs.

Equations

• Language.tierSuffix T xs = {w : List α | List.filter T w ∈ Language.ofSuffix xs}

@[simp]

theorem Language.mem_tierWord {α : Type u_1} {T : α → Bool} {xs w : List α} : w ∈ tierWord T xs ↔ List.filter T w = xs

@[simp]

theorem Language.mem_tierPrefix {α : Type u_1} {T : α → Bool} {xs w : List α} : w ∈ tierPrefix T xs ↔ xs <+: List.filter T w

@[simp]

theorem Language.mem_tierSuffix {α : Type u_1} {T : α → Bool} {xs w : List α} : w ∈ tierSuffix T xs ↔ xs <:+ List.filter T w

theorem Language.isBTN_tierWord {α : Type u_1} (T : α → Bool) (xs : List α) : (tierWord T xs).IsBTN

theorem Language.isBTD_tierWord {α : Type u_1} {k : ℕ} (T : α → Bool) (xs : List α) (hk : xs.length < k) : IsBTD k (tierWord T xs)

theorem Language.isBTK_tierWord {α : Type u_1} {k : ℕ} (T : α → Bool) (xs : List α) (hk : xs.length < k) : IsBTK k (tierWord T xs)

theorem Language.isBTK_tierPrefix {α : Type u_1} {k : ℕ} (T : α → Bool) (xs : List α) (hk : xs.length ≤ k) : IsBTK k (tierPrefix T xs)

theorem Language.isBTD_tierSuffix {α : Type u_1} {k : ℕ} (T : α → Bool) (xs : List α) (hk : xs.length ≤ k) : IsBTD k (tierSuffix T xs)

theorem Language.isBTK_ofPrefix {α : Type u_1} {k : ℕ} (xs : List α) (hk : xs.length ≤ k) : IsBTK k (ofPrefix xs)

theorem Language.isBTD_ofSuffix {α : Type u_1} {k : ℕ} (xs : List α) (hk : xs.length ≤ k) : IsBTD k (ofSuffix xs)

Tier-based strictly local languages

theorem Language.isTierStrictlyLocal_iff_isTierBased {α : Type u_1} {L : Language α} {k : ℕ} : IsTierStrictlyLocal k L ↔ IsTierBased (fun (x : Language α) => x.IsStrictlyLocal k) L

The tier-based strictly k-local languages are the tier-based closure of the strictly k-local ones, since a TierStrictlyLocalGrammar is a tier together with an SL_k language pulled back along erasure of the off-tier symbols.

theorem Language.IsTierStrictlyLocal.toIsBTSL {α : Type u_1} {L : Language α} {k : ℕ} (h : IsTierStrictlyLocal k L) : IsBTSL k L

Every tier-based strictly local language lies in the multitier closure of strictly local languages.

Refuting membership by indistinguishability

A language lies outside IsBTC 𝒞 when it separates two words that every 𝒞-language assigns the same membership under every tier projection. For the generalized definite languages it suffices that the two words share their length-k prefix and suffix on every tier.

def Language.IsBTC.Indist {α : Type u_1} (𝒞 : Language α → Prop) (w₁ w₂ : List α) : Prop

Two words are 𝒞-tier-indistinguishable when every 𝒞-language assigns them the same membership under every Bool tier projection.

Equations

• Language.IsBTC.Indist 𝒞 w₁ w₂ = ∀ (T : α → Bool) (L' : Language α), 𝒞 L' → (List.filter T w₁ ∈ L' ↔ List.filter T w₂ ∈ L')

theorem Language.IsBTC.Indist.refl {α : Type u_1} (𝒞 : Language α → Prop) (w : List α) : Indist 𝒞 w w

theorem Language.IsBTC.Indist.symm {α : Type u_1} {𝒞 : Language α → Prop} {w₁ w₂ : List α} (h : Indist 𝒞 w₁ w₂) : Indist 𝒞 w₂ w₁

theorem Language.IsBTC.Indist.trans {α : Type u_1} {𝒞 : Language α → Prop} {w₁ w₂ w₃ : List α} (h₁ : Indist 𝒞 w₁ w₂) (h₂ : Indist 𝒞 w₂ w₃) : Indist 𝒞 w₁ w₃

theorem Language.IsBTC.mem_iff_of_indist {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} {w₁ w₂ : List α} (hL : IsBTC 𝒞 L) (hindist : Indist 𝒞 w₁ w₂) : w₁ ∈ L ↔ w₂ ∈ L

Two 𝒞-tier-indistinguishable words have the same membership in every IsBTC 𝒞-language.

theorem Language.not_isBTC_of_indist {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} {w₁ w₂ : List α} (h_indist : IsBTC.Indist 𝒞 w₁ w₂) (h_w₁ : w₁ ∈ L) (h_w₂ : w₂ ∉ L) : ¬IsBTC 𝒞 L

If w₁ ∈ L and w₂ ∉ L but w₁ and w₂ are 𝒞-tier-indistinguishable, then L ∉ IsBTC 𝒞.

theorem Language.IsBTC.indist_isGeneralizedDefinite_of_tierAffixes {α : Type u_1} {k : ℕ} {w₁ w₂ : List α} (h : ∀ (T : α → Bool), Edge.left.takeAt k (List.filter T w₁) = Edge.left.takeAt k (List.filter T w₂) ∧ Edge.right.takeAt k (List.filter T w₁) = Edge.right.takeAt k (List.filter T w₂)) : Indist (fun (x : Language α) => x.IsGeneralizedDefinite k) w₁ w₂

Two words sharing their length-k prefix and suffix on every Bool tier are indistinguishable by the tier-projected generalized k-definite languages.

Varieties of languages

A tier projection is the free monoid endomorphism FreeMonoid.filter T, and a variety of languages is a Boolean algebra closed under inverse images of such endomorphisms, so it contains the multitier closure of any class it contains.

theorem Language.IsBTC.mem_languageVariety {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} {𝒱 : Monoid.LanguageVariety} (h𝒞 : ∀ (L : Language α), 𝒞 L → L ∈ 𝒱 α) (h : IsBTC 𝒞 L) : L ∈ 𝒱 α

The multitier closure of 𝒞 lies in every variety of languages containing 𝒞.

theorem Language.IsBTC.isStarFree {α : Type u_1} {𝒞 : Language α → Prop} {L : Language α} (h𝒞 : ∀ (L : Language α), 𝒞 L → L.IsStarFree) (h : IsBTC 𝒞 L) : L.IsStarFree

The multitier closure of a star-free base class is star-free.

theorem Language.IsBTSL.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : IsBTSL k L) : L.IsStarFree

theorem Language.IsBTSP.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : IsBTSP k L) : L.IsStarFree

theorem Language.IsBTLI.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : IsBTLI k L) : L.IsStarFree

theorem Language.IsBTD.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : IsBTD k L) : L.IsStarFree

theorem Language.IsBTK.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : IsBTK k L) : L.IsStarFree

theorem Language.IsBTN.isStarFree {α : Type u_1} {L : Language α} [Finite α] (h : L.IsBTN) : L.IsStarFree