Hayes (1989): Compensatory Lengthening in Moraic Phonology

[Hay89]

Bruce Hayes. "Compensatory Lengthening in Moraic Phonology." Linguistic Inquiry 20(2): 253–306.

This study file formalizes the empirical core of Hayes 1989: the typology of compensatory lengthening (CL) and its three central arguments for moraic theory over segmental prosodic theories (X theory, CV theory).

Core claims formalized

1. CL is governed by a prosodic frame provided by moraic structure (not by constraints on association line rearrangements).

2. Onset-deletion asymmetry: CL from coda deletion is common; CL from onset deletion is unattested. Moraic theory derives this from the universal non-moraicity of onsets — onset deletion strands no μ (Syllable.deleteOnset_strandedCount).

3. Weight prerequisite: CL occurs only in languages with a syllable-weight distinction. Only languages with bimoraic syllables (Syllable.ofCV … wbp) have a coda μ to strand.

4. Moraic conservation: CL conserves total mora count. Because a stranded μ survives deletion, this follows from Syllable.strand_moraCount / Syllable.relicense_moraCount rather than stipulation.

Languages covered

• Latin (s-deletion: kasnus → ka:nus; onset s-deletion: smereo → mereo)
• Middle English (vowel loss: talə → ta:l)
• Lardil (no WBP: CL impossible)
• Estonian (trimoraic syllables, Q1/Q2/Q3 quantity system)

The CL typology ([Hay89])

inductive Hayes1989.CLType : Type

The seven attested compensatory-lengthening types ([Hay89]). Each is a deletion trigger plus a re-association target; all share the moraic mechanism — deletion strands a mora, which is then re-associated to an adjacent segment (the substrate Syllable.strand ∘ relicense/relicenseLeft).

• classical : CLType

  Vowel lengthens when a following coda consonant deletes (Latin kasnus → kaːnus).

• totalAssimilation : CLType

  Total consonant assimilation, formally equivalent to CL (asta → atta).

• glideFormation : CLType

  Glide formation frees a mora that lengthens a neighbour (tia → tyaː).

• prenasalization : CLType

  Prenasalization absorbs a mora from the following stop (Bantu amba → aːmba).

• doubleFlop : CLType

  Non-adjacent CL via double flop (Ancient Greek odwos → oːdos).

• vowelLoss : CLType

  A following vowel deletes; the preceding vowel lengthens (Middle English talə → taːl).

• inverseCL : CLType

  A vowel shortens, lengthening the following consonant (Luganda aika → akka).

@[implicit_reducible]

instance Hayes1989.instDecidableEqCLType : DecidableEq CLType

Equations

• Hayes1989.instDecidableEqCLType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hayes1989.instReprCLType : Repr CLType

Equations

• Hayes1989.instReprCLType = { reprPrec := Hayes1989.instReprCLType.repr }

def Hayes1989.instReprCLType.repr : CLType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hayes1989.instReprCLType.repr Hayes1989.CLType.classical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.CLType.classical")).group prec✝
• Hayes1989.instReprCLType.repr Hayes1989.CLType.doubleFlop prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.CLType.doubleFlop")).group prec✝
• Hayes1989.instReprCLType.repr Hayes1989.CLType.vowelLoss prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.CLType.vowelLoss")).group prec✝
• Hayes1989.instReprCLType.repr Hayes1989.CLType.inverseCL prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.CLType.inverseCL")).group prec✝

inductive Hayes1989.Locality : Type

Whether a CL type re-associates the stranded μ within one syllable (Syllable.relicense) or moves it across a syllable boundary (Syllable.relicenseLeft).

• tautosyllabic : Locality
• heterosyllabic : Locality

@[implicit_reducible]

instance Hayes1989.instDecidableEqLocality : DecidableEq Locality

Equations

• Hayes1989.instDecidableEqLocality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hayes1989.instReprLocality.repr : Locality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hayes1989.instReprLocality : Repr Locality

Equations

• Hayes1989.instReprLocality = { reprPrec := Hayes1989.instReprLocality.repr }

def Hayes1989.CLType.locality : CLType → Locality

The locality of each attested CL type ([Hay89]): vowel loss and the double flop strand a μ that a next-syllable vowel picks up; the rest re-link within the deletion's own syllable.

Equations

• Hayes1989.CLType.vowelLoss.locality = Hayes1989.Locality.heterosyllabic
• Hayes1989.CLType.doubleFlop.locality = Hayes1989.Locality.heterosyllabic
• Hayes1989.CLType.classical.locality = Hayes1989.Locality.tautosyllabic
• Hayes1989.CLType.totalAssimilation.locality = Hayes1989.Locality.tautosyllabic
• Hayes1989.CLType.glideFormation.locality = Hayes1989.Locality.tautosyllabic
• Hayes1989.CLType.prenasalization.locality = Hayes1989.Locality.tautosyllabic
• Hayes1989.CLType.inverseCL.locality = Hayes1989.Locality.tautosyllabic

Segment inventory (minimal, for derivations)

Latin s-deletion — classical CL

def Hayes1989.kasnus_σ₁ : Prosody.Syllable

Latin underlying form *kasnus 'gray': σ₁ = ⟨kas⟩ — onset ⟨k⟩, a nucleus μ, and a coda ⟨s⟩ μ (Weight-by-Position), making σ₁ heavy.

Equations

• Hayes1989.kasnus_σ₁ = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.s✝] Hayes1989.kasnus_σ₁._proof_1

def Hayes1989.kasnus_σ₂ : Prosody.Syllable

Equations

• Hayes1989.kasnus_σ₂ = Prosody.Syllable.ofMorae [Hayes1989.n✝] [Prosody.Mora.of Hayes1989.u✝, Prosody.Mora.of Hayes1989.s✝] Hayes1989.kasnus_σ₂._proof_1

def Hayes1989.kasnus : List Prosody.Syllable

Equations

• Hayes1989.kasnus = [Hayes1989.kasnus_σ₁, Hayes1989.kasnus_σ₂]

theorem Hayes1989.kasnus_σ₁_heavy : kasnus_σ₁.weight = Prosody.Syllable.Weight.heavy

σ₁ of *kasnus is heavy (2 morae: nucleus + coda with WBP).

theorem Hayes1989.kasnus_s_deletion_strands : (kasnus_σ₁.strand 1).strandedCount = 1

Deleting the coda ⟨s⟩ from σ₁ strands one mora.

def Hayes1989.kaanus_σ₁ : Prosody.Syllable

After spreading, the vowel ⟨a⟩ becomes long: σ₁ = [ka:] with 2 morae.

Equations

• Hayes1989.kaanus_σ₁ = (Hayes1989.kasnus_σ₁.strand 1).relicense

theorem Hayes1989.kaanus_σ₁_heavy : kaanus_σ₁.weight = Prosody.Syllable.Weight.heavy

theorem Hayes1989.kasnus_conservation : kasnus_σ₁.moraCount = kaanus_σ₁.moraCount

Moraic conservation: *kasnus σ₁ and ka:nus σ₁ have the same mora count — derived from the general stranding/spreading conservation lemmas.

def Hayes1989.kosmis_σ₁ : Prosody.Syllable

Latin *kosmis → ko:mis 'courteous': same pattern.

Equations

• Hayes1989.kosmis_σ₁ = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.o✝, Prosody.Mora.of Hayes1989.s✝] Hayes1989.kosmis_σ₁._proof_1

theorem Hayes1989.kosmis_conservation : kosmis_σ₁.moraCount = (kosmis_σ₁.strand 1).relicense.moraCount

Latin word-initial s-deletion — no CL

def Hayes1989.smereo_σ₁ : Prosody.Syllable

Latin *smereo → mereo: ⟨s⟩ deletes word-initially (onset position). Onset ⟨s⟩ bears no mora, so no CL occurs.

Equations

• Hayes1989.smereo_σ₁ = Prosody.Syllable.ofMorae [Hayes1989.s✝] [Prosody.Mora.of Hayes1989.e✝] Hayes1989.smereo_σ₁._proof_1

theorem Hayes1989.smereo_onset_no_cl : (smereo_σ₁.deleteOnset 0).strandedCount = smereo_σ₁.strandedCount

Onset deletion strands no mora — the onset-deletion asymmetry.

theorem Hayes1989.smereo_remains_light : (smereo_σ₁.deleteOnset 0).weight = Prosody.Syllable.Weight.light

The mora count after onset deletion is still 1 (light syllable).

Middle English vowel-loss CL

def Hayes1989.tale_σ₁ : Prosody.Syllable

Middle English ⟨talə⟩ 'tale' (original disyllabic form): σ₁ = ⟨ta⟩ (open, light), σ₂ = ⟨lə⟩ (open, light). When word-final schwa deletes, Parasitic Delinking strands a mora, filled by leftward spreading that lengthens ⟨a⟩.

Equations

• Hayes1989.tale_σ₁ = Prosody.Syllable.ofMorae [Hayes1989.t✝] [Prosody.Mora.of Hayes1989.a✝] Hayes1989.tale_σ₁._proof_1

def Hayes1989.tale_σ₂ : Prosody.Syllable

Equations

• Hayes1989.tale_σ₂ = Prosody.Syllable.ofMorae [Hayes1989.l✝] [Prosody.Mora.of Hayes1989.e✝] Hayes1989.smereo_σ₁._proof_1

def Hayes1989.tale_input : List Prosody.Syllable

Equations

• Hayes1989.tale_input = [Hayes1989.tale_σ₁, Hayes1989.tale_σ₂]

theorem Hayes1989.tale_input_morae : (Prosody.Yield.ofSyllables tale_input).moraCount = 2

Input ⟨talə⟩ has 2 total morae (one per syllable).

theorem Hayes1989.tale_schwa_strands : (tale_σ₂.strand 0).strandedCount = 1

Deleting σ₂'s schwa strands one mora.

theorem Hayes1989.tale_migrate_lengthens_σ₁ : (tale_σ₁.relicenseLeft (tale_σ₂.strand 0)).1.weight = Prosody.Syllable.Weight.heavy

Vowel loss is heterosyllabic CL (CLType.vowelLoss): Parasitic Delinking deletes the de-nucleated σ₂ (its nucleus mora is stranded by Schwa Drop), and that mora migrates left onto σ₁, lengthening ⟨a⟩ to ⟨a:⟩ so σ₁ becomes heavy.

theorem Hayes1989.tale_vowel_loss_conserves : (tale_σ₁.relicenseLeft (tale_σ₂.strand 0)).1.moraCount + (Option.map Prosody.Syllable.moraCount (tale_σ₁.relicenseLeft (tale_σ₂.strand 0)).2).getD 0 = tale_σ₁.moraCount + (tale_σ₂.strand 0).moraCount

The migration conserves total weight — derived from Syllable.relicenseLeft_conserves, not a stipulated output: the de-nucleated σ₂ deletes (none) and its mora is gained by σ₁.

def Hayes1989.tale_output : Prosody.Syllable

CL result: ⟨a⟩ becomes long and ⟨l⟩ resyllabifies as a non-moraic coda riding on the second mora. Output σ = [ta:l] with 2 morae.

Equations

• Hayes1989.tale_output = Prosody.Syllable.ofMorae [Hayes1989.t✝] [Prosody.Mora.of Hayes1989.a✝, { dominates := [Hayes1989.a✝, Hayes1989.l✝] }] Hayes1989.tale_output._proof_1

theorem Hayes1989.tale_conservation : (Prosody.Yield.ofSyllables tale_input).moraCount = tale_output.moraCount

Conservation: input total morae = output morae.

Weight prerequisite — CL requires bimoraic syllables

def Hayes1989.lardil_cvc : Prosody.Syllable

Without WBP (e.g. Lardil), Syllable.ofCV leaves the coda non-moraic (riding on the nucleus μ). There is no coda μ to strand → no CL.

Equations

• Hayes1989.lardil_cvc = Prosody.Syllable.ofCV [Hayes1989.t✝] [Hayes1989.a✝] [Hayes1989.k✝] false Hayes1989.lardil_cvc._proof_1

theorem Hayes1989.lardil_cvc_is_light : lardil_cvc.weight = Prosody.Syllable.Weight.light

theorem Hayes1989.lardil_no_cl_from_coda : (lardil_cvc.strand 1).strandedCount = 0

def Hayes1989.latin_cvc : Prosody.Syllable

With WBP (e.g. Latin), Syllable.ofCV gives the coda its own mora. Stranding it strands one mora → CL is possible.

Equations

• Hayes1989.latin_cvc = Prosody.Syllable.ofCV [Hayes1989.t✝] [Hayes1989.a✝] [Hayes1989.k✝] true Hayes1989.lardil_cvc._proof_1

theorem Hayes1989.latin_cvc_is_heavy : latin_cvc.weight = Prosody.Syllable.Weight.heavy

theorem Hayes1989.latin_cl_from_coda : (latin_cvc.strand 1).strandedCount = 1

theorem Hayes1989.weight_determines_cl : (latin_cvc.strand 1).strandedCount ≠ (lardil_cvc.strand 1).strandedCount

The weight prerequisite: Latin (CL possible) vs Lardil (CL impossible) is exactly the WBP parameter.

Estonian trimoraic syllables

def Hayes1989.estonian_q1 : Prosody.Syllable

Estonian Q1/Q2/Q3 (short/long/overlong) syllables realize the three-way weight distinction as 1μ/2μ/3μ directly — a long vowel is two morae, an overlong rime three.

Equations

• Hayes1989.estonian_q1 = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.a✝] Hayes1989.tale_σ₁._proof_1

def Hayes1989.estonian_q2 : Prosody.Syllable

Equations

• Hayes1989.estonian_q2 = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.a✝] Hayes1989.estonian_q2._proof_1

def Hayes1989.estonian_q3 : Prosody.Syllable

Equations

• Hayes1989.estonian_q3 = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.l✝] Hayes1989.estonian_q3._proof_1

theorem Hayes1989.q1_is_light : estonian_q1.weight = Prosody.Syllable.Weight.light

theorem Hayes1989.q2_is_heavy : estonian_q2.weight = Prosody.Syllable.Weight.heavy

theorem Hayes1989.q3_is_superheavy : estonian_q3.weight = Prosody.Syllable.Weight.superheavy

theorem Hayes1989.q3_to_q2_loses_one_mora : estonian_q3.moraCount = estonian_q2.moraCount + 1

Q3 → Q2 grade shift: removing the third mora.

def Hayes1989.paat_ti_q3 : Prosody.Syllable

Estonian gemination loss: Q3 ⟨pa:t.ti⟩ → Q2 ⟨pa:.ti⟩; σ₁ goes from 3μ to 2μ as the geminate loses its mora.

Equations

• Hayes1989.paat_ti_q3 = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.t✝] Hayes1989.paat_ti_q3._proof_1

def Hayes1989.paa_ti_q2 : Prosody.Syllable

Equations

• Hayes1989.paa_ti_q2 = Prosody.Syllable.ofMorae [Hayes1989.k✝] [Prosody.Mora.of Hayes1989.a✝, Prosody.Mora.of Hayes1989.a✝] Hayes1989.estonian_q2._proof_1

theorem Hayes1989.gemination_loss_removes_mora : paat_ti_q3.moraCount = paa_ti_q2.moraCount + 1

Integration — the prosodic pipeline

def Hayes1989.kaanus_form : List Prosody.Syllable

The full pipeline for Latin ka:nus after CL: moraic syllables → weight profile → prosodic word. σ₁ = [ka:] (heavy), σ₂ = [nus] (heavy), so the weight profile is [H, H].

Equations

• Hayes1989.kaanus_form = [Hayes1989.kaanus_σ₁, Hayes1989.kasnus_σ₂]

theorem Hayes1989.kaanus_weight_profile : Prosody.Yield.ofSyllables kaanus_form = [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy]

CL output has the weight profile [heavy, heavy].

theorem Hayes1989.kaanus_satisfies_minword : (Prosody.Yield.ofSyllables kaanus_form).satisfiesMinWord

CL output satisfies the bimoraic minimal-word constraint (4μ ≥ 2μ).

theorem Hayes1989.tale_minword_preserved : (Prosody.Yield.ofSyllables tale_input).satisfiesMinWord ∧ (Prosody.Yield.ofSyllables [tale_output]).satisfiesMinWord

Middle English: CL preserves the bimoraic minimum across syllable restructuring. Input ⟨talə⟩ = [L, L] (2μ); output [ta:l] = [H] (2μ). Both satisfy the bimoraic minimum — a consequence of moraic conservation.