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

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

@[instance_reducible]

instance Tangale.instReprTone : Repr Tone

Equations

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

def Tangale.hts (L : Bool → Bool → ℕ → ℕ → Prop) (i j : ℕ) (b b' : Bool) (p q : ℕ) : Prop

High Tone Spread ([Kid85] (31)) on the link presentation: the toneme at i — an H linked to TBU j at a morpheme or word boundary — spreads onto the following TBU.

Equations

• Tangale.hts L i j b b' p q = (L b b' p q ∨ b = true ∧ b' = false ∧ p = i ∧ q = j + 1)

def Tangale.lld (L : Bool → Bool → ℕ → ℕ → Prop) (i j : ℕ) (b b' : Bool) (p q : ℕ) : Prop

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

Equations

• Tangale.lld L i j b b' p q = (L b b' p q ∧ ¬(b = true ∧ b' = false ∧ p = i ∧ q = j))

theorem Tangale.hts_surfacesWith_H {ws : (b : Bool) → List (Autosegmental.TwoTier Tone Unit b)} {L : Bool → Bool → ℕ → ℕ → Prop} {i j : ℕ} (hH : (ws true)[i]? = some Tone.H) (hj : j + 1 < (ws false).length) : Autosegmental.AR.surfacesWith (Autosegmental.AR.ofData ws (hts L i j)) 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 {ws : (b : Bool) → List (Autosegmental.TwoTier Tone Unit b)} {L : Bool → Bool → ℕ → ℕ → Prop} {i j : ℕ} (hH : (ws true)[i]? = some Tone.H) (hj : j + 1 < (ws false).length) (hne : j + 1 ≠ j) (hor : ∀ (p q : ℕ), ¬L false true p q) : Autosegmental.AR.surfacesWith (Autosegmental.AR.ofData ws (lld (hts L i j) i j)) Tone.H (j + 1) ∧ ¬Autosegmental.AR.link (Autosegmental.AR.ofData ws (lld (hts L i j) i j)) true false i j

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.

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

@[instance_reducible]

instance Tangale.instDecidableEqSlot : DecidableEq Slot

Equations

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

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

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