Jardine (2017): The local nature of tone-association patterns

This file formalizes [Jar17b]'s claim that tone-association patterns are local: each is specified by a finite grammar ¬r₁ ∧ … ∧ ¬rₙ of forbidden connected subgraphs of autosegmental representations, so that well-formedness is checked, and learned, by scanning a bounded window. The directional patterns of the paper's typology are the test case: Mende allows plateaus and contours only at the right word edge, (4)–(5), and Hausa only at the left, (6)–(7). The grammars (21) and (22) forbid non-final spreading and contours, and non-initial ones, mirror images differing only in the edge. Mende.free and Hausa.free show every word of (4) and (6) well formed under its own grammar, and Mende.not_free_hántúnàa and Hausa.not_free_félàmà that each language's diagnostic form fails the other's grammar, left-edge spreading being exactly what (21) forbids and right-edge spreading exactly what (22) forbids, (18) and (16). Northern Karanga Shona, Kukuya, and Hirosaki Japanese, (23)–(38), follow the same schema and are not formalized.

Implementation notes

• Forbidden subgraphs are factors (AR.FactorEmbeds). The contour subgraph (19) leaves its two tones unordered so as to match rising as well as falling contours; a factor's tier word is ordered, so (19) is rendered as the pair of orders.

References

• [Jar17b]

@[reducible, inline]

abbrev Jardine2017.σ : Tone.TBUKind

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

Equations

• Jardine2017.σ = Tone.TBUKind.syllable

@[reducible, inline]

abbrev Jardine2017.ar (tones : List Tone.TRN) (tbus : List Tone.TBUKind) (lines : List (ℕ × ℕ)) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

A representation drawn as the paper does: a melody over a syllable string, with the association lines given as pairs of positions.

Equations

• Jardine2017.ar tones tbus lines = Autosegmental.AR.ofWords tones tbus fun (p q : ℕ) => (p, q) ∈ lines

@[reducible, inline]

abbrev Jardine2017.Grammar : Type (u_1 + 1)

The grammar of forbidden subgraphs ¬r₁ ∧ … ∧ ¬rₙ of (3a), as the list of factors.

Equations

• Jardine2017.Grammar = List { F : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind) // Finite F.obj.V }

Mende: multiple association at the right edge

def Jardine2017.Mende.forms : List (List Tone.TRN × List Tone.TBUKind × List (ℕ × ℕ))

The words of (4), drawn as in (5): mbû 'owl', ngílà 'dog', félàmà 'junction', mbâ 'companion', nyàhâ 'woman', nìkílì 'groundnut' — melody, syllables, lines.

Equations

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

@[reducible, inline]

abbrev Jardine2017.Mende.nonfinalH : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

(17): a non-final H, and a non-final L, associated to two syllables.

Equations

• Jardine2017.Mende.nonfinalH = Jardine2017.ar [Tone.TRN.H, Tone.TRN.L] [Jardine2017.σ, Jardine2017.σ] [(0, 0), (0, 1)]

@[reducible, inline]

abbrev Jardine2017.Mende.nonfinalL : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

Equations

• Jardine2017.Mende.nonfinalL = Jardine2017.ar [Tone.TRN.L, Tone.TRN.H] [Jardine2017.σ, Jardine2017.σ] [(0, 0), (0, 1)]

@[reducible, inline]

abbrev Jardine2017.Mende.nonfinalHL : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

(19): a contour on a non-final syllable, in both tone orders.

Equations

• Jardine2017.Mende.nonfinalHL = Jardine2017.ar [Tone.TRN.H, Tone.TRN.L] [Jardine2017.σ, Jardine2017.σ] [(0, 0), (1, 0)]

@[reducible, inline]

abbrev Jardine2017.Mende.nonfinalLH : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

Equations

• Jardine2017.Mende.nonfinalLH = Jardine2017.ar [Tone.TRN.L, Tone.TRN.H] [Jardine2017.σ, Jardine2017.σ] [(0, 0), (1, 0)]

def Jardine2017.Mende.grammar : Grammar

The Mende grammar (21).

Equations

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

theorem Jardine2017.Mende.free_grammar_iff (X : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)) [Finite X.obj.V] : Autosegmental.AR.Free X grammar ↔ ¬Autosegmental.AR.FactorEmbeds nonfinalH X ∧ ¬Autosegmental.AR.FactorEmbeds nonfinalL X ∧ ¬Autosegmental.AR.FactorEmbeds nonfinalHL X ∧ ¬Autosegmental.AR.FactorEmbeds nonfinalLH X

@[instance_reducible]

instance Jardine2017.Mende.instDecidableFreeBoolTwoTierTRNTBUKindArGrammar (tones : List Tone.TRN) (tbus : List Tone.TBUKind) (lines : List (ℕ × ℕ)) : Decidable (Autosegmental.AR.Free (ar tones tbus lines) grammar)

Equations

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

theorem Jardine2017.Mende.free (f : List Tone.TRN × List Tone.TBUKind × List (ℕ × ℕ)) : f ∈ forms → Autosegmental.AR.Free (ar f.1 f.2.1 f.2.2) grammar

Every word of (4) is well-formed under (21).

Hausa: multiple association at the left edge

def Jardine2017.Hausa.forms : List (List Tone.TRN × List Tone.TBUKind × List (ℕ × ℕ))

The words of (6), drawn as in (7): fáadì 'fall', hántúnàa 'noses', búhúnhúnàa 'sacks', mántá 'forget', káràntá 'read', kákkáràntá 'reread' — melody, syllables, lines.

Equations

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

@[reducible, inline]

abbrev Jardine2017.Hausa.noninitialH : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

(22): a non-initial H, and a non-initial L, associated to two syllables.

Equations

• Jardine2017.Hausa.noninitialH = Jardine2017.ar [Tone.TRN.L, Tone.TRN.H] [Jardine2017.σ, Jardine2017.σ] [(1, 0), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Hausa.noninitialL : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

Equations

• Jardine2017.Hausa.noninitialL = Jardine2017.ar [Tone.TRN.H, Tone.TRN.L] [Jardine2017.σ, Jardine2017.σ] [(1, 0), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Hausa.noninitialHL : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

(22): a contour on a non-initial syllable, in both tone orders.

Equations

• Jardine2017.Hausa.noninitialHL = Jardine2017.ar [Tone.TRN.H, Tone.TRN.L] [Jardine2017.σ, Jardine2017.σ] [(0, 1), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Hausa.noninitialLH : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)

Equations

• Jardine2017.Hausa.noninitialLH = Jardine2017.ar [Tone.TRN.L, Tone.TRN.H] [Jardine2017.σ, Jardine2017.σ] [(0, 1), (1, 1)]

def Jardine2017.Hausa.grammar : Grammar

The Hausa grammar (22).

Equations

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

theorem Jardine2017.Hausa.free_grammar_iff (X : Autosegmental.TieredAR Bool (Autosegmental.TwoTier Tone.TRN Tone.TBUKind)) [Finite X.obj.V] : Autosegmental.AR.Free X grammar ↔ ¬Autosegmental.AR.FactorEmbeds noninitialH X ∧ ¬Autosegmental.AR.FactorEmbeds noninitialL X ∧ ¬Autosegmental.AR.FactorEmbeds noninitialHL X ∧ ¬Autosegmental.AR.FactorEmbeds noninitialLH X

@[instance_reducible]

instance Jardine2017.Hausa.instDecidableFreeBoolTwoTierTRNTBUKindArGrammar (tones : List Tone.TRN) (tbus : List Tone.TBUKind) (lines : List (ℕ × ℕ)) : Decidable (Autosegmental.AR.Free (ar tones tbus lines) grammar)

Equations

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

theorem Jardine2017.Hausa.free (f : List Tone.TRN × List Tone.TBUKind × List (ℕ × ℕ)) : f ∈ forms → Autosegmental.AR.Free (ar f.1 f.2.1 f.2.2) grammar

Every word of (6) is well-formed under (22).

The contrast: the same subgraphs at opposite edges

theorem Jardine2017.Mende.not_free_hántúnàa : ¬Autosegmental.AR.Free (ar [Tone.TRN.H, Tone.TRN.L] [σ, σ, σ] [(0, 0), (0, 1), (1, 2)]) grammar

Hausa's hántúnàa (HHL, H spread at the left edge) contains (21)'s non-final H spread ((18a) is a valid Hausa representation).

theorem Jardine2017.Hausa.not_free_félàmà : ¬Autosegmental.AR.Free (ar [Tone.TRN.H, Tone.TRN.L] [σ, σ, σ] [(0, 0), (1, 1), (1, 2)]) grammar

Mende's félàmà (HLL, L spread at the right edge) contains (22)'s non-initial L spread ((16a) is ill-formed in Hausa).