Jardine (2019): the expressivity of autosegmental grammars

[Jar19] defines ASL^g — stringsets given by forbidden-subgraph grammars over autosegmental representations interpreted through a realization g — and places the tone class ASL^{gT} in the subregular hierarchy. This file instantiates the Autosegmental.ASL substrate with the tone realization gT and checks banned-subgraph constraints over its realizations.

Scope

Two realizations are checked, against the same forbidden tone melody *HLH:

• Autosegmental.realize uses the project's bridge-only concat (the coproduct), so an H-plateau Hⁿ stays n separate H nodes. Banning *HLH over realize then catches only a local H-L-H (three adjacent tonal nodes) — hlh_excluded.
• Autosegmental.realizeMerged (Collapse.lean) is [Jar19]'s OCP-merging g_T: g_T(Hⁿ) is a single H node multiply associated. Banning *HLH over realizeMerged becomes genuinely non-local — it forbids H⁺ L⁺ H⁺ for any plateau widths, because the plateaus collapse to single nodes before the melody is read (hlhTier_merged_excludes_plateau vs hlhTier_unmerged_admits_plateau).

Subregular placement

[Jar19] places the bridge-only class ASL strictly inside the star-free languages. We prove the link-free fragment: when no forbidden subgraph carries association lines, ASL g₀ B is star-free (Autosegmental.ASL.isStarFree_of_links_empty) — over any alphabet, no [Finite S] needed — because such a grammar is a Boolean combination of per-tier factor constraints, each the inverse image of a star-free contains-factor language ([Sch65] [McNP71]) along a tier projection. The *HLH tonal-tier melody hlhTier is one such constraint (hlhTier_isStarFree).

The genuinely autosegmental case — links coupling the two tiers — is deeper: a forbidden subgraph can match with an unlinked run-end arbitrarily far from its linked core, so a bounded sliding-window scanner over the realization is unsound; a two-tape synchronising aperiodic recognizer is needed, and is left to future work.

The relation-level L = ASL^{gT} equivalences ([Jar19]) remain future work.

theorem Autosegmental.isStarFree_occur_of_links_empty {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (F : Graph α β) (hF : F.links = ∅) : Language.IsStarFree {w : List S | F.SubgraphEmbeds (realize g₀ w).toGraph}

For a single link-free forbidden subgraph F, the strings whose realization contains F form a star-free language: the intersection of two per-tier factor-occurrence constraints, each the inverse image (comap) of a star-free contains-factor language along a tier projection.

theorem Autosegmental.ASL.isStarFree_of_links_empty {S : Type u_1} {α : Type u_2} {β : Type u_3} (g₀ : S → AR α β) (B : List (Graph α β)) (hB : ∀ F ∈ B, F.links = ∅) : (ASL g₀ B).IsStarFree

Link-free autosegmental SL sets are star-free. When every forbidden subgraph in B has no association lines, ASL g₀ B is star-free — over any symbol alphabet, with no [Finite S] hypothesis, since each tier's contains-factor recognizer is a fixed finite aperiodic monoid. A link-free forbidden grammar is exactly a Boolean combination of per-tier factor constraints; the genuinely autosegmental case (links coupling the tiers) is the deeper part of [Jar19]'s placement and is not covered here.

inductive Jardine2019.ToneSym : Type

The tone alphabet ([Jar19] §2): high, low, falling.

• H : ToneSym
• L : ToneSym
• F : ToneSym

@[implicit_reducible]

instance Jardine2019.instDecidableEqToneSym : DecidableEq ToneSym

Equations

• Jardine2019.instDecidableEqToneSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jardine2019.instReprToneSym.repr : ToneSym → ℕ → Std.Format

Equations

• Jardine2019.instReprToneSym.repr Jardine2019.ToneSym.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2019.ToneSym.H")).group prec✝
• Jardine2019.instReprToneSym.repr Jardine2019.ToneSym.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2019.ToneSym.L")).group prec✝
• Jardine2019.instReprToneSym.repr Jardine2019.ToneSym.F prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2019.ToneSym.F")).group prec✝

@[implicit_reducible]

instance Jardine2019.instReprToneSym : Repr ToneSym

Equations

• Jardine2019.instReprToneSym = { reprPrec := Jardine2019.instReprToneSym.repr }

inductive Jardine2019.Mora : Type

The tone-bearing unit (a mora).

• μ : Mora

@[implicit_reducible]

instance Jardine2019.instDecidableEqMora : DecidableEq Mora

Equations

• Jardine2019.instDecidableEqMora x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jardine2019.instReprMora.repr : Mora → ℕ → Std.Format

Equations

• Jardine2019.instReprMora.repr Jardine2019.Mora.μ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2019.Mora.μ")).group prec✝

@[implicit_reducible]

instance Jardine2019.instReprMora : Repr Mora

Equations

• Jardine2019.instReprMora = { reprPrec := Jardine2019.instReprMora.repr }

def Jardine2019.gT : ToneSym → Autosegmental.AR ToneSym Mora

The tone realization g_T ([Jar19] (23)): H/L are a single tone on one mora; the falling tone F is an H-L contour on one mora (multiple association).

Equations

• Jardine2019.gT Jardine2019.ToneSym.H = Autosegmental.AR.single Jardine2019.ToneSym.H Jardine2019.Mora.μ
• Jardine2019.gT Jardine2019.ToneSym.L = Autosegmental.AR.single Jardine2019.ToneSym.L Jardine2019.Mora.μ
• Jardine2019.gT Jardine2019.ToneSym.F = Autosegmental.AR.contour [Jardine2019.ToneSym.H, Jardine2019.ToneSym.L] Jardine2019.Mora.μ

def Jardine2019.hlh : Autosegmental.Graph ToneSym Mora

The forbidden subgraph *HLH ([Jar19] (3)): an H-L-H tone sequence, three tones each on their own mora.

Equations

• One or more equations did not get rendered due to their size.

theorem Jardine2019.hlh_excluded : [ToneSym.H, ToneSym.L, ToneSym.H] ∉ Autosegmental.ASL gT [hlh]

HLH is excluded: its realization contains the *HLH subgraph.

theorem Jardine2019.hl_included : [ToneSym.H, ToneSym.L] ∈ Autosegmental.ASL gT [hlh]

HL is admitted (no H-L-H).

theorem Jardine2019.lhl_included : [ToneSym.L, ToneSym.H, ToneSym.L] ∈ Autosegmental.ASL gT [hlh]

LHL is admitted (no H-L-H).

theorem Jardine2019.hhlh_excluded : [ToneSym.H, ToneSym.H, ToneSym.L, ToneSym.H] ∉ Autosegmental.ASL gT [hlh]

And the constraint reaches inside longer strings: HHLH is excluded (the medial H-L-H realizes the forbidden subgraph).

The OCP-merging realization: non-local tone plateauing

[Jar19]'s g_T is OCP-merging — an H-plateau Hⁿ is a single H node, not n of them. realizeMerged (Collapse.lean) supplies that merge. Against it we ban the tonal-tier melody *HLH — an H-L-H sequence read off the tone tier alone (hlhTier: upper [H, L, H], no morae pinned), so the constraint is on tonal adjacency after merging, not on per-mora docking. This is where merging buys non-local power: H⁺ L⁺ H⁺ is excluded for any plateau widths, because the plateaus collapse first.

def Jardine2019.hlhTier : Autosegmental.Graph ToneSym Mora

The forbidden tonal-tier melody *HLH: an H-L-H sequence of adjacent tonal nodes, with the mora tier left unconstrained (empty lower tier, no links). Read off the tone tier after OCP merging, this is the genuine non-local plateauing ban — contrast hlh, whose diagonal per-mora docking makes it sensitive to plateau width.

Equations

• Jardine2019.hlhTier = (Autosegmental.AR.float Jardine2019.ToneSym.H * Autosegmental.AR.float Jardine2019.ToneSym.L * Autosegmental.AR.float Jardine2019.ToneSym.H).toGraph

def Jardine2019.ASL' (g₀ : ToneSym → Autosegmental.AR ToneSym Mora) (B : List (Autosegmental.Graph ToneSym Mora)) : Language ToneSym

The merging variant of ASL: the same forbidden-subgraph preimage, taken along the OCP-merging realization realizeMerged instead of the bridge-only realize.

Equations

• Jardine2019.ASL' g₀ B = Autosegmental.realizeMerged g₀ ⁻¹' {A : Autosegmental.AR Jardine2019.ToneSym Jardine2019.Mora | Autosegmental.isFreeOf B A}

@[implicit_reducible]

instance Jardine2019.instDecidableMemListToneSymLanguageASL' (g₀ : ToneSym → Autosegmental.AR ToneSym Mora) (B : List (Autosegmental.Graph ToneSym Mora)) (w : List ToneSym) : Decidable (w ∈ ASL' g₀ B)

Equations

• Jardine2019.instDecidableMemListToneSymLanguageASL' g₀ B w = Jardine2019.instDecidableMemListToneSymLanguageASL'._aux_1 g₀ B w

theorem Jardine2019.lhhlh_merged_excluded : [ToneSym.L, ToneSym.H, ToneSym.H, ToneSym.L, ToneSym.H] ∉ ASL' gT [hlhTier]

LHHLH is excluded under merging: the HH-plateau merges, so the tone tier reads L-H-L-H and the medial H-L-H melody appears ([Jar19]'s *HLH).

theorem Jardine2019.hhh_merged_included : [ToneSym.H, ToneSym.H, ToneSym.H] ∈ ASL' gT [hlhTier]

A single H-plateau is admitted under merging: HHH collapses to one H node, so the tone tier is just H — no H-L-H melody to forbid.

theorem Jardine2019.hlhTier_merged_excludes_plateau : [ToneSym.H, ToneSym.H, ToneSym.L, ToneSym.L, ToneSym.H, ToneSym.H] ∉ ASL' gT [hlhTier]

The non-local power merging buys. An unbounded plateau HH-LL-HH is excluded under realizeMerged: every run collapses, so the tone tier reads H-L-H and the melody appears — no matter the plateau widths.

theorem Jardine2019.hlhTier_unmerged_admits_plateau : [ToneSym.H, ToneSym.H, ToneSym.L, ToneSym.L, ToneSym.H, ToneSym.H] ∈ Autosegmental.ASL gT [hlhTier]

The same string is admitted under the non-merging realize: with the plateaus kept apart, the tone tier reads H-H-L-L-H-H, which has no three adjacent H-L-H nodes. The contrast with hlhTier_merged_excludes_plateau is exactly the non-local expressivity OCP merging adds — the local hlh_excluded constraint cannot see it.

theorem Jardine2019.hlhTier_isStarFree : (Autosegmental.ASL gT [hlhTier]).IsStarFree

The *HLH tonal-tier melody set is star-free. hlhTier carries no association lines, so ASL gT [hlhTier] falls in the link-free fragment (ASL.isStarFree_of_links_empty): a concrete instance of [Jar19]'s ASL ⊊ SF placement that the bridge-only realization already settles.