Compensatory Lengthening in Moraic Theory

Compensatory lengthening (CL) as the filling of stranded morae following segment deletion. This module formalizes the core theoretical claims of @cite{hayes-1989}:

1. Moraic Conservation: CL processes conserve total mora count. Deletion strands a mora; spreading fills it.

2. Onset Deletion Asymmetry: CL does not compensate for loss of onset consonants, because onsets are universally non-moraic.

3. Weight Prerequisite: CL occurs only in languages with a syllable weight distinction (bimoraic syllables), because only such languages have morae that can be stranded.

The CL typology classifies seven attested CL types, all derivable from moraic representations without stipulating constraints on association line rearrangements.

@cite{hayes-1989}

inductive Phonology.Moraic.CL.CLType : Type

The typology of compensatory lengthening processes (@cite{hayes-1989}, §5.1).

Each type is defined by the deletion trigger and the spreading target. All types share the core mechanism: deletion strands a mora, which is then filled by spreading from an adjacent segment.

• classical : CLType

  Vowel lengthens when a following coda consonant deletes. Example: Latin *kasnus → ka:nus.

• totalAssimilation : CLType

  Total assimilation of a consonant, formally equivalent to CL. Example: asta → [atta] (progressive), asta → [assa] (regressive).

• glideFormation : CLType

  Glide formation shortens a vowel, freeing a mora that lengthens an adjacent segment. Example: tia → [tya:].

• prenasalization : CLType

  Prenasalization absorbs a mora from the following stop. Example: Bantu amba → [a: m̌ba].

• doubleFlop : CLType

  Non-adjacent CL via double flop. Deletion causes resyllabification, which strands a mora accessible to a non-adjacent vowel. Example: Ancient Greek *odwos → o:dos.

• vowelLoss : CLType

  Vowel in the following syllable deletes; the preceding vowel lengthens via Parasitic Delinking. Example: Middle English talə → [ta:l].

• inverseCL : CLType

  A vowel deletes or shortens, with concomitant lengthening of the following consonant. Example: Luganda aika → [akka].

@[implicit_reducible]

instance Phonology.Moraic.CL.instDecidableEqCLType : DecidableEq CLType

Equations

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

@[implicit_reducible]

instance Phonology.Moraic.CL.instReprCLType : Repr CLType

Equations

• Phonology.Moraic.CL.instReprCLType = { reprPrec := Phonology.Moraic.CL.instReprCLType.repr }

def Phonology.Moraic.CL.instReprCLType.repr : CLType → ℕ → Std.Format

Equations

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

def Phonology.Moraic.CL.deleteMoraic (σ : MoraicSyllable) (idx : ℕ) : MoraicSyllable × ℕ

Delete a segment from a moraic syllable at a given index in the moraic tier. Returns the modified syllable and the number of stranded morae.

Following @cite{hayes-1989} §3: deletion on the segmental tier only — the mora remains, becoming segmentally unaffiliated.

Equations

• Phonology.Moraic.CL.deleteMoraic σ idx = match σ.moraic[idx]? with | some ms => ({ onset := σ.onset, moraic := σ.moraic.eraseIdx idx }, ms.morae.toNat) | none => (σ, 0)

def Phonology.Moraic.CL.deleteOnset (σ : MoraicSyllable) (idx : ℕ) : MoraicSyllable

Delete an onset consonant from a moraic syllable. Returns the modified syllable. No morae are stranded because onsets are non-moraic.

Equations

• Phonology.Moraic.CL.deleteOnset σ idx = { onset := σ.onset.eraseIdx idx, moraic := σ.moraic }

inductive Phonology.Moraic.CL.SpreadDir : Type

Direction of spreading to fill a stranded mora.

• left : SpreadDir

  Spread from the left: the preceding segment acquires the stranded mora. This is the typical case for classical CL and vowel loss CL.

• right : SpreadDir

  Spread from the right: the following segment acquires the stranded mora. This is the typical case for inverse CL.

@[implicit_reducible]

instance Phonology.Moraic.CL.instDecidableEqSpreadDir : DecidableEq SpreadDir

Equations

• Phonology.Moraic.CL.instDecidableEqSpreadDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.Moraic.CL.instReprSpreadDir : Repr SpreadDir

Equations

• Phonology.Moraic.CL.instReprSpreadDir = { reprPrec := Phonology.Moraic.CL.instReprSpreadDir.repr }

def Phonology.Moraic.CL.instReprSpreadDir.repr : SpreadDir → ℕ → Std.Format

Equations

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

def Phonology.Moraic.CL.spreadToFill (σ : MoraicSyllable) (strandedMorae : ℕ) (dir : SpreadDir) : MoraicSyllable

Apply spreading to fill stranded morae in a moraic syllable.

Following @cite{hayes-1989}: CL is part of syllabification. When a mora is stranded, syllabification principles fill it by spreading from the nearest available segment. The direction of spreading is language-specific (part of the syllabification algorithm).

Handles 1 or 2 stranded morae (geminate deletion).

Equations

• One or more equations did not get rendered due to their size.
• Phonology.Moraic.CL.spreadToFill σ strandedMorae dir✝ = if (strandedMorae == 0) = true then σ else σ

theorem Phonology.Moraic.CL.onset_deletion_no_stranding (σ : MoraicSyllable) (idx : ℕ) : (deleteOnset σ idx).moraCount = σ.moraCount

Onset Deletion Asymmetry (@cite{hayes-1989}, §5.2.1): Deleting an onset consonant strands zero morae, because onset consonants are universally non-moraic.

This follows directly from the representation: onsets are List Segment with no mora association. There is nothing to strand.

This is the strongest theorem in the formalization — fully general over all syllables and all onset indices. It is derived from the representation, not stipulated.

theorem Phonology.Moraic.CL.moraic_conservation_left (v c : Segment) : have σ := { onset := [], moraic := [{ seg := v, morae := MoraCount.one }, { seg := c, morae := MoraCount.one }] }; match deleteMoraic σ 1 with | (σ_del, stranded) => σ.moraCount = (spreadToFill σ_del stranded SpreadDir.left).moraCount

Moraic Conservation for single-mora CL (@cite{hayes-1989}, Rule (64)): Deleting a monomoraic segment and spreading left preserves total morae.

theorem Phonology.Moraic.CL.moraic_conservation_right (v c : Segment) : have σ := { onset := [], moraic := [{ seg := v, morae := MoraCount.one }, { seg := c, morae := MoraCount.one }] }; match deleteMoraic σ 0 with | (σ_del, stranded) => σ.moraCount = (spreadToFill σ_del stranded SpreadDir.right).moraCount

Moraic conservation also holds for rightward spreading (inverse CL).

theorem Phonology.Moraic.CL.no_wbp_no_cl (v c₁ c₂ : Segment) : (deleteMoraic { onset := [c₁], moraic := [{ seg := v, morae := MoraCount.one }, { seg := c₂, morae := MoraCount.zero }] } 1).snd = 0

Weight prerequisite (@cite{hayes-1989}, §6): deleting a non-moraic coda (WBP inactive) strands zero morae. No CL is possible.

theorem Phonology.Moraic.CL.wbp_strands_mora (v c₁ c₂ : Segment) : (deleteMoraic { onset := [c₁], moraic := [{ seg := v, morae := MoraCount.one }, { seg := c₂, morae := MoraCount.one }] } 1).snd = 1

Deleting a moraic coda (WBP active) strands one mora. CL is possible.

theorem Phonology.Moraic.CL.vowel_loss_leftward (v₁ v₂ : Segment) : have σ₁ := { onset := [], moraic := [{ seg := v₁, morae := MoraCount.one }] }; have σ₂ := { onset := [], moraic := [{ seg := v₂, morae := MoraCount.one }] }; match deleteMoraic σ₂ 0 with | (fst, stranded) => have σ₁_cl := spreadToFill σ₁ stranded SpreadDir.left; σ₁_cl.moraCount = σ₁.moraCount + stranded

Vowel-loss directionality (@cite{hayes-1989}, §5.2.2): CL through vowel loss always lengthens the vowel to the left of the deleted vowel, never to the right. In moraic theory this follows from Parasitic Delinking + the No-Crossing Constraint (derived from temporal precedence in Phonology.Autosegmental.no_crossing, @cite{sagey-1986} §5.3): a stranded mora can only be picked up by spreading leftward without crossing.

theorem Phonology.Moraic.CL.wbp_params_enable_cl (o n c : Segment) : have σ := syllableToMoraic { wbp := true } { onset := [o], nucleus := [n], coda := [c] }; (deleteMoraic σ 1).snd = 1

Syllabification with WBP (Rule (10)) produces moraic codas that can trigger CL. This connects MoraicParams to the CL mechanism: the same parameter that determines syllable weight also determines CL possibility (@cite{hayes-1989}, §6).

theorem Phonology.Moraic.CL.no_wbp_params_disable_cl (o n c : Segment) : have σ := syllableToMoraic { wbp := false } { onset := [o], nucleus := [n], coda := [c] }; (deleteMoraic σ 1).snd = 0

Without WBP, syllabification produces non-moraic codas: no CL.