Autosegmental strictly local languages

A realization r maps strings to autosegmental representations, and a banned-subgraph grammar B describes the strings whose realization contains no factor of B, Jardine's L(B^g); the languages so described are the autosegmental strictly local class ASL^g. Such a language is downward closed under containment of realizations, which is how Jardine separates ASL from other classes. Strings themselves are one-tier representations, and at the string realization the class contains every strictly local language with finitely many forbidden factors, the parallel Jardine draws between banned subgraphs and banned substrings. For grammars without association lines the class is a Boolean combination of tier-projected factor constraints, hence star-free.

Main definitions

• Language.bannedSubgraph r B: the strings whose realization avoids the grammar B.
• Language.IsAutosegmentalStrictlyLocal r L: some banned-subgraph grammar describes L.

Main results

• Language.IsAutosegmentalStrictlyLocal.mem_of_factorEmbeds: an autosegmental strictly local language is downward closed under containment of realizations.
• Language.bannedSubgraph_ofList_boundary: a forbidden-factor SL_k language is the banned-subgraph language of its factors over boundary-padded strings.
• Language.bannedSubgraph_realize_eq_of_link_free, Language.isStarFree_bannedSubgraph_realize: without lines, a banned-subgraph language is an intersection of unions of tier-avoidance preimages, and so star-free.

Implementation notes

The class is parametrized by the realization itself rather than by a primitive map: Jardine's ASL^g is the class at the merging realization of g with border primitives, and the unmerged realization and the string realization are other instances. The grammar's factors live in the realization's universe. Jardine bans only connected factors (Autosegmental/Factors.lean), so the class here contains his and its separation results are the stronger statements.

References

• [Jar16b]
• [Jar19]

def Language.bannedSubgraph {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} (r : List S → Autosegmental.TieredAR ι τ) [∀ (w : List S), Finite (r w).obj.V] (B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }) : Language S

The strings whose realization under r avoids every factor of the grammar B.

Equations

• Language.bannedSubgraph r B = {w : List S | Autosegmental.AR.Free (r w) B}

def Language.IsAutosegmentalStrictlyLocal {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} (r : List S → Autosegmental.TieredAR ι τ) [∀ (w : List S), Finite (r w).obj.V] (L : Language S) : Prop

A language is autosegmental strictly local over r when a banned-subgraph grammar describes it.

Equations

• Language.IsAutosegmentalStrictlyLocal r L = ∃ (B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }), Language.bannedSubgraph r B = L

@[simp]

theorem Language.mem_bannedSubgraph {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] {B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }} {w : List S} : w ∈ bannedSubgraph r B ↔ Autosegmental.AR.Free (r w) B

theorem Language.isAutosegmentalStrictlyLocal_bannedSubgraph {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] {B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }} : IsAutosegmentalStrictlyLocal r (bannedSubgraph r B)

@[simp]

theorem Language.bannedSubgraph_nil {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] : bannedSubgraph r [] = Set.univ

theorem Language.bannedSubgraph_cons {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] {B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }} (F : { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }) : bannedSubgraph r (F :: B) = {w : List S | Autosegmental.AR.FactorEmbeds (↑F) (r w)}ᶜ ⊓ bannedSubgraph r B

A grammar's language is the intersection of its factors' avoidance languages.

Downward closure

theorem Language.mem_bannedSubgraph_of_factorEmbeds {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] {B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }} {u v : List S} (h : Autosegmental.AR.FactorEmbeds (r u) (r v)) (hv : v ∈ bannedSubgraph r B) : u ∈ bannedSubgraph r B

A banned-subgraph language is downward closed under containment of realizations.

theorem Language.IsAutosegmentalStrictlyLocal.mem_of_factorEmbeds {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] {L : Language S} {u v : List S} (hL : IsAutosegmentalStrictlyLocal r L) (h : Autosegmental.AR.FactorEmbeds (r u) (r v)) (hv : v ∈ L) : u ∈ L

theorem Language.not_isAutosegmentalStrictlyLocal_of_factorEmbeds {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} {r : List S → Autosegmental.TieredAR ι τ} [∀ (w : List S), Finite (r w).obj.V] {L : Language S} {u v : List S} (h : Autosegmental.AR.FactorEmbeds (r u) (r v)) (hu : u ∉ L) (hv : v ∈ L) : ¬IsAutosegmentalStrictlyLocal r L

A language that separates two strings whose realizations are contained one in the other is not autosegmental strictly local.

Strings as one-tier representations

theorem Language.bannedSubgraph_ofList_boundary {α : Type u_1} {Fs : List (Augmented α)} {k : ℕ} (hk : ∀ f ∈ Fs, List.length f = k) : bannedSubgraph (fun (w : List α) => Autosegmental.AR.ofList (boundary k w)) (List.map (fun (f : List (Option α)) => ⟨Autosegmental.AR.ofList f, ⋯⟩) Fs) = StrictlyLocalGrammar.language k (StrictlyLocalGrammar.ofForbidden {f : Augmented α | f ∈ Fs})

A forbidden-factor SL_k language is the banned-subgraph language of its forbidden factors over boundary-padded strings.

theorem Language.isAutosegmentalStrictlyLocal_ofForbidden {α : Type u_1} {Fs : List (Augmented α)} {k : ℕ} (hk : ∀ f ∈ Fs, List.length f = k) : IsAutosegmentalStrictlyLocal (fun (w : List α) => Autosegmental.AR.ofList (boundary k w)) (StrictlyLocalGrammar.language k (StrictlyLocalGrammar.ofForbidden {f : Augmented α | f ∈ Fs}))

At the boundary-padded string realization, every finite forbidden-factor SL_k language is autosegmental strictly local.

Grammars without association lines

theorem Language.setOf_factorEmbeds_realize_eq_of_link_free {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} (g : S → Autosegmental.TieredAR ι τ) [∀ (s : S), Finite (g s).obj.V] (F : Autosegmental.TieredAR ι τ) [Finite F.obj.V] (hF : ∀ (i j : ι) (p q : ℕ), ¬Autosegmental.AR.link F i j p q) : {w : List S | Autosegmental.AR.FactorEmbeds F (Autosegmental.AR.realize g w)} = ⋂ (i : ι), {w : List S | Autosegmental.AR.tierWord i <:+: (Autosegmental.AR.tierProj g i) (FreeMonoid.ofList w)}

The strings whose realization contains a link-free factor are those whose tier projections contain its tier words.

theorem Language.bannedSubgraph_realize_eq_of_link_free {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} (g : S → Autosegmental.TieredAR ι τ) [∀ (s : S), Finite (g s).obj.V] (B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }) (hB : ∀ F ∈ B, ∀ (i j : ι) (p q : ℕ), ¬Autosegmental.AR.link (↑F) i j p q) : bannedSubgraph (Autosegmental.AR.realize g) B = ⋂ F ∈ B, ⋃ (i : ι), {w : List S | ¬Autosegmental.AR.tierWord i <:+: (Autosegmental.AR.tierProj g i) (FreeMonoid.ofList w)}

Without lines, a banned-subgraph language is an intersection over the factors of unions over the tiers of tier-avoidance preimages.

theorem Language.isStarFree_bannedSubgraph_realize {S : Type u_1} {ι : Type u₁} {τ : ι → Type u₂} (g : S → Autosegmental.TieredAR ι τ) [∀ (s : S), Finite (g s).obj.V] [Finite ι] (B : List { F : Autosegmental.TieredAR ι τ // Finite F.obj.V }) (hB : ∀ F ∈ B, ∀ (i j : ι) (p q : ℕ), ¬Autosegmental.AR.link (↑F) i j p q) : (bannedSubgraph (Autosegmental.AR.realize g) B).IsStarFree

Without lines, a banned-subgraph language over a realization is star-free.