Kawahara (2015): The Phonology of Japanese Accent

This file formalizes the core generalizations of [Kaw15], a survey of Tokyo Japanese pitch accent: a single lexical accent per word determines the surface tone contour, and its location is predictable in loanwords, compounds, and affixed words. The Table 1 comparison of the antepenultimate accent rule ([McC68]) with the Latin Stress Rule ([Hay95b]) is decided on the eight trisyllabic weight profiles, the accent-to-tone derivation of Section 1.4 is proved culminative for every accent location and word length (accentToTones_culminative), and the compound accent rules of Section 4 never yield a final accent, the NonFinality of [PS93]. The affixes of Section 6 carry their effect on the root's accent, and the recessive and dominant classes are properties of that effect: no affix is both (Affix.Recessive.not_dominant), and the accent-shifting suffix is neither.

References

• [Kaw15]
• [McC68], [Hay95b], [PS93], [Kub06]

Default accent: the AAR vs the Latin Stress Rule

Language-neutral accent-placement rules over a syllable-weight profile, compared on loanword default accentuation (§2).

def Kawahara2015.defaultAccentAAR (weights : List Prosody.Syllable.Weight) : Option ℕ

The antepenultimate accent rule, which accents the syllable containing the antepenultimate mora and the initial syllable of shorter words ([McC68]). Returns the 0-indexed syllable.

Equations

• One or more equations did not get rendered due to their size.
• Kawahara2015.defaultAccentAAR [] = none

def Kawahara2015.latinStressRule (weights : List Prosody.Syllable.Weight) : Option ℕ

The Latin Stress Rule, which accents a heavy (≥ 2μ) penult and the antepenult otherwise, with mono- and disyllables accented initially ([Hay95b]). §2.3 reviews arguments that LSR-conforming variants occur even where the two rules diverge, making the LSR arguably the better characterization of the Japanese default.

Equations

• Kawahara2015.latinStressRule [] = none
• Kawahara2015.latinStressRule weights = some (weights.length - if Prosody.Syllable.Weight.heavy ≤ weights.reverse.getD 1 0 then 2 else 3)

def Kawahara2015.trisyllabicConditions : List (List Prosody.Syllable.Weight)

The eight trisyllabic weight conditions of Table 1.

Equations

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

theorem Kawahara2015.aar_lsr_mismatches : List.filter (fun (w : List Prosody.Syllable.Weight) => defaultAccentAAR w != latinStressRule w) trisyllabicConditions = [[Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy], [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy]]

The AAR and the LSR agree on six of the eight trisyllabic weight conditions and diverge exactly on HLH and LLH (Table 1).

theorem Kawahara2015.aar_lsr_mismatch_hlh : defaultAccentAAR [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 1 ∧ latinStressRule [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 0

On HLH the AAR accents σ₂, the syllable containing the antepenultimate mora, while the LSR accents the antepenult σ₁ since the penult is light (Table 1c: HL'H vs H'LH).

theorem Kawahara2015.aar_lsr_mismatch_llh : defaultAccentAAR [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 1 ∧ latinStressRule [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 0

On LLH the AAR accents σ₂ and the LSR σ₁ (Table 1g: LL'H vs L'LH).

Loanword accent (§2)

Loanwords lack lexical accent specifications, so their accentuation reveals the default pattern (§2.1; [Kub06]).

def Kawahara2015.lightProfile (e : Japanese.Prosody.ProsodicEntry) : List Prosody.Syllable.Weight

The weight profile of an all-light loanword — one light syllable per mora.

Equations

• Kawahara2015.lightProfile e = List.replicate e.nMorae Prosody.Syllable.Weight.light

def Kawahara2015.kurisumasu : Japanese.Prosody.ProsodicEntry

ku-ri-su'-ma-su 'Christmas', accented on the antepenultimate mora ((10a)).

Equations

• Kawahara2015.kurisumasu = { form := "kurisumasu", gloss := "Christmas", accentMora := some 2, nMorae := 5 }

def Kawahara2015.asufaruto : Japanese.Prosody.ProsodicEntry

a-su-fa'-ru-to 'asphalt', accented on the antepenultimate mora ((10g)).

Equations

• Kawahara2015.asufaruto = { form := "asufaruto", gloss := "asphalt", accentMora := some 2, nMorae := 5 }

def Kawahara2015.makudonarudo : Japanese.Prosody.ProsodicEntry

ma-ku-do-na'-ru-do 'McDonald', accented on the antepenultimate mora ((10h)).

Equations

• Kawahara2015.makudonarudo = { form := "makudonarudo", gloss := "McDonald's", accentMora := some 3, nMorae := 6 }

def Kawahara2015.amerika : Japanese.Prosody.ProsodicEntry

a.me.ri.ka 'America', unaccented as a four-mora word with two final light non-epenthetic syllables ((16a)).

Equations

• Kawahara2015.amerika = { form := "amerika", gloss := "America", accentMora := none, nMorae := 4 }

theorem Kawahara2015.loanwords_match_aar : defaultAccentAAR (lightProfile kurisumasu) = kurisumasu.accentMora ∧ defaultAccentAAR (lightProfile asufaruto) = asufaruto.accentMora ∧ defaultAccentAAR (lightProfile makudonarudo) = makudonarudo.accentMora

The accented loanwords of (10) carry the accent the AAR assigns.

theorem Kawahara2015.loanwords_match_lsr : latinStressRule (lightProfile kurisumasu) = kurisumasu.accentMora ∧ latinStressRule (lightProfile asufaruto) = asufaruto.accentMora ∧ latinStressRule (lightProfile makudonarudo) = makudonarudo.accentMora

On all-light profiles the LSR agrees with the AAR, so the (10) loanwords match it as well (§2.3).

theorem Kawahara2015.amerika_beyond_default_rules : defaultAccentAAR (lightProfile amerika) ≠ amerika.accentMora ∧ latinStressRule (lightProfile amerika) ≠ amerika.accentMora

Neither default rule derives amerika's unaccentedness, as neither produces unaccented outputs (§2.3 n. 10). Four-mora light-final unaccentedness is §2.4's separate generalization.

From accent to surface tones (§1.4)

Japanese lexically uses only the two level tones H and L (§1.3). Tones are specified by the accentual HL and the initial rise, then spread rightward ((7)–(9)).

def Kawahara2015.accentualHL (accentMora : Option ℕ) (i : ℕ) : Option Prosody.LevelTone

The accentual HL — H on the accented mora, L on its successor ((4)).

Equations

• Kawahara2015.accentualHL accentMora i = if accentMora = some i then some Prosody.LevelTone.H else if Option.map (fun (x : ℕ) => x + 1) accentMora = some i then some Prosody.LevelTone.L else none

def Kawahara2015.initialRise (i : ℕ) : Option Prosody.LevelTone

The initial rise — L on mora 0, H on mora 1 ((5)).

Equations

• Kawahara2015.initialRise i = if i = 0 then some Prosody.LevelTone.L else if i = 1 then some Prosody.LevelTone.H else none

def Kawahara2015.toneSpec (accentMora : Option ℕ) (i : ℕ) : Option Prosody.LevelTone

The tonal specification of mora i before spreading, with the accentual HL taking precedence over the initial rise ((5b)).

Equations

• Kawahara2015.toneSpec accentMora i = (Kawahara2015.accentualHL accentMora i).or (Kawahara2015.initialRise i)

def Kawahara2015.accentToTones (accentMora : Option ℕ) (nMorae : ℕ) : List Prosody.LevelTone

The surface tones of an nMorae-word from its accent position, by specification (toneSpec) followed by spreading — a left scan copying the most recent specified tone rightward ((7)–(9)). The seed is never consulted, since mora 0 is always specified.

Equations

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

theorem Kawahara2015.ameCandy_ga_tones : accentToTones Japanese.Prosody.ameCandy.accentMora 3 = [Prosody.LevelTone.L, Prosody.LevelTone.H, Prosody.LevelTone.H]

Unaccented ame(+ga) 'candy' surfaces LHH by initial rise and spreading ((6b)).

theorem Kawahara2015.ameRain_ga_tones : accentToTones Japanese.Prosody.ameRain.accentMora 3 = [Prosody.LevelTone.H, Prosody.LevelTone.L, Prosody.LevelTone.L]

Initially-accented a'me(+ga) 'rain' surfaces HLL, since the accentual HL blocks the initial rise ((5b), (8)).

theorem Kawahara2015.trisyllabic_tone_patterns : [accentToTones none 3, accentToTones (some 0) 3, accentToTones (some 1) 3].Nodup ∧ accentToTones none 3 = accentToTones (some 2) 3

Of the n+1 accent patterns of a trisyllable ((3)), the unaccented, initial, and medial contours are distinct, while final accent neutralizes with unaccentedness word-internally because the post-accent L falls off the word edge (§1.4).

Culminativity

"Japanese allows only one HL pitch fall within a word" (§1.4) — accentToTones_culminative derives this for every accent location and word length.

def Kawahara2015.hlFallCount (l : List Prosody.LevelTone) : ℕ

The number of H-to-L falls in a tone string — the occurrences of (H, L) among adjacent pairs.

Equations

• Kawahara2015.hlFallCount l = List.count (Prosody.LevelTone.H, Prosody.LevelTone.L) (l.zip l.tail)

theorem Kawahara2015.hlFallCount_L_cons (l : List Prosody.LevelTone) : hlFallCount (Prosody.LevelTone.L :: l) = hlFallCount l

An L head opens no fall.

theorem Kawahara2015.hlFallCount_cons_cons (t u : Prosody.LevelTone) (l : List Prosody.LevelTone) : hlFallCount (t :: u :: l) = hlFallCount (u :: l) + if t = Prosody.LevelTone.H ∧ u = Prosody.LevelTone.L then 1 else 0

theorem Kawahara2015.hlFallCount_le_count_tail (l : List Prosody.LevelTone) : hlFallCount l ≤ List.count Prosody.LevelTone.L l.tail

Every fall consumes an L strictly after the first position.

theorem Kawahara2015.hlFallCount_cons_self (t : Prosody.LevelTone) (l : List Prosody.LevelTone) : hlFallCount (t :: t :: l) = hlFallCount (t :: l)

Stuttering a tone creates no fall.

theorem Kawahara2015.hlFallCount_cons_scanl (spec : List (Option Prosody.LevelTone)) (x t : Prosody.LevelTone) : hlFallCount (x :: List.scanl (fun (t : Prosody.LevelTone) (o : Option Prosody.LevelTone) => o.getD t) t spec) = hlFallCount (x :: t :: spec.reduceOption)

Spreading is fall-invariant, since copying a tone neither creates nor destroys an HL fall.

theorem Kawahara2015.toneSpec_zero (a : Option ℕ) : toneSpec a 0 = some (if a = some 0 then Prosody.LevelTone.H else Prosody.LevelTone.L)

Mora 0 is always specified, as H under initial accent and otherwise as the initial-rise L.

theorem Kawahara2015.toneSpec_eq_L {a : Option ℕ} {j : ℕ} (hj : 1 ≤ j) : toneSpec a j = some Prosody.LevelTone.L ↔ Option.map (fun (x : ℕ) => x + 1) a = some j

After mora 0, the only source of a specified L is the post-accent L, which pins the accent location.

theorem Kawahara2015.count_L_toneSpec_dense (a : Option ℕ) (l : List ℕ) (hnd : l.Nodup) (hpos : ∀ j ∈ l, 1 ≤ j) : List.count Prosody.LevelTone.L (List.filterMap (toneSpec a) l) ≤ 1

The specified tones after mora 0 contain at most one L, since the post-accent L pins the accent location and positions are distinct.

theorem Kawahara2015.accentToTones_culminative (a : Option ℕ) (n : ℕ) : hlFallCount (accentToTones a n) ≤ 1

A word carries at most one HL fall, whatever its accent location and length (culminativity, §1.4).

Compound accent (§4)

The traditional dichotomy by N2 length: short N2s (≤ 2μ) either retain accent or pre-accent the N1-final position; long N2s (≥ 3μ) take N2-initial accent unless their own accent is nonfinal. Both rules are stated over mora counts; the paper's rules target syllables, and the two coincide on the light-syllable data of (21)–(24) formalized below.

def Kawahara2015.shortN2Retain (n1Morae : ℕ) (n2Accent : Option ℕ) : Option ℕ

A retaining short N2 keeps its own accent, shifted into the compound (§4.1, (21)).

Equations

• Kawahara2015.shortN2Retain n1Morae n2Accent = Option.map (fun (x : ℕ) => n1Morae + x) n2Accent

def Kawahara2015.shortN2PreAccent (n1Morae : ℕ) : Option ℕ

A pre-accenting short N2 accents the N1-final mora — the partial predecessor of N1's length — its own accent lost to NonFinality (§4.1, (22)).

Equations

• Kawahara2015.shortN2PreAccent n1Morae = n1Morae.ppred

def Kawahara2015.longN2CompoundAccent (n1Morae n2Morae : ℕ) (n2Accent : Option ℕ) : Option ℕ

The compound accent under a long (≥ 3μ) N2, which receives N2-initial accent when unaccented or finally-accented and otherwise retains its own accent (§4.2).

Equations

• Kawahara2015.longN2CompoundAccent n1Morae n2Morae n2Accent = some (n1Morae + (Option.filter (fun (x : ℕ) => x + 1 != n2Morae) n2Accent).getD 0)

def Kawahara2015.nonFinality : OptimalityTheory.Constraint (Option ℕ × ℕ)

The NonFinality constraint over an (accent, mora count) pair, violated once when the accent sits on the final mora ([PS93]; §4.1 invokes it for the loss of final accent in compounds).

Equations

• Kawahara2015.nonFinality = OptimalityTheory.Constraint.binary fun (an : Option ℕ × ℕ) => Option.map (fun (x : ℕ) => x + 1) an.1 = some an.2

theorem Kawahara2015.faasuto_kisu_compound : shortN2Retain 4 (some 0) = some 4

In fa'asuto+ki'su → faasuto+ki'su 'first kiss', the short N2 retains its accent on ki ((21a)).

theorem Kawahara2015.kabuto_musi_compound : shortN2PreAccent 3 = some 2

In ka'buto+musi → kabuto'+musi 'beetle', the pre-accenting short N2 puts the accent on N1-final to ((22a)).

theorem Kawahara2015.sin_yokohama_compound : longN2CompoundAccent 2 4 none = some 2

In si'n+yokohama → sin+yo'kohama 'Shin-Yokohama', the unaccented long N2 receives N2-initial accent ((23a)).

theorem Kawahara2015.sin_tamanegi_compound : longN2CompoundAccent 2 4 (some 2) = some 4

In si'n+tamane'gi → sin+tamane'gi 'new onion', the long N2 retains its nonfinal accent ((24a)).

@[simp]

theorem Kawahara2015.nonFinality_eq_zero {acc : Option ℕ} {n : ℕ} : nonFinality (acc, n) = 0 ↔ Option.map (fun (x : ℕ) => x + 1) acc ≠ some n

nonFinality is satisfied exactly when the accent's successor is not the mora count.

theorem Kawahara2015.shortN2_preaccent_nonfinal (n1Morae n2Morae : ℕ) (h : 1 ≤ n2Morae) : nonFinality (shortN2PreAccent n1Morae, n1Morae + n2Morae) = 0

Short-N2 pre-accenting never yields final accent, since the new accent lands on the N1-final position and N2 intervenes (§4.1).

theorem Kawahara2015.longN2_nonfinal (n1Morae n2Morae : ℕ) (n2Accent : Option ℕ) (h2 : 3 ≤ n2Morae) : nonFinality (longN2CompoundAccent n1Morae n2Morae n2Accent, n1Morae + n2Morae) = 0

Long-N2 compound accent never yields final accent, since retention is filtered to N2-nonfinal accents and the N2-initial default is nonfinal in a trimoraic-or-longer N2 (§4.2).

Affix accent (§6)

Section 6 describes each affix by what it does to an unaccented root and to an accented one. A recessive affix acts only on unaccented roots, so an accented root keeps its accent; a dominant affix acts the same way whatever the root's accent. Each affix below carries its effect, the affixed word's accent as a function of the root's, and both classes are properties of that function.

An accented root keeps its accent on its own syllable, as the nominal roots of (31e–h) do. Verbs contrast only accented against unaccented, and their inflection places the accent (§5), so the accented verb roots of (29e–g) surface with the accent elsewhere; that placement is not modelled.

inductive Kawahara2015.Locus : Type

The accented syllable of an affixed word: the root's i-th syllable, or the affix's own accented syllable.

• root (i : ℕ) : Locus
• affix : Locus

@[instance_reducible]

instance Kawahara2015.instDecidableEqLocus : DecidableEq Locus

Equations

• Kawahara2015.instDecidableEqLocus = Kawahara2015.instDecidableEqLocus.decEq

def Kawahara2015.instDecidableEqLocus.decEq (x✝ x✝¹ : Locus) : Decidable (x✝ = x✝¹)

Equations

• Kawahara2015.instDecidableEqLocus.decEq (Kawahara2015.Locus.root a) (Kawahara2015.Locus.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Kawahara2015.instDecidableEqLocus.decEq (Kawahara2015.Locus.root i) Kawahara2015.Locus.affix = isFalse ⋯
• Kawahara2015.instDecidableEqLocus.decEq Kawahara2015.Locus.affix (Kawahara2015.Locus.root i) = isFalse ⋯
• Kawahara2015.instDecidableEqLocus.decEq Kawahara2015.Locus.affix Kawahara2015.Locus.affix = isTrue ⋯

def Kawahara2015.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Kawahara2015.instReprLocus : Repr Locus

Equations

• Kawahara2015.instReprLocus = { reprPrec := Kawahara2015.instReprLocus.repr }

structure Kawahara2015.Affix : Type

An affix with its accentual effect: the accent of the affixed word (none if it is unaccented), given a root of n + 1 syllables and the root's accented syllable (none if the root is unaccented).

• form : String
• gloss : String
• accent (n : ℕ) : Option (Fin (n + 1)) → Option Locus

def Kawahara2015.Affix.Recessive (x : Affix) : Prop

A recessive affix leaves an accented root's accent where it is.

Equations

• x.Recessive = ∀ (n : ℕ) (i : Fin (n + 1)), x.accent n (some i) = some (Kawahara2015.Locus.root ↑i)

def Kawahara2015.Affix.Dominant (x : Affix) : Prop

A dominant affix gives the same accent whatever the root's accent.

Equations

• x.Dominant = ∀ (n : ℕ) (a b : Option (Fin (n + 1))), x.accent n a = x.accent n b

theorem Kawahara2015.Affix.Recessive.not_dominant {x : Affix} (h : x.Recessive) : ¬x.Dominant

No affix is both recessive and dominant: on a root of two syllables, keeping either accent in place gives two different words.

def Kawahara2015.taraSuffix : Affix

The recessive conditional suffix /+ta'ra/: accented on unaccented roots, losing its accent to an accented root ((29)).

Equations

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

def Kawahara2015.ppoiSuffix : Affix

The dominant suffix /+ppo'i/ '-ish', which keeps its accent and deletes the root's ((30)).

Equations

• Kawahara2015.ppoiSuffix = { form := "-ppo'i", gloss := "-ish", accent := fun (x : ℕ) (x_1 : Option (Fin (x + 1))) => some Kawahara2015.Locus.affix }

def Kawahara2015.siSuffix : Affix

The recessive pre-accenting suffix /+si/ 'Mr.', which accents the root-final syllable of an unaccented root only ((31)).

Equations

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

def Kawahara2015.keSuffix : Affix

The dominant pre-accenting suffix /+'ke/ 'family of', which accents the root-final syllable of every root ((32)).

Equations

• Kawahara2015.keSuffix = { form := "-ke", gloss := "family of", accent := fun (n : ℕ) (x : Option (Fin (n + 1))) => some (Kawahara2015.Locus.root n) }

def Kawahara2015.monoSuffix : Affix

The accent-shifting suffix /+mono/ 'thing', which moves an accented root's accent to the root-final syllable and leaves an unaccented root unaccented ((33)).

Equations

• Kawahara2015.monoSuffix = { form := "-mono", gloss := "thing", accent := fun (n : ℕ) (a : Option (Fin (n + 1))) => Option.map (fun (x : Fin (n + 1)) => Kawahara2015.Locus.root n) a }

def Kawahara2015.oPrefix : Affix

The post-accenting honorific prefix /o+/, which accents the syllable after it, the root-initial one, whatever the root's accent ((34)).

Equations

• Kawahara2015.oPrefix = { form := "o-", gloss := "honorific", accent := fun (x : ℕ) (x_1 : Option (Fin (x + 1))) => some (Kawahara2015.Locus.root 0) }

def Kawahara2015.tekiSuffix : Affix

The deaccenting suffix /+teki/ '-like', which leaves the word unaccented ((36)).

Equations

• Kawahara2015.tekiSuffix = { form := "-teki", gloss := "-like", accent := fun (x : ℕ) (x_1 : Option (Fin (x + 1))) => none }

def Kawahara2015.zuSuffix : Affix

The group-name suffix /+zu/, which accents the root-initial syllable. The roots in (39) are all unaccented; the text states the root-initial accent without condition.

Equations

• Kawahara2015.zuSuffix = { form := "-zu", gloss := "group", accent := fun (x : ℕ) (x_1 : Option (Fin (x + 1))) => some (Kawahara2015.Locus.root 0) }

theorem Kawahara2015.taraSuffix_recessive : taraSuffix.Recessive

theorem Kawahara2015.siSuffix_recessive : siSuffix.Recessive

theorem Kawahara2015.ppoiSuffix_dominant : ppoiSuffix.Dominant

theorem Kawahara2015.keSuffix_dominant : keSuffix.Dominant

theorem Kawahara2015.oPrefix_dominant : oPrefix.Dominant

theorem Kawahara2015.tekiSuffix_dominant : tekiSuffix.Dominant

theorem Kawahara2015.zuSuffix_dominant : zuSuffix.Dominant

theorem Kawahara2015.monoSuffix_not_recessive_not_dominant : ¬monoSuffix.Recessive ∧ ¬monoSuffix.Dominant

The accent-shifting suffix is neither recessive nor dominant: it acts only on accented roots, the mirror image of a recessive affix.