Jardine (2019): The expressivity of autosegmental grammars

The map gT sends each tone symbol to a primitive autosegmental graph, H and L a tone over a mora and F the falling contour H L over one, and extends to strings by merging concatenation, which fuses a run of Hs into one H over its morae. A banned-subgraph grammar over this realization describes the strings whose graph avoids it, an instance of the autosegmental strictly local class (Language.bannedSubgraph). Every graph in gT(Σ*) obeys the OCP and the No-Crossing Constraint. Membership decides on strings: the spreading grammar admits exactly its example strings, and the grammar of unbounded tonal plateauing admits L_UTP and excludes the plateau HHLLHH at any width, which the unmerged realization leaves free.

Theorem 3 compares the class with the string classes. gT(HL) is a subgraph of gT(HF), so no grammar excludes HL without excluding HF. And L_UTP is neither strictly local nor tier-based strictly local at any width: with x = L^(k-1), H L x and x H are in it and H L x H is not, and every symbol is visible, so a tier-based grammar would be strictly local.

Main results

• isCleanAt_and_noCrossing_mergeRealize: graphs in gT(Σ*) obey the OCP and the NCC.
• rows_agree: the grammars decide the paper's example strings.
• not_mem_ASL_HF_of_not_mem_ASL_HL: a grammar excluding HL excludes HF.
• not_isStrictlyLocal_ASL_utp, not_isTierStrictlyLocal_ASL_utp: L_UTP is neither strictly local nor tier-based strictly local.

Implementation notes

• The paper evaluates a grammar on g(⋊w⋉), with border primitives for ⋊ and ⋉, which this file omits. The grammars here mention no border.
• Banned subgraphs need not be connected (Autosegmental/Factors.lean), so the class here contains the paper's.
• gT extends to strings by Definition 2, the left fold of merging concatenation (AR.mergeRealize). Its primitives are OCP-clean, so it agrees with collapsing the bridged concatenation (AR.nonempty_fullIso_realizeMerged), whose presentation merged the proofs compute with.
• The unmerged AR.realize is kept for the contrast merging makes.

TODO

Add the border primitives, and with them Theorem 3's other half, that the strictly 2-local HL-free language is not in the class. Theorem 2, that the class is properly contained in the star-free languages, is formalized only for the link-free unmerged fragment (isStarFree_free_realize_hlh); Theorem 4, incomparability with the strictly piecewise languages, needs connected factors.

References

• [Jar19]

inductive Jardine2019.Sym : Type

A symbol of the string alphabet Σ_T (§5.2.2) is a high, low or falling-toned mora.

• H : Sym
• L : Sym
• F : Sym

@[instance_reducible]

instance Jardine2019.instDecidableEqSym : DecidableEq Sym

Equations

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

@[instance_reducible]

instance Jardine2019.instReprSym : Repr Sym

Equations

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

def Jardine2019.instReprSym.repr : Sym → ℕ → Std.Format

Equations

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

def Jardine2019.Sym.melody : Sym → List Tone.TRN

A symbol's primitive carries its melody, F the falling contour H L.

Equations

• Jardine2019.Sym.H.melody = [Tone.TRN.H]
• Jardine2019.Sym.L.melody = [Tone.TRN.L]
• Jardine2019.Sym.F.melody = [Tone.TRN.H, Tone.TRN.L]

@[reducible, inline]

abbrev Jardine2019.μ : Tone.TBUKind

The mora, the paper's tone-bearing unit.

Equations

• Jardine2019.μ = Tone.TBUKind.mora

def Jardine2019.gT (s : Sym) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

gT (23) maps a symbol to the primitive (Definition 1) of its melody over one mora.

Equations

• Jardine2019.gT s = Autosegmental.AR.primitive s.melody Jardine2019.μ

instance Jardine2019.instFiniteVSigmaBoolTwoTierTRNTBUKindObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesGT (s : Sym) : Finite (gT s).obj.V

@[reducible, inline]

abbrev Jardine2019.merged (w : List Sym) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

The merged realization of a string, read as a representation of words.

Equations

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

@[reducible, inline]

abbrev Jardine2019.unmerged (w : List Sym) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

The unmerged realization of a string, read as a representation of words.

Equations

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

theorem Jardine2019.isCleanAt_gT (s : Sym) : Autosegmental.AR.IsCleanAt (gT s) true

The primitives of gT are OCP-clean.

theorem Jardine2019.tierWord_mergeRealize_gT (w : List Sym) (i : Bool) : Autosegmental.AR.tierWord i = Autosegmental.AR.tierWord i

theorem Jardine2019.link_mergeRealize_gT (w : List Sym) (i j : Bool) (p q : ℕ) : Autosegmental.AR.link (Autosegmental.AR.mergeRealize true gT w) i j p q ↔ Autosegmental.AR.link (merged w) i j p q

def Jardine2019.ASL (B : List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }) : Language Sym

L(B^{gT}) (§5.3) is the set of strings whose merged realization avoids the grammar.

Equations

• Jardine2019.ASL B = Language.bannedSubgraph (Autosegmental.AR.mergeRealize true Jardine2019.gT) B

theorem Jardine2019.mem_ASL_iff {B : List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }} {w : List Sym} : w ∈ ASL B ↔ Autosegmental.AR.Free (merged w) B

theorem Jardine2019.free_realize_iff (B : List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }) (w : List Sym) : Autosegmental.AR.Free (Autosegmental.AR.realize gT w) B ↔ Autosegmental.AR.Free (unmerged w) B

theorem Jardine2019.isCleanAt_and_noCrossing_mergeRealize (w : List Sym) : Autosegmental.AR.IsCleanAt (Autosegmental.AR.mergeRealize true gT w) true ∧ Autosegmental.NoCrossing (Autosegmental.AR.mergeRealize true gT w).obj.edges (Autosegmental.AR.mergeRealize true gT w).obj.arcs

Every graph in gT(Σ*) obeys the OCP and the NCC, as they are preserved from the primitives (§5.2.2).

The grammars of (26) and (33)

@[reducible, inline]

abbrev Jardine2019.spread : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

The factor of (26) is a tone over two morae.

Equations

• Jardine2019.spread = Autosegmental.AR.ofWords [Tone.TRN.H] [Jardine2019.μ, Jardine2019.μ] fun (x x_1 : ℕ) => True

@[reducible, inline]

abbrev Jardine2019.hlh : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

(3), the melody H L H.

Equations

• Jardine2019.hlh = Autosegmental.AR.ofWords [Tone.TRN.H, Tone.TRN.L, Tone.TRN.H] [] fun (x x_1 : ℕ) => False

@[reducible, inline]

abbrev Jardine2019.fall : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

The falling contour is H L over one mora.

Equations

• Jardine2019.fall = Autosegmental.AR.primitive [Tone.TRN.H, Tone.TRN.L] Jardine2019.μ

def Jardine2019.spreadGrammar : List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }

The grammar of (26) bans a tone over two morae.

Equations

• Jardine2019.spreadGrammar = [⟨Jardine2019.spread, Jardine2019.spreadGrammar._proof_1⟩]

def Jardine2019.utpGrammar : List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }

The grammar B_UTP (33) bans the melody H L H and the contour.

Equations

• Jardine2019.utpGrammar = [⟨Jardine2019.hlh, Jardine2019.utpGrammar._proof_1⟩, ⟨Jardine2019.fall, Jardine2019.utpGrammar._proof_2⟩]

theorem Jardine2019.mem_ASL_spreadGrammar_iff (w : List Sym) : w ∈ ASL spreadGrammar ↔ ¬Autosegmental.AR.FactorEmbeds spread (merged w)

theorem Jardine2019.mem_ASL_utpGrammar_iff (w : List Sym) : w ∈ ASL utpGrammar ↔ ¬Autosegmental.AR.FactorEmbeds hlh (merged w) ∧ ¬Autosegmental.AR.FactorEmbeds fall (merged w)

@[instance_reducible]

instance Jardine2019.instDecidableMemListSymLanguageASLSpreadGrammar (w : List Sym) : Decidable (w ∈ ASL spreadGrammar)

Equations

• Jardine2019.instDecidableMemListSymLanguageASLSpreadGrammar w = decidable_of_iff (¬Autosegmental.AR.FactorEmbeds Jardine2019.spread (Jardine2019.merged w)) ⋯

@[instance_reducible]

instance Jardine2019.instDecidableMemListSymLanguageASLUtpGrammar (w : List Sym) : Decidable (w ∈ ASL utpGrammar)

Equations

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

The data of (27) and (32)

inductive Jardine2019.Grammar : Type

The two grammars of the paper's examples.

• spread : Grammar
• utp : Grammar

@[instance_reducible]

instance Jardine2019.instDecidableEqGrammar : DecidableEq Grammar

Equations

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

structure Jardine2019.Row : Type

A row records a string, the grammar it is tested against, and whether it is in the set.

• string : List Sym
• grammar : Grammar
• member : Bool

def Jardine2019.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Jardine2019.instDecidableEqRow : DecidableEq Row

Equations

• Jardine2019.instDecidableEqRow = Jardine2019.instDecidableEqRow.decEq

def Jardine2019.Sym.ofChar : Char → Sym

A symbol from its spelling.

Equations

• Jardine2019.Sym.ofChar 'H' = Jardine2019.Sym.H
• Jardine2019.Sym.ofChar 'F' = Jardine2019.Sym.F
• Jardine2019.Sym.ofChar x✝ = Jardine2019.Sym.L

def Jardine2019.Row.ofDatum (e : Datum) : Option Row

A row from the paper's features.

Equations

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

def Jardine2019.rows : List Row

The strings of (27) with the HH and HF the grammar (26) excludes, and those of (32).

Equations

• Jardine2019.rows = List.filterMap Jardine2019.Row.ofDatum Jardine2019.Examples.all

def Jardine2019.Grammar.set : Grammar → Language Sym

The set a row's grammar describes.

Equations

• Jardine2019.Grammar.spread.set = Jardine2019.ASL Jardine2019.spreadGrammar
• Jardine2019.Grammar.utp.set = Jardine2019.ASL Jardine2019.utpGrammar

@[instance_reducible]

instance Jardine2019.instDecidableMemListSymLanguageSet (g : Grammar) (w : List Sym) : Decidable (w ∈ g.set)

Equations

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

theorem Jardine2019.rows_agree (r : Row) : r ∈ rows → (r.string ∈ r.grammar.set ↔ r.member = true)

The grammar (26) admits the strings of (27) and excludes HH and HF, whose fused H spans two morae, and B_UTP admits the strings of L_UTP, (32).

theorem Jardine2019.HLH_not_mem_ASL_utp : [Sym.H, Sym.L, Sym.H] ∉ ASL utpGrammar

HLH is excluded, its melody being H L H.

theorem Jardine2019.LHHLH_not_mem_ASL_utp : [Sym.L, Sym.H, Sym.H, Sym.L, Sym.H] ∉ ASL utpGrammar

LHHLH is excluded, since the HH plateau fuses and the melody reads L H L H.

theorem Jardine2019.HHLLHH_not_mem_ASL_utp : [Sym.H, Sym.H, Sym.L, Sym.L, Sym.H, Sym.H] ∉ ASL utpGrammar

The unbounded plateau HHLLHH is excluded, since both plateaus fuse and the melody reads H L H at any widths.

theorem Jardine2019.HHLLHH_free_realize : Autosegmental.AR.Free (Autosegmental.AR.realize gT [Sym.H, Sym.H, Sym.L, Sym.L, Sym.H, Sym.H]) utpGrammar

The same string is free of B_UTP under the unmerged realization, whose melody H H L L H H has no three adjacent nodes spelling H L H.

Theorem 3: contours contain their pure counterparts

theorem Jardine2019.mergeRealize_HL_embeds_HF : Autosegmental.AR.FactorEmbeds (Autosegmental.AR.mergeRealize true gT [Sym.H, Sym.L]) (Autosegmental.AR.mergeRealize true gT [Sym.H, Sym.F])

gT(HL) is a subgraph of gT(HF), since the falling contour on the second mora contains the L on it.

theorem Jardine2019.not_mem_ASL_HF_of_not_mem_ASL_HL (B : List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }) (h : [Sym.H, Sym.L] ∉ ASL B) : [Sym.H, Sym.F] ∉ ASL B

No forbidden-subgraph grammar excludes HL without excluding HF (Theorem 3), since a subgraph of gT(HL) is a subgraph of gT(HF).

The link-free fragment of the unmerged class is star-free

theorem Jardine2019.isStarFree_free_realize_hlh : (Language.bannedSubgraph (Autosegmental.AR.realize gT) [⟨hlh, ⋯⟩]).IsStarFree

The melody constraint of B_UTP is link-free, so under the unmerged realization it specifies a star-free set.

Theorem 3: L_UTP is neither strictly local nor tier-based strictly local

In a string without F every mora carries its own symbol's single tone, so no contour occurs and membership in L_UTP depends only on the merged melody. With x = L^{k−1}, H L·x and x·H are in L_UTP and H L·x·H is not, which breaks suffix substitution at every width; and every symbol is visible, so a tier-based grammar would have to be strictly local.

theorem Jardine2019.not_fall_factorEmbeds_merged {w : List Sym} (hw : ∀ s ∈ w, s ≠ Sym.F) : ¬Autosegmental.AR.FactorEmbeds fall (merged w)

An F-free string has no contour.

theorem Jardine2019.hlh_factorEmbeds_merged_iff (w : List Sym) : Autosegmental.AR.FactorEmbeds hlh (merged w) ↔ [Tone.TRN.H, Tone.TRN.L, Tone.TRN.H] <:+: OCP.collapse (List.map Sym.melody w).flatten

The melody H L H occurs iff it is an infix of the merged melody.

theorem Jardine2019.mem_ASL_utp_HL_replicate (m : ℕ) : [Sym.H, Sym.L] ++ List.replicate m Sym.L ∈ ASL utpGrammar

theorem Jardine2019.mem_ASL_utp_replicate_H (m : ℕ) : List.replicate m Sym.L ++ [Sym.H] ∈ ASL utpGrammar

theorem Jardine2019.not_mem_ASL_utp_HL_replicate_H (m : ℕ) : [Sym.H, Sym.L] ++ List.replicate m Sym.L ++ [Sym.H] ∉ ASL utpGrammar

theorem Jardine2019.not_isStrictlyLocal_ASL_utp (k : ℕ) : ¬(ASL utpGrammar).IsStrictlyLocal k

L_UTP is not strictly local at any width (Theorem 3).

theorem Jardine2019.ASL_utp_visible (a : Sym) : ∃ (u : List Sym) (v : List Sym), ¬(u ++ a :: v ∈ ASL utpGrammar ↔ u ++ v ∈ ASL utpGrammar)

Every symbol is visible in L_UTP, deleting it from some string changing membership.

theorem Jardine2019.not_isTierStrictlyLocal_ASL_utp (k : ℕ) : ¬Language.IsTierStrictlyLocal k (ASL utpGrammar)

L_UTP is not tier-based strictly local at any width (Theorem 3).