Hyman (2006): Word-prosodic typology

This file formalizes [Hym06]'s two prototypes of word prosody and the argument that pitch accent is no third. A language has tone when an indication of pitch enters the lexical realization of some morpheme, definition (3) (Tonal); it has stress accent when word-level metrical structure marks a head syllable in every lexical word, definition (5), which separates into obligatoriness, at least one head (Obligatory), and culminativity, at most one (Culminative), the pair that the usual one and only one conflates (obligatory_and_culminative_iff). Obligatoriness is the definitional criterion, OBLHEAD, and it targets syllables: a language whose words may lack syllables cannot have stress accent (not_obligatory_of_no_units, Bella Coola), and an obligatory H assigned by mora is restricted tone rather than stress accent (kinga_not_stressAccent).

The four combinations of the two criteria are all attested among restricted-H systems, Table II: Kinga's antepenultimate-mora H is obligatory and culminative, Creek's tonal accent obligatory but not culminative, Tokyo Japanese's accent culminative but not obligatory, read off the accent lexicon of the Japanese fragment (tokyo_not_obligatory), and Seneca's trochaic H neither, derived from the analysis of (21) (seneca_not_obligatory). So neither criterion implies the other, no hierarchical typology can cut first by one and then by the other, and the cut by OBLHEAD and the reviewer's cut by culminativity of Section 7 classify Creek and Tokyo Japanese oppositely (cuts_differ).

Implementation notes

• A Marking records, for each lexical word, its units and the units bearing the mark, the primary stress or the restricted tone; the tone-bearing unit is Tone.TBUKind. Tone is stated on a lexicon of morphemes with an optional pitch specification.
• Table I's languages are not listed; its two dimensions are Tonal and StressAccent, which Studies/Lionnet2025 evaluates for Drubea.

References

• [Hym06]
• [Lio25]

The two prototypes

def Hyman2006.Tonal {M : Type u_1} {P : Type u_2} (pitch : M → Option P) : Prop

Definition (3): a lexicon is tonal when an indication of pitch enters the lexical realization of at least one morpheme.

Equations

• Hyman2006.Tonal pitch = ∃ (μ : M), (pitch μ).isSome = true

structure Hyman2006.Marking (Word : Type u_1) (U : Type u_2) : Type (max u_1 u_2)

A word-level marking: the units of each lexical word and those bearing the mark, the highest degree of metrical prominence or the restricted tone, on units of a kind.

• units : Word → Finset U
• marked : Word → Finset U
• marked_subset (w : Word) : self.marked w ⊆ self.units w
• tbu : Tone.TBUKind

def Hyman2006.Obligatory {Word : Type u_1} {U : Type u_2} (m : Marking Word U) : Prop

(5a): every lexical word has at least one marked unit, OBLHEAD.

Equations

• Hyman2006.Obligatory m = ∀ (w : Word), (m.marked w).Nonempty

def Hyman2006.Culminative {Word : Type u_1} {U : Type u_2} (m : Marking Word U) : Prop

(5b): every lexical word has at most one marked unit.

Equations

• Hyman2006.Culminative m = ∀ (w : Word), (m.marked w).card ≤ 1

def Hyman2006.StressAccent {Word : Type u_1} {U : Type u_2} (m : Marking Word U) : Prop

Definition (5): stress accent is an obligatory, culminative marking of syllables.

Equations

• Hyman2006.StressAccent m = (m.tbu = Tone.TBUKind.syllable ∧ Hyman2006.Obligatory m ∧ Hyman2006.Culminative m)

theorem Hyman2006.obligatory_and_culminative_iff {Word : Type u_1} {U : Type u_2} (m : Marking Word U) : Obligatory m ∧ Culminative m ↔ ∀ (w : Word), (m.marked w).card = 1

The two criteria together are the one and only one head of McCarthy's HEAD(PWd), which (5) separates.

theorem Hyman2006.grid_isCulminative_iff (g : Prosody.Grid) : g.IsCulminative ↔ 1 ≤ List.countP (fun (x : ℕ) => x == g.peak) g ∧ List.countP (fun (x : ℕ) => x == g.peak) g ≤ 1

The metrical grid's culminativity, exactly one peak, is the same conflation.

def Hyman2006.Marking.ofRule {Word : Type u_1} {U : Type u_2} (units : Word → Finset U) (pos : Word → U) (h : ∀ (w : Word), pos w ∈ units w) (tbu : Tone.TBUKind) : Marking Word U

A marking assigned by a rule that names one unit of every word is obligatory and culminative.

Equations

• Hyman2006.Marking.ofRule units pos h tbu = { units := units, marked := fun (w : Word) => {pos w}, marked_subset := ⋯, tbu := tbu }

theorem Hyman2006.obligatory_ofRule {Word : Type u_1} {U : Type u_2} (units : Word → Finset U) (pos : Word → U) (h : ∀ (w : Word), pos w ∈ units w) (tbu : Tone.TBUKind) : Obligatory (Marking.ofRule units pos h tbu)

theorem Hyman2006.culminative_ofRule {Word : Type u_1} {U : Type u_2} (units : Word → Finset U) (pos : Word → U) (h : ∀ (w : Word), pos w ∈ units w) (tbu : Tone.TBUKind) : Culminative (Marking.ofRule units pos h tbu)

theorem Hyman2006.not_obligatory_of_no_units {Word : Type u_1} {U : Type u_2} {m : Marking Word U} {w : Word} (h : m.units w = ∅) : ¬Obligatory m

Section 4: a word without units of the marked kind, Bella Coola's syllable-less [ktskʷ] or Gokana's words, can bear no head, so the language fails OBLHEAD.

theorem Hyman2006.not_stressAccent_of_no_units {Word : Type u_1} {U : Type u_2} {m : Marking Word U} {w : Word} (h : m.units w = ∅) : ¬StressAccent m

Tokyo Japanese

def Hyman2006.tokyo : Marking Japanese.Prosody.ProsodicEntry ℕ

The accent of Tokyo Japanese as a marking of moras: the accented mora of each lexical entry of the fragment, or none.

Equations

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

theorem Hyman2006.tokyo_tonal : Tonal fun (e : Japanese.Prosody.ProsodicEntry) => e.accentMora

The accent is an indication of pitch in the lexical realization of a'me 'rain', so Tokyo Japanese is tonal by (3).

theorem Hyman2006.tokyo_culminative : Culminative tokyo

At most one accent per word.

theorem Hyman2006.tokyo_not_obligatory : ¬Obligatory tokyo

ame 'candy' is unaccented, so the accent is not obligatory.

theorem Hyman2006.tokyo_not_stressAccent : ¬StressAccent tokyo

Section 5.2: the classic pitch-accent language is tonal without stress accent.

Kinga

inductive Hyman2006.KingaWord : Type

The words of (18b).

• ukuheka : KingaWord
• ukuvala : KingaWord
• ukugeenda : KingaWord
• ukugeendelela : KingaWord
• ukuhwaanana : KingaWord

@[instance_reducible]

instance Hyman2006.instDecidableEqKingaWord : DecidableEq KingaWord

Equations

• Hyman2006.instDecidableEqKingaWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hyman2006.instReprKingaWord.repr : KingaWord → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hyman2006.instReprKingaWord : Repr KingaWord

Equations

• Hyman2006.instReprKingaWord = { reprPrec := Hyman2006.instReprKingaWord.repr }

def Hyman2006.KingaWord.nMorae : KingaWord → ℕ

The mora counts of the words.

Equations

• Hyman2006.KingaWord.ukuheka.nMorae = 4
• Hyman2006.KingaWord.ukuvala.nMorae = 4
• Hyman2006.KingaWord.ukugeenda.nMorae = 5
• Hyman2006.KingaWord.ukugeendelela.nMorae = 7
• Hyman2006.KingaWord.ukuhwaanana.nMorae = 6

def Hyman2006.kinga : Marking KingaWord ℕ

Kinga's obligatory H falls on the antepenultimate mora, (18b).

Equations

• Hyman2006.kinga = Hyman2006.Marking.ofRule (fun (w : Hyman2006.KingaWord) => Finset.range w.nMorae) (fun (w : Hyman2006.KingaWord) => w.nMorae - 3) ⋯ Tone.TBUKind.mora

theorem Hyman2006.kinga_obligatory : Obligatory kinga

theorem Hyman2006.kinga_culminative : Culminative kinga

theorem Hyman2006.kinga_not_stressAccent : ¬StressAccent kinga

Section 5.2: assigned by mora, the obligatory H of Kinga is restricted tone, not stress accent.

Creek

inductive Hyman2006.CreekWord : Type

The words of (20) and the fixed-accent /náfka:kís/ of Section 5.3.

• hicita : CreekWord
• ahicita : CreekWord
• caalo : CreekWord
• sokca : CreekWord
• nafkaakis : CreekWord

@[instance_reducible]

instance Hyman2006.instDecidableEqCreekWord : DecidableEq CreekWord

Equations

• Hyman2006.instDecidableEqCreekWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hyman2006.instReprCreekWord : Repr CreekWord

Equations

• Hyman2006.instReprCreekWord = { reprPrec := Hyman2006.instReprCreekWord.repr }

def Hyman2006.instReprCreekWord.repr : CreekWord → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hyman2006.instReprCreekWord.repr Hyman2006.CreekWord.hicita prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2006.CreekWord.hicita")).group prec✝
• Hyman2006.instReprCreekWord.repr Hyman2006.CreekWord.caalo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2006.CreekWord.caalo")).group prec✝
• Hyman2006.instReprCreekWord.repr Hyman2006.CreekWord.sokca prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2006.CreekWord.sokca")).group prec✝

def Hyman2006.CreekWord.nSyllables : CreekWord → ℕ

Equations

• Hyman2006.CreekWord.hicita.nSyllables = 3
• Hyman2006.CreekWord.ahicita.nSyllables = 4
• Hyman2006.CreekWord.caalo.nSyllables = 2
• Hyman2006.CreekWord.sokca.nSyllables = 2
• Hyman2006.CreekWord.nafkaakis.nSyllables = 3

def Hyman2006.CreekWord.accents : CreekWord → Finset ℕ

The tonal accents: the last even-numbered light syllable (20a), a heavy penult (20b), and the two fixed accents of /náfka:kís/.

Equations

• Hyman2006.CreekWord.hicita.accents = {1}
• Hyman2006.CreekWord.ahicita.accents = {3}
• Hyman2006.CreekWord.caalo.accents = {0}
• Hyman2006.CreekWord.sokca.accents = {0}
• Hyman2006.CreekWord.nafkaakis.accents = {0, 2}

def Hyman2006.creek : Marking CreekWord ℕ

Equations

• Hyman2006.creek = { units := fun (w : Hyman2006.CreekWord) => Finset.range w.nSyllables, marked := Hyman2006.CreekWord.accents, marked_subset := ⋯, tbu := Tone.TBUKind.syllable }

theorem Hyman2006.creek_obligatory : Obligatory creek

Creek obeys OBLHEAD.

theorem Hyman2006.creek_not_culminative : ¬Culminative creek

/náfka:kís/ carries two H tones.

Seneca

def Hyman2006.senecaH (closed : List Bool) : Finset ℕ

The trochaic analysis of (21): the first syllable is extrametrical, disyllabic trochees are built left to right, and a trochee's initial syllable takes H when the trochee contains a closed syllable. A word is its syllables' closedness.

Equations

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

inductive Hyman2006.SenecaWord : Type

The words of (23), with a closed syllable marked true.

• willing : SenecaWord
• busy : SenecaWord
• necktie : SenecaWord

@[instance_reducible]

instance Hyman2006.instDecidableEqSenecaWord : DecidableEq SenecaWord

Equations

• Hyman2006.instDecidableEqSenecaWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hyman2006.instReprSenecaWord : Repr SenecaWord

Equations

• Hyman2006.instReprSenecaWord = { reprPrec := Hyman2006.instReprSenecaWord.repr }

def Hyman2006.instReprSenecaWord.repr : SenecaWord → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hyman2006.instReprSenecaWord.repr Hyman2006.SenecaWord.busy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2006.SenecaWord.busy")).group prec✝

def Hyman2006.SenecaWord.closed : SenecaWord → List Bool

Equations

• Hyman2006.SenecaWord.willing.closed = [false, false, false, true, true]
• Hyman2006.SenecaWord.busy.closed = [false, false, true, false, false, true, true]
• Hyman2006.SenecaWord.necktie.closed = [false, false, false, false, false, true]

def Hyman2006.seneca : Marking SenecaWord ℕ

Equations

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

theorem Hyman2006.seneca_willing : seneca.marked SenecaWord.willing = {3}

(23a): one H, obligatory and culminative for this word.

theorem Hyman2006.seneca_busy : seneca.marked SenecaWord.busy = {1, 5}

(23b): two H tones.

theorem Hyman2006.seneca_necktie : seneca.marked SenecaWord.necktie = ∅

(23c): no H, the footed syllables all open.

theorem Hyman2006.seneca_not_obligatory : ¬Obligatory seneca

theorem Hyman2006.seneca_not_culminative : ¬Culminative seneca

The cuts of Section 7

theorem Hyman2006.tableII : (Obligatory kinga ∧ Culminative kinga) ∧ (Obligatory creek ∧ ¬Culminative creek) ∧ (¬Obligatory tokyo ∧ Culminative tokyo) ∧ ¬Obligatory seneca ∧ ¬Culminative seneca

The four restricted-H systems of Table II attest every combination of the two criteria: no hierarchical typology can take one criterion as its first cut and the other as its second.

theorem Hyman2006.cuts_differ : (Obligatory creek ∧ ¬Obligatory tokyo) ∧ Culminative tokyo ∧ ¬Culminative creek

The most significant cut, by OBLHEAD, and the reviewer's alternative, by culminativity, sort Creek and Tokyo Japanese oppositely.