Autosegmental Strictly Local stringsets

[Jar19]'s class ASL^g: a stringset described by a forbidden-subgraph grammar B over autosegmental representations, interpreted through a realization g (Realization.lean). A string is in the class iff its realization avoids every forbidden subgraph in B.

This unifies the autosegmental and subregular layers. It is the same construction as the tier-based strictly local sets: both a subregular class as the preimage of a local base condition along a free-monoid homomorphism.

  TSL  =  tierProject ⁻¹' (SL-language)        -- string→tier-string projection
  ASL  =  realize g₀  ⁻¹' { A | isFreeOf B A } -- string→AR realization

tierProject (Core/Computability/Subregular/Language/TierStrictlyLocal.lean) and realize (Realization.lean) are both concat-distributing free-monoid homs; the difference is only the codomain — a tier string (discarding off-tier material) vs an AR (keeping the association lines). That extra structure is why [Jar19] finds ASL and TSL incomparable.

def Autosegmental.isFreeOf {α : Type u_2} {β : Type u_3} (B : List (Graph α β)) (A : AR α β) : Prop

A banned-subgraph grammar as an AR object-property: the ARs free of every forbidden pattern in B ([Jar16] Ch. 5's L^NL_G, packaged for AR).

Equations

• Autosegmental.isFreeOf B A = A.Free B

@[implicit_reducible]

instance Autosegmental.instDecidableIsFreeOfOfDecidableEq {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] (B : List (Graph α β)) (A : AR α β) : Decidable (isFreeOf B A)

Equations

• Autosegmental.instDecidableIsFreeOfOfDecidableEq B A = Autosegmental.instDecidableIsFreeOfOfDecidableEq._aux_1 B A

def Autosegmental.ASL {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (B : List (Graph α β)) : Language S

The Autosegmental Strictly Local stringset of a realization g₀ and a forbidden grammar B ([Jar19]): the strings whose realization avoids B. The preimage of the AR object-property isFreeOf B along realize g₀ — the same shape as TSL.lang = tierProject ⁻¹' (SL-language), with the AR realization in place of the tier projection.

Equations

• Autosegmental.ASL g₀ B = Autosegmental.realize g₀ ⁻¹' {A : Autosegmental.AR α β | Autosegmental.isFreeOf B A}

@[simp]

theorem Autosegmental.mem_ASL {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (B : List (Graph α β)) (w : List S) : w ∈ ASL g₀ B ↔ isFreeOf B (realize g₀ w)

@[implicit_reducible]

instance Autosegmental.instDecidableMemListLanguageASLOfDecidableEq {S : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] (g₀ : S → AR α β) (B : List (Graph α β)) (w : List S) : Decidable (w ∈ ASL g₀ B)

Equations

• Autosegmental.instDecidableMemListLanguageASLOfDecidableEq g₀ B w = Autosegmental.instDecidableMemListLanguageASLOfDecidableEq._aux_1 g₀ B w

def Autosegmental.IsASL {S : Type u_1} (L : Language S) : Prop

A stringset is autosegmental strictly local when some realization and forbidden grammar present it ([Jar19]).

Equations

• Autosegmental.IsASL L = ∃ (α : Type) (β : Type) (g₀ : S → Autosegmental.AR α β) (B : List (Autosegmental.Graph α β)), L = Autosegmental.ASL g₀ B