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 defines the class on the graph foundation, instantiates it 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.AR.realize uses the project's bridge-only concat (the coproduct), so an H-plateau Hⁿ stays n separate H nodes. Banning *HLH over AR.realize then catches only a local H-L-H (three adjacent tonal nodes) — hlh_excluded.
• Autosegmental.AR.realizeMerged (OCP.lean) is [Jar19]'s OCP-merging g_T: g_T(Hⁿ) is a single H node multiply associated. Banning *HLH over AR.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 (AR.ASL.isStarFree_of_link_free) — 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.

The star-free placement in coordinates

def Autosegmental.AR.ASL {S : Type u_1} {ι : Type u_2} {τ : ι → Type u_3} (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (B : List { F : AR Sigma.fst // Finite F.obj.V }) : Language S

The Autosegmental Strictly Local stringset ASL^g: strings whose realization avoids every forbidden factor. It is the same construction as the tier-based strictly local sets — a preimage of a local condition along a free-monoid homomorphism (TSL = tierProject ⁻¹' SL); the association structure AR.realize keeps is why [Jar19] finds the two classes incomparable.

Equations

• Autosegmental.AR.ASL g₀ B = {w : List S | Autosegmental.AR.Free (Autosegmental.AR.realize g₀ w) B}

@[simp]

theorem Autosegmental.AR.mem_ASL {S : Type u_1} {ι : Type u_2} {τ : ι → Type u_3} {g₀ : S → AR Sigma.fst} [∀ (s : S), Finite (g₀ s).obj.V] {B : List { F : AR Sigma.fst // Finite F.obj.V }} {w : List S} : w ∈ ASL g₀ B ↔ Free (realize g₀ w) B

theorem Autosegmental.AR.isStarFree_occur_of_link_free {S : Type u_1} {ι : Type u_2} [Finite ι] {τ : ι → Type u_3} (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (F : AR Sigma.fst) [Finite F.obj.V] (hF : ∀ (i j : ι) (p q : ℕ), ¬F.link i j p q) : Language.IsStarFree {w : List S | F.FactorEmbeds (realize g₀ w)}

For a single link-free forbidden factor, the strings whose realization contains it form a star-free language: the finite intersection of per-tier factor constraints, each the inverse image of a star-free contains-factor language along a tier projection.

theorem Autosegmental.AR.ASL.isStarFree_of_link_free {S : Type u_1} {ι : Type u_2} [Finite ι] {τ : ι → Type u_3} (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (B : List { F : AR Sigma.fst // Finite F.obj.V }) (hB : ∀ F ∈ B, ∀ (i j : ι) (p q : ℕ), ¬(↑F).link i j p q) : (ASL g₀ B).IsStarFree

Link-free autosegmental SL sets are star-free, on the graph foundation: when no forbidden factor carries association lines, AR.ASL is a Boolean combination of per-tier factor constraints.

inductive Jardine2019.ToneSym : Type

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

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

@[instance_reducible]

instance Jardine2019.instDecidableEqToneSym : DecidableEq ToneSym

Equations

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

@[instance_reducible]

instance Jardine2019.instReprToneSym : Repr ToneSym

Equations

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

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✝

inductive Jardine2019.Mora : Type

The tone-bearing unit (a mora).

• μ : Mora

@[instance_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✝

@[instance_reducible]

instance Jardine2019.instReprMora : Repr Mora

Equations

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

@[reducible, inline]

abbrev Jardine2019.TRep : Type (u_1 + 1)

Two-tier tone representations (melody over true, morae over false).

Equations

• Jardine2019.TRep = Autosegmental.AR Sigma.fst

def Jardine2019.mkL (links : List (ℕ × ℕ)) (i j : Bool) (p q : ℕ) : Prop

Link presentations from finite pair lists.

Equations

• Jardine2019.mkL links i j p q = (i = true ∧ j = false ∧ (p, q) ∈ links)

@[instance_reducible]

instance Jardine2019.instDecidableMkL (links : List (ℕ × ℕ)) (i j : Bool) (p q : ℕ) : Decidable (mkL links i j p q)

Equations

• Jardine2019.instDecidableMkL links i j p q = Jardine2019.instDecidableMkL._aux_1 links i j p q

@[reducible, inline]

abbrev Jardine2019.mk (tones : List ToneSym) (moras : List Mora) (links : List (ℕ × ℕ)) : TRep

Build a representation from a tone melody, morae, and links.

Equations

• Jardine2019.mk tones moras links = Autosegmental.AR.ofData (fun (b : Bool) => match b with | true => tones | false => moras) (Jardine2019.mkL links)

theorem Jardine2019.mk_embeds_iff {tF tX : List ToneSym} {bF bX : List Mora} {lF lX : List (ℕ × ℕ)} : Autosegmental.AR.FactorEmbeds (mk tF bF lF) (mk tX bX lX) ↔ Autosegmental.dataEmbeds (fun (b : Bool) => match b with | true => tF | false => bF) (fun (b : Bool) => match b with | true => tX | false => bX) (mkL lF) (mkL lX)

@[reducible, inline]

abbrev Jardine2019.hlh : TRep

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

Equations

• Jardine2019.hlh = Jardine2019.mk [Jardine2019.ToneSym.H, Jardine2019.ToneSym.L, Jardine2019.ToneSym.H] [Jardine2019.Mora.μ, Jardine2019.Mora.μ, Jardine2019.Mora.μ] [(0, 0), (1, 1), (2, 2)]

The bridge-only realization: local *HLH

The realization of a tone string under the bridge-only tensor is, in flattened presentation, the diagonal literal — one tone per mora (gT (23), with F an H-L contour). The *HLH verdicts compute through the data-level checker.

theorem Jardine2019.hlh_excluded : Autosegmental.AR.FactorEmbeds hlh (mk [ToneSym.H, ToneSym.L, ToneSym.H] [Mora.μ, Mora.μ, Mora.μ] [(0, 0), (1, 1), (2, 2)])

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

theorem Jardine2019.hl_included : ¬Autosegmental.AR.FactorEmbeds hlh (mk [ToneSym.H, ToneSym.L] [Mora.μ, Mora.μ] [(0, 0), (1, 1)])

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

theorem Jardine2019.lhl_included : ¬Autosegmental.AR.FactorEmbeds hlh (mk [ToneSym.L, ToneSym.H, ToneSym.L] [Mora.μ, Mora.μ, Mora.μ] [(0, 0), (1, 1), (2, 2)])

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

theorem Jardine2019.hhlh_excluded : Autosegmental.AR.FactorEmbeds hlh (mk [ToneSym.H, ToneSym.H, ToneSym.L, ToneSym.H] [Mora.μ, Mora.μ, Mora.μ, Mora.μ] [(0, 0), (1, 1), (2, 2), (3, 3)])

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ⁿ fuses to a single H node (AR.collapse). Against the merged forms we ban the tonal-tier melody *HLH — adjacent tonal nodes, morae unconstrained — which is where merging buys non-local power: H⁺ L⁺ H⁺ is excluded for any plateau widths, because the plateaus collapse first.

@[reducible, inline]

abbrev Jardine2019.hlhTier : TRep

The forbidden tonal-tier melody *HLH: no morae pinned, no links.

Equations

• Jardine2019.hlhTier = Jardine2019.mk [Jardine2019.ToneSym.H, Jardine2019.ToneSym.L, Jardine2019.ToneSym.H] [] []

theorem Jardine2019.lhhlh_merged_excluded : Autosegmental.AR.FactorEmbeds hlhTier (mk [ToneSym.L, ToneSym.H, ToneSym.L, ToneSym.H] [Mora.μ, Mora.μ, Mora.μ, Mora.μ, Mora.μ] [(0, 0), (1, 1), (1, 2), (2, 3), (3, 4)])

LHHLH is excluded under merging: the HH-plateau fuses, the tone tier reads L-H-L-H, and the medial H-L-H melody appears.

theorem Jardine2019.hhh_merged_included : ¬Autosegmental.AR.FactorEmbeds hlhTier (mk [ToneSym.H] [Mora.μ, Mora.μ, Mora.μ] [(0, 0), (0, 1), (0, 2)])

A single H-plateau is admitted under merging: HHH fuses to one H.

theorem Jardine2019.hlhTier_merged_excludes_plateau : Autosegmental.AR.FactorEmbeds hlhTier (mk [ToneSym.H, ToneSym.L, ToneSym.H] [Mora.μ, Mora.μ, Mora.μ, Mora.μ, Mora.μ, Mora.μ] [(0, 0), (0, 1), (1, 2), (1, 3), (2, 4), (2, 5)])

The non-local power merging buys: the unbounded plateau HH-LL-HH fuses to tone tier H-L-H, so the melody appears — at any widths.

theorem Jardine2019.hlhTier_unmerged_admits_plateau : ¬Autosegmental.AR.FactorEmbeds hlhTier (mk [ToneSym.H, ToneSym.H, ToneSym.L, ToneSym.L, ToneSym.H, ToneSym.H] [Mora.μ, Mora.μ, Mora.μ, Mora.μ, Mora.μ, Mora.μ] [(0, 0), (1, 1), (2, 2), (3, 3), (4, 4), (5, 5)])

The same string unmerged is admitted: the plateaus stay apart, the tone tier reads H-H-L-L-H-H, and no three adjacent nodes spell H-L-H. The contrast with hlhTier_merged_excludes_plateau is exactly the non-local expressivity OCP merging adds.

theorem Jardine2019.hlhTier_link_free (i j : Bool) (p q : ℕ) : ¬Autosegmental.AR.link hlhTier i j p q

The *HLH tonal-tier melody set is star-free: hlhTier carries no links, so any grammar built from it falls in the link-free fragment (AR.ASL.isStarFree_of_link_free) — a concrete instance of [Jar19]'s ASL ⊊ SF placement.