Tangale tone processes and the elision cascade

[Kid85]'s tonal and segmental rules that carry the perfective focus-marking reflex of [HZ04]. Tonemes are two (H, L; §1.16); High Tone Spread (her (31)) links a boundary-adjacent H one TBU rightward, creating a falling contour on the docked TBU, and Left Line Delinking (her (35a), her coinage) then erases the original line, shifting the H. Segmentally, final-vowel elision plus u-epenthesis into the resulting final cluster produce the perfective alternation pon-go ~ pon-ug (her (4a)): the suffix surfaces faithful at a prosodic boundary and elided–repaired phrase-medially. boundary_audible is the witness that blocking the cascade — the prosodic reflex of [HZ04]'s perfective focus — is perceptible.

inductive Tangale.Tone : Type

Tangale tonemes ([Kid85] §1.16): two levels; extralow is a phonetic realization, and falling contours arise only from spread.

• H : Tone
• L : Tone

@[implicit_reducible]

instance Tangale.instDecidableEqTone : DecidableEq Tone

Equations

• Tangale.instDecidableEqTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tangale.instReprTone.repr : Tone → ℕ → Std.Format

Equations

• Tangale.instReprTone.repr Tangale.Tone.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.Tone.H")).group prec✝
• Tangale.instReprTone.repr Tangale.Tone.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.Tone.L")).group prec✝

@[implicit_reducible]

instance Tangale.instReprTone : Repr Tone

Equations

• Tangale.instReprTone = { reprPrec := Tangale.instReprTone.repr }

def Tangale.hts {β : Type u_1} (g : Autosegmental.Graph Tone β) (i j : ℕ) : Autosegmental.Graph Tone β

High Tone Spread ([Kid85] (31)): the toneme at i — an H linked to TBU j at a morpheme or word boundary — spreads onto the following TBU. The structural description is carried by the application theorems.

Equations

• Tangale.hts g i j = g.link i (j + 1)

def Tangale.lld {β : Type u_1} (g : Autosegmental.Graph Tone β) (i j : ℕ) : Autosegmental.Graph Tone β

Left Line Delinking ([Kid85] (35a)): erase the original (left) line after the toneme has spread rightward.

Equations

• Tangale.lld g i j = g.delink i j

theorem Tangale.hts_surfacesWith_H {β : Type u_1} {g : Autosegmental.Graph Tone β} {i j : ℕ} (hH : g.upper.get? i = some Tone.H) : (hts g i j).SurfacesWith Tone.H (j + 1)

Spread creates the falling contour (§4.6): the docked TBU surfaces with H on top of whatever it already bore.

theorem Tangale.lld_hts_shift {β : Type u_1} {g : Autosegmental.Graph Tone β} {i j : ℕ} (hH : g.upper.get? i = some Tone.H) : (lld (hts g i j) i j).SurfacesWith Tone.H (j + 1) ∧ (i, j) ∉ (lld (hts g i j) i j).links

Spread followed by Left Line Delinking shifts the H one TBU rightward ((34)): the docked TBU keeps the new line and the source loses the original.

theorem Tangale.hts_ne_self {β : Type u_1} {g : Autosegmental.Graph Tone β} {i j : ℕ} (h : (i, j + 1) ∉ g.links) : hts g i j ≠ g

Blocking is representationally visible: where the spread line is absent, applying HTS changes the graph.

def Tangale.horseIsGood : Autosegmental.Graph Tone Unit

'Horse is good' ([Kid85] (29a) tuužé koŋ): H on the noun's final TBU, L on the predicate.

Equations

• Tangale.horseIsGood = { upper := LabeledTuple.ofList [Tangale.Tone.H, Tangale.Tone.L], lower := LabeledTuple.ofList [(), (), ()], links := {(0, 1), (1, 2)} }

The elision cascade (Ch. 2)

Final-vowel elision builds consonant clusters; the cluster constraints then force u-epenthesis. On the perfective suffix this yields [Kid85]'s (4a) alternation pón-é + gó → pon-go (clause-final, faithful) vs pon-ug (phrase-medial, elided and repaired) — the alternation whose blocking under focus is [HZ04]'s prosodic reflex.

inductive Tangale.Slot : Type

CV slots for the cluster phonotactics.

• C : Slot
• V : Slot

@[implicit_reducible]

instance Tangale.instDecidableEqSlot : DecidableEq Slot

Equations

• Tangale.instDecidableEqSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Tangale.instReprSlot : Repr Slot

Equations

• Tangale.instReprSlot = { reprPrec := Tangale.instReprSlot.repr }

def Tangale.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

• Tangale.instReprSlot.repr Tangale.Slot.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.Slot.C")).group prec✝
• Tangale.instReprSlot.repr Tangale.Slot.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tangale.Slot.V")).group prec✝

def Tangale.Phonotactic (w : List Slot) : Prop

The cluster constraints ([Kid85] p. 64): initial clusters are impermissible, medial three-consonant clusters are disallowed, and word-final clusters are not permitted.

Equations

• Tangale.Phonotactic w = (¬[Tangale.Slot.C, Tangale.Slot.C] <+: w ∧ ¬[Tangale.Slot.C, Tangale.Slot.C, Tangale.Slot.C] <:+: w ∧ ¬[Tangale.Slot.C, Tangale.Slot.C] <:+ w)

@[implicit_reducible]

instance Tangale.instDecidablePhonotactic (w : List Slot) : Decidable (Phonotactic w)

Equations

• Tangale.instDecidablePhonotactic w = Tangale.instDecidablePhonotactic._aux_1 w

def Tangale.ve (w : List Slot) : List Slot

Final-vowel elision (§2.2): delete a word-final vowel. Triggered by suffixation, compounding, and phrase-medial position; blocked at a prosodic boundary.

Equations

• Tangale.ve w = if w.getLast? = some Tangale.Slot.V then w.dropLast else w

def Tangale.epenthesize (w : List Slot) : List Slot

u-epenthesis ((4)): repair a word-final cluster by inserting the vowel between the penultimate and ultimate consonants.

Equations

• Tangale.epenthesize w = if [Tangale.Slot.C, Tangale.Slot.C] <:+ w then w.dropLast ++ [Tangale.Slot.V, Tangale.Slot.C] else w

def Tangale.ponE : List Slot

pón-é 'knew' ((4a)).

Equations

• Tangale.ponE = [Tangale.Slot.C, Tangale.Slot.V, Tangale.Slot.C, Tangale.Slot.V]

def Tangale.go : List Slot

The perfective suffix gó.

Equations

• Tangale.go = [Tangale.Slot.C, Tangale.Slot.V]

def Tangale.blockedForm : List Slot

The boundary form: word-internal elision only; the suffix surfaces faithful (pon-go; before a focused constituent, wai-gó lánda of [HZ04] (25)).

Equations

• Tangale.blockedForm = Tangale.ve Tangale.ponE ++ Tangale.go

def Tangale.elidedForm : List Slot

The phrase-medial form: phrasal elision hits the suffix vowel and epenthesis repairs the final cluster (pon-ug ŋâi 'knew Ngai').

Equations

• Tangale.elidedForm = Tangale.epenthesize (Tangale.ve (Tangale.ve Tangale.ponE ++ Tangale.go))

theorem Tangale.boundary_audible : blockedForm ≠ elidedForm ∧ Phonotactic blockedForm ∧ Phonotactic elidedForm

The cascade is audible: both outputs are phonotactically licit and they differ — blocking phrasal elision (the prosodic boundary of the perfective focus reflex) is perceptible.