Kawahara (2015) [Kaw15]

The phonology of Japanese accent surveys 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. This file formalizes the survey's core generalizations — the Table 1 comparison of the antepenultimate accent rule ([McC68]) with the Latin Stress Rule ([Hay95a]), the accent-to-tone derivation and its culminativity (accentToTones_culminative), and NonFinality ([PS93]) in compound accent. The §6 affix accent lexicon lives in Fragments/Japanese/Prosody.lean.

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 ([Hay95a]). §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)

Tones are specified by the accentual HL and the initial rise, then spread rightward ((7)–(9)).

inductive Kawahara2015.LevelTone : Type

A level tone. Japanese distinguishes only H and L at the lexical level (§1.3).

• H : LevelTone
• L : LevelTone

@[instance_reducible]

instance Kawahara2015.instDecidableEqLevelTone : DecidableEq LevelTone

Equations

• Kawahara2015.instDecidableEqLevelTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kawahara2015.instReprLevelTone.repr : LevelTone → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Kawahara2015.instReprLevelTone : Repr LevelTone

Equations

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

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

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

Equations

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

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

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

Equations

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

def Kawahara2015.toneSpec (accentMora : Option ℕ) (i : ℕ) : Option 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 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 = [LevelTone.L, LevelTone.H, 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 = [LevelTone.H, LevelTone.L, 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 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 (Kawahara2015.LevelTone.H, Kawahara2015.LevelTone.L) (l.zip l.tail)

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

An L head opens no fall.

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

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

Every fall consumes an L strictly after the first position.

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

Stuttering a tone creates no fall.

theorem Kawahara2015.hlFallCount_cons_scanl (spec : List (Option LevelTone)) (x t : LevelTone) : hlFallCount (x :: List.scanl (fun (t : LevelTone) (o : Option 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 LevelTone.H else 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 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 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 : Constraints.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 = Constraints.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).