Grammatical tone

Grammatical tone is a tonological operation restricted to a specific morpheme or construction, or a natural class of them, and not attributable to the general tonal phonology. This file gives Rolle's vocabulary for it over strings of tone-bearing units: the grammatical tune that covaries with the construction, anchored at an edge of its host, and the four dominance effects by which a trigger's tune interacts with the tones of its target-host. A dominant trigger imposes its pattern whatever the target's tones, a recessive one only on an unvalued target, and a neutral one leaves the target to the general phonology. Dominance is the neutralisation of the target's valued–unvalued contrast, which Rolle calls transparadigmatic uniformity, and Dominance.isDominant_iff_uniform derives his classification from it.

Main definitions

• TBU, TBU.IsValued: a tone-bearing unit with its tonal root node, valued when the node is specified.
• Tune, Tune.realize: a grammatical tune, a melody anchored at an edge of the host, and its realisation over a number of units: one tone per unit from the anchored edge, the last tone reached spreading over the remainder.
• overwrite, unvalue: replacement of a host's tones by a tune, and their deletion.
• Uniform: transparadigmatic uniformity of an operation on hosts.
• Dominance, Dominance.apply: Rolle's replacive-dominant, subtractive-dominant, recessive, and neutral triggers, and the automatic operation each performs on its target-host.

Main results

• overwrite_unvalue: a host and its unvalued projection are overwritten alike.
• Dominance.isDominant_iff_uniform: a trigger is dominant exactly when its operation is uniform across targets of the same segments.

Implementation notes

A tone-bearing unit carries one root node, so contours are not represented and a tune longer than its host is truncated at the anchored edge. The valuation window is coextensive with the host, Rolle's default; local windows are not modelled. The neutral trigger's tune floats and its docking is left to the general phonology, so its automatic operation is the identity on the host. Which edge a tune anchors at is a property of the construction: Akinbo and Fwangwar's M-H verbaliser anchors right, putting H on the final unit and M on the rest.

References

• [Rol18]
• [LMcPR22]
• [Ink98]
• [KH77]
• [Hym18]
• [CG84]
• [AF26]

Tone-bearing units

structure Tone.TBU (S : Type u_1) : Type u_1

A tone-bearing unit is segmental content of type S, a syllable or a mora, carrying one tonal root node.

• seg : S
• tone : TRN

@[instance_reducible]

instance Tone.instDecidableEqTBU {S✝ : Type u_1} [DecidableEq S✝] : DecidableEq (TBU S✝)

Equations

• Tone.instDecidableEqTBU = Tone.instDecidableEqTBU.decEq

def Tone.instDecidableEqTBU.decEq {S✝ : Type u_1} [DecidableEq S✝] (x✝ x✝¹ : TBU S✝) : Decidable (x✝ = x✝¹)

Equations

• Tone.instDecidableEqTBU.decEq { seg := a, tone := a_1 } { seg := b, tone := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Tone.instReprTBU.repr {S✝ : Type u_1} [Repr S✝] : TBU S✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tone.instReprTBU {S✝ : Type u_1} [Repr S✝] : Repr (TBU S✝)

Equations

• Tone.instReprTBU = { reprPrec := Tone.instReprTBU.repr }

def Tone.TBU.IsValued {S : Type u_1} (τ : TBU S) : Prop

A unit is valued when its root node is specified and unvalued when it is a free unit ([Rol18] Table 1, after [CG84]).

Equations

• τ.IsValued = (τ.tone ≠ Tone.TRN.empty)

@[instance_reducible]

instance Tone.TBU.instDecidablePredIsValued {S : Type u_1} : DecidablePred IsValued

Equations

• x✝.instDecidablePredIsValued = { decide := !decide (x✝.tone = Tone.TRN.empty), reflects_decide := ⋯ }

Grammatical tunes

structure Tone.Tune : Type

A grammatical tune ([Rol18] (1a)) is the tone sequence that covaries with the construction, anchored at an edge of its host.

• melody : List TRN
• anchor : Edge

def Tone.instDecidableEqTune.decEq (x✝ x✝¹ : Tune) : Decidable (x✝ = x✝¹)

Equations

• Tone.instDecidableEqTune.decEq { melody := a, anchor := a_1 } { melody := b, anchor := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Tone.instDecidableEqTune : DecidableEq Tune

Equations

• Tone.instDecidableEqTune = Tone.instDecidableEqTune.decEq

def Tone.instReprTune.repr : Tune → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tone.instReprTune : Repr Tune

Equations

• Tone.instReprTune = { reprPrec := Tone.instReprTune.repr }

def Tone.Tune.realizeLeft : ℕ → List TRN → List TRN

A melody over n units from the left puts one tone on each unit, the last tone spreading over the remaining units and an empty melody leaving them unvalued.

Equations

• Tone.Tune.realizeLeft 0 x✝ = []
• Tone.Tune.realizeLeft n.succ [] = List.replicate (n + 1) Tone.TRN.empty
• Tone.Tune.realizeLeft n.succ [t] = t :: Tone.Tune.realizeLeft n [t]
• Tone.Tune.realizeLeft n.succ (t :: t' :: ts) = t :: Tone.Tune.realizeLeft n (t' :: ts)

def Tone.Tune.realize (u : Tune) (n : ℕ) : List TRN

The tune realised over n units puts one tone on each unit from the anchored edge, the last tone reached spreading over the remainder.

Equations

• u.realize n = match u.anchor with | Edge.left => Tone.Tune.realizeLeft n u.melody | Edge.right => (Tone.Tune.realizeLeft n u.melody.reverse).reverse

@[simp]

theorem Tone.Tune.length_realizeLeft (n : ℕ) (m : List TRN) : (realizeLeft n m).length = n

@[simp]

theorem Tone.Tune.length_realize (u : Tune) (n : ℕ) : (u.realize n).length = n

theorem Tone.Tune.realizeLeft_singleton (n : ℕ) (t : TRN) : realizeLeft n [t] = List.replicate n t

@[simp]

theorem Tone.Tune.realize_singleton (t : TRN) (e : Edge) (n : ℕ) : { melody := [t], anchor := e }.realize n = List.replicate n t

A one-tone tune spreads its tone over every unit, whichever edge it anchors at.

theorem Tone.Tune.realize_pair_right (t₁ t₂ : TRN) (n : ℕ) : { melody := [t₁, t₂], anchor := Edge.right }.realize (n + 1) = List.replicate n t₁ ++ [t₂]

A two-tone tune anchored right puts its second tone on the final unit and its first on the rest.

Operations on a target-host

def Tone.withTier {S : Type u_1} (host : List (TBU S)) (tier : List TRN) : List (TBU S)

The host with its tonal tier replaced.

Equations

• Tone.withTier host tier = List.zipWith (fun (τ : Tone.TBU S) (t : Tone.TRN) => { seg := τ.seg, tone := t }) host tier

theorem Tone.withTier_eq_of_map_seg_eq {S : Type u_1} {h h' : List (TBU S)} (tier : List TRN) : List.map TBU.seg h = List.map TBU.seg h' → withTier h tier = withTier h' tier

theorem Tone.map_seg_withTier {S : Type u_1} (h : List (TBU S)) (tier : List TRN) : tier.length = h.length → List.map TBU.seg (withTier h tier) = List.map TBU.seg h

theorem Tone.map_tone_withTier {S : Type u_1} (h : List (TBU S)) (tier : List TRN) : tier.length = h.length → List.map TBU.tone (withTier h tier) = tier

def Tone.overwrite {S : Type u_1} (host : List (TBU S)) (u : Tune) : List (TBU S)

Replacement of the host's tones by the tune ([Rol18] Def 1) is the tune realised over the host's units.

Equations

• Tone.overwrite host u = Tone.withTier host (u.realize host.length)

def Tone.unvalue {S : Type u_1} (host : List (TBU S)) : List (TBU S)

Deletion of the host's tones ([Rol18] Def 2) leaves every unit unvalued.

Equations

• Tone.unvalue host = List.map (fun (τ : Tone.TBU S) => { seg := τ.seg, tone := Tone.TRN.empty }) host

@[simp]

theorem Tone.overwrite_nil {S : Type u_1} (u : Tune) : overwrite [] u = []

@[simp]

theorem Tone.map_seg_overwrite {S : Type u_1} (host : List (TBU S)) (u : Tune) : List.map TBU.seg (overwrite host u) = List.map TBU.seg host

@[simp]

theorem Tone.map_tone_overwrite {S : Type u_1} (host : List (TBU S)) (u : Tune) : List.map TBU.tone (overwrite host u) = u.realize host.length

The tonal tier of an overwritten host is the tune realised over it.

@[simp]

theorem Tone.length_overwrite {S : Type u_1} (host : List (TBU S)) (u : Tune) : (overwrite host u).length = host.length

theorem Tone.map_tone_overwrite_singleton {S : Type u_1} (host : List (TBU S)) (t : TRN) (e : Edge) : List.map TBU.tone (overwrite host { melody := [t], anchor := e }) = List.map (fun (x : TBU S) => t) host

A one-tone tune makes every unit's tone that tone.

@[simp]

theorem Tone.map_seg_unvalue {S : Type u_1} (host : List (TBU S)) : List.map TBU.seg (unvalue host) = List.map TBU.seg host

def Tone.Uniform {S : Type u_1} (op : List (TBU S) → List (TBU S)) : Prop

An operation on target-hosts is transparadigmatically uniform ([Rol18] ch. 5) when it gives the same output for hosts of the same segments, whatever their tones.

Equations

• Tone.Uniform op = ∀ ⦃h h' : List (Tone.TBU S)⦄, List.map Tone.TBU.seg h = List.map Tone.TBU.seg h' → op h = op h'

theorem Tone.overwrite_eq_of_map_seg_eq {S : Type u_1} {h h' : List (TBU S)} (hs : List.map TBU.seg h = List.map TBU.seg h') (u : Tune) : overwrite h u = overwrite h' u

theorem Tone.uniform_overwrite {S : Type u_1} (u : Tune) : Uniform fun (x : List (TBU S)) => overwrite x u

theorem Tone.uniform_unvalue {S : Type u_1} : Uniform unvalue

@[simp]

theorem Tone.overwrite_unvalue {S : Type u_1} (host : List (TBU S)) (u : Tune) : overwrite (unvalue host) u = overwrite host u

Overwriting erases, in that a host and its unvalued projection are overwritten alike, which is why a replacive trigger neutralises the target's tones.

Dominance effects

inductive Tone.Dominance : Type

[Rol18]'s dominance effects, his four types of trigger (Defs 1–4, Table 2) by how the trigger's tune interacts with the tonal value of its target-host. Dominance is a lexical idiosyncrasy of the trigger, predictable neither from its segments and prosody nor from the markedness of the tune nor from its position relative to the target ([Ink98]); the terms are those of the accentual morphology of [KH77].

• replacive : Dominance

  A replacive-dominant trigger (Def 1) replaces the underlying tones within the valuation window by the tune, whether by a floating tone or by spreading from the sponsor. Valued and unvalued targets come out alike, an intentional neutralisation in [Hym18]'s sense.

• subtractive : Dominance

  A subtractive-dominant trigger (Def 2) deletes the underlying tones within the valuation window, with no tune to revalue them; the surface tones are supplied later by default.

• recessive : Dominance

  The tune of a recessive non-dominant trigger (Def 3) does not apply to a target valued within the valuation window, so it docks only to unvalued targets, as in privative systems with one contrastive tone.

• neutral : Dominance

  A neutral non-dominant trigger (Def 4) has neither automatic replacement or deletion nor automatic non-application; the tune concatenates with the target and the general phonology decides its docking.

@[instance_reducible]

instance Tone.instDecidableEqDominance : DecidableEq Dominance

Equations

• Tone.instDecidableEqDominance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Tone.instReprDominance : Repr Dominance

Equations

• Tone.instReprDominance = { reprPrec := Tone.instReprDominance.repr }

def Tone.instReprDominance.repr : Dominance → ℕ → Std.Format

Equations

• Tone.instReprDominance.repr Tone.Dominance.replacive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Dominance.replacive")).group prec✝
• Tone.instReprDominance.repr Tone.Dominance.subtractive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Dominance.subtractive")).group prec✝
• Tone.instReprDominance.repr Tone.Dominance.recessive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Dominance.recessive")).group prec✝
• Tone.instReprDominance.repr Tone.Dominance.neutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Dominance.neutral")).group prec✝

def Tone.Dominance.IsDominant (d : Dominance) : Prop

The dominant types, which neutralise the target's valued–unvalued contrast.

Equations

• d.IsDominant = (d = Tone.Dominance.replacive ∨ d = Tone.Dominance.subtractive)

@[instance_reducible]

instance Tone.Dominance.instDecidablePredIsDominant : DecidablePred IsDominant

Equations

• x✝.instDecidablePredIsDominant = { decide := decide (x✝ = Tone.Dominance.replacive) || decide (x✝ = Tone.Dominance.subtractive), reflects_decide := ⋯ }

def Tone.Dominance.apply {S : Type u_1} (d : Dominance) (u : Tune) (host : List (TBU S)) : List (TBU S)

The automatic operation a trigger of each type performs on its target-host, the valuation window being the whole host. The four are replacement by the tune, deletion, docking of the tune only to a wholly unvalued host, and nothing.

Equations

• Tone.Dominance.replacive.apply u host = Tone.overwrite host u
• Tone.Dominance.subtractive.apply u host = Tone.unvalue host
• Tone.Dominance.recessive.apply u host = if ∃ τ ∈ host, τ.IsValued then host else Tone.overwrite host u
• Tone.Dominance.neutral.apply u host = host

@[simp]

theorem Tone.Dominance.apply_replacive {S : Type u_1} (u : Tune) (host : List (TBU S)) : replacive.apply u host = overwrite host u

@[simp]

theorem Tone.Dominance.apply_subtractive {S : Type u_1} (u : Tune) (host : List (TBU S)) : subtractive.apply u host = unvalue host

@[simp]

theorem Tone.Dominance.apply_neutral {S : Type u_1} (u : Tune) (host : List (TBU S)) : neutral.apply u host = host

theorem Tone.Dominance.apply_recessive_of_valued {S : Type u_1} (u : Tune) {host : List (TBU S)} (h : ∃ τ ∈ host, τ.IsValued) : recessive.apply u host = host

A recessive tune does not apply to a valued target.

theorem Tone.Dominance.apply_recessive_of_unvalued {S : Type u_1} (u : Tune) {host : List (TBU S)} (h : ∀ τ ∈ host, ¬τ.IsValued) : recessive.apply u host = overwrite host u

A recessive tune docks to an unvalued target.

theorem Tone.Dominance.uniform_apply_of_isDominant {S : Type u_1} {d : Dominance} (hd : d.IsDominant) (u : Tune) : Uniform (d.apply u)

theorem Tone.Dominance.isDominant_iff_uniform {S : Type u_1} [Inhabited S] (d : Dominance) : d.IsDominant ↔ ∀ (u : Tune), Uniform (d.apply u)

Dominance is transparadigmatic uniformity ([Rol18] ch. 5), in that a trigger is dominant exactly when its operation gives the same output for every target of the same segments.