Jardine and Heinz (2015): A Concatenation Operation to Derive Autosegmental Graphs

Jardine and Heinz derive autosegmental graphs by concatenating graph primitives. Concatenation bridges the two graphs tier by tier and merges the last melody node of the first with the first melody node of the second when the two bear the same label (AR.mergeConcat); a string denotes the left fold of its symbols' primitives (AR.mergeRealize). The operation has the empty graph as unit and is associative, and it preserves the No-Crossing Constraint and, over OCP-clean primitives, the OCP; these are the theorems of Autosegmental/MergeConcat.lean.

Because only the seam merges, a primitive that violates the OCP keeps its violation. The authors use this for Kishambaa, where a high-toned noun with a downstepped second high contrasts with one whose high spreads over both morae: a primitive H H with only its second H linked derives the downstep, and concatenating then collapsing every run, the method they set aside, would derive the spread instead.

Main statements

• mergeConcat_G₁_G₂: Example 3, the merge of b with b at the seam (Figure 4).
• mergeRealize_γ₁_γ₂, mergeRealize_γ₁_γ₁: the Kishambaa graphs of Figure 12.
• realizeMerged_γ₁_γ₂, not_nonempty_fullIso_realizeMerged: collapsing after concatenation derives the spread graph for the downstep form, so it does not agree with merging concatenation once a primitive violates the OCP.

References

• [JH15]

Example 1: concatenation merges the seam

inductive JardineHeinz2015.Mel : Type

The melody symbols a and b of Example 1.

• a : Mel
• b : Mel

@[instance_reducible]

instance JardineHeinz2015.instDecidableEqMel : DecidableEq Mel

Equations

• JardineHeinz2015.instDecidableEqMel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev JardineHeinz2015.Γ : Bool → Type

Example 1's labels: melody symbols over true, and the one timing symbol c over false.

Equations

• JardineHeinz2015.Γ = Autosegmental.TwoTier JardineHeinz2015.Mel Unit

@[reducible, inline]

abbrev JardineHeinz2015.G₁ : Autosegmental.TieredAR Bool Γ

G₁ of Figure 2: the melody a b, both associated to one timing node.

Equations

• JardineHeinz2015.G₁ = Autosegmental.AR.primitive [JardineHeinz2015.Mel.a, JardineHeinz2015.Mel.b] ()

@[reducible, inline]

abbrev JardineHeinz2015.G₂ : Autosegmental.TieredAR Bool Γ

G₂ of Figure 2: b over a timing node.

Equations

• JardineHeinz2015.G₂ = Autosegmental.AR.primitive [JardineHeinz2015.Mel.b] ()

@[reducible, inline]

abbrev JardineHeinz2015.fig4 : Autosegmental.TieredAR Bool Γ

The graph of Figure 4: a then the merged b, over two timing nodes, with the merged b associated to both.

Equations

• JardineHeinz2015.fig4 = Autosegmental.AR.ofWords [JardineHeinz2015.Mel.a, JardineHeinz2015.Mel.b] [(), ()] fun (p q : ℕ) => q = 0 ∨ p = 1

theorem JardineHeinz2015.mergeConcat_G₁_G₂ : Nonempty ((Autosegmental.AR.mergeConcat true G₁ G₂).obj.Iso fig4.obj)

Concatenating G₁ and G₂ merges their b nodes (Example 3, Figure 4).

Kishambaa: an OCP-violating primitive

@[reducible, inline]

abbrev JardineHeinz2015.μ : Tone.TBUKind

The mora, the tone-bearing unit.

Equations

• JardineHeinz2015.μ = Tone.TBUKind.mora

inductive JardineHeinz2015.Sym : Type

The symbols of the Kishambaa alphabet (Figure 13).

• γ₁ : Sym
• γ₂ : Sym

@[instance_reducible]

instance JardineHeinz2015.instDecidableEqSym : DecidableEq Sym

Equations

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

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

γ₁ is a high-toned mora; γ₂ is a mora carrying a high preceded by a floating high.

Equations

• JardineHeinz2015.Sym.γ₁.melody = [Tone.TRN.H]
• JardineHeinz2015.Sym.γ₂.melody = [Tone.TRN.H, Tone.TRN.H]

def JardineHeinz2015.Sym.lines : Sym → ℕ → ℕ → Prop

The lines of a symbol's primitive: γ₁'s high is linked, and only the second high of γ₂.

Equations

• JardineHeinz2015.Sym.γ₁.lines = fun (x x_1 : ℕ) => True
• JardineHeinz2015.Sym.γ₂.lines = fun (p x : ℕ) => p = 1

@[instance_reducible]

instance JardineHeinz2015.instDecidableRelNatLines (s : Sym) : DecidableRel s.lines

Equations

• JardineHeinz2015.instDecidableRelNatLines JardineHeinz2015.Sym.γ₁ = fun (x x_1 : ℕ) => { decide := true, reflects_decide := ⋯ }
• JardineHeinz2015.instDecidableRelNatLines JardineHeinz2015.Sym.γ₂ = fun (p x : ℕ) => { decide := p.beq 1, reflects_decide := ⋯ }

def JardineHeinz2015.g (s : Sym) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

The primitives of Figure 13.

Equations

• JardineHeinz2015.g s = Autosegmental.AR.ofWords s.melody [JardineHeinz2015.μ] s.lines

instance JardineHeinz2015.instFiniteVSigmaBoolTwoTierTRNTBUKindObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesG (s : Sym) : Finite (g s).obj.V

theorem JardineHeinz2015.not_isCleanAt_g_γ₂ : ¬Autosegmental.AR.IsCleanAt (g Sym.γ₂) true

g(γ₂) violates the OCP.

@[reducible, inline]

abbrev JardineHeinz2015.snake : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

Figure 12a, 'snake': one high spread over two morae.

Equations

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

@[reducible, inline]

abbrev JardineHeinz2015.sheep : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

Figure 12b, 'sheep': a high and a downstepped high, one per mora.

Equations

• JardineHeinz2015.sheep = Autosegmental.AR.ofWords [Tone.TRN.H, Tone.TRN.H] [JardineHeinz2015.μ, JardineHeinz2015.μ] fun (p q : ℕ) => p = q

theorem JardineHeinz2015.mergeRealize_γ₁_γ₁ : Nonempty ((Autosegmental.AR.mergeRealize true g [Sym.γ₁, Sym.γ₁]).obj.Iso snake.obj)

γ₁γ₁ derives the spread high of Figure 12a.

theorem JardineHeinz2015.mergeRealize_γ₁_γ₂ : Nonempty ((Autosegmental.AR.mergeRealize true g [Sym.γ₁, Sym.γ₂]).obj.Iso sheep.obj)

γ₁γ₂ derives the high and downstepped high of Figure 12b: the floating high of γ₂ merges with the high of γ₁, and the linked high stays distinct.

theorem JardineHeinz2015.realizeMerged_γ₁_γ₂ : Nonempty ((Autosegmental.realizeMerged true g [Sym.γ₁, Sym.γ₂]).obj.Iso snake.obj)

Collapsing every run after concatenating merges all three highs of γ₁γ₂, deriving the spread graph of Figure 12a instead.

theorem JardineHeinz2015.not_nonempty_fullIso_realizeMerged : ¬Nonempty ((Autosegmental.AR.mergeRealize true g [Sym.γ₁, Sym.γ₂]).obj.Iso (Autosegmental.realizeMerged true g [Sym.γ₁, Sym.γ₂]).obj)

Once a primitive violates the OCP, collapsing after concatenation does not compute merging concatenation: the two realizations of γ₁γ₂ differ.