Vowel hiatus

Two adjacent vowels — a hiatus — are cross-linguistically dispreferred, and languages repair the configuration, most often at morpheme junctures, by eliding one of the two vowels ([Cas97]'s question: which one goes?), epenthesizing a consonant between them, or fusing them ([Cas11b]). This file defines the configuration and its elision and epenthesis repairs.

Like OCP.IsClean, Hiatus.Free is a thin layer over List.IsChain — but over co-vowelhood rather than identity, and string-adjacent rather than tier-adjacent, so neither constraint instantiates the other and the repairs differ (elision and epenthesis here; fusion and antigemination there).

Main definitions

• Hiatus.Free / Hiatus.count — no vowel–vowel adjacency; the number of vowel–vowel adjacencies.
• Hiatus.Juncture — hiatus at a morpheme boundary: a vowel-final stem meets a vowel-initial suffix.
• Juncture.epenthesize, Juncture.elideV1, Juncture.elideV2 — the repairs, applicable only to a genuine hiatus configuration.

Main results

• Hiatus.free_iff_count_eq_zero — the ban and the count agree.
• Juncture.elideV2_eq_stem_iff — V2 elision merges the suffixed form with the bare stem exactly for monosegmental suffixes.

def Phonology.Hiatus.Free (fm : List Segment) : Prop

A form is hiatus-free when no two adjacent segments are both vowels.

Equations

• Phonology.Hiatus.Free fm = List.IsChain (fun (a b : Phonology.Segment) => ¬(a.IsVowel ∧ b.IsVowel)) fm

@[instance_reducible]

instance Phonology.Hiatus.instDecidablePredListSegmentFree : DecidablePred Free

Equations

• Phonology.Hiatus.instDecidablePredListSegmentFree fm = Phonology.Hiatus.instDecidablePredListSegmentFree._aux_1 fm

def Phonology.Hiatus.count (fm : List Segment) : ℕ

The number of vowel–vowel adjacencies in a form — the violation count of the markedness constraint *Hiatus.

Equations

• Phonology.Hiatus.count fm = List.countP (fun (p : Phonology.Segment × Phonology.Segment) => decide (p.1.IsVowel ∧ p.2.IsVowel)) (fm.zip fm.tail)

@[simp]

theorem Phonology.Hiatus.count_nil : count [] = 0

@[simp]

theorem Phonology.Hiatus.count_singleton (a : Segment) : count [a] = 0

theorem Phonology.Hiatus.count_cons_cons (a b : Segment) (fm : List Segment) : count (a :: b :: fm) = count (b :: fm) + if a.IsVowel ∧ b.IsVowel then 1 else 0

theorem Phonology.Hiatus.free_iff_count_eq_zero (fm : List Segment) : Free fm ↔ count fm = 0

The categorical ban and the violation count agree.

Hiatus at a morpheme juncture

structure Phonology.Hiatus.Juncture : Type

Hiatus at a morpheme boundary ([Cas97]'s hiatus context): a vowel-final stem stemBody ++ [v1] meets a vowel-initial suffix v2 :: suffixBody. The repairs below resolve the v1–v2 adjacency, and apply only here — a consonant-final stem or consonant-initial suffix never presents the configuration.

• stemBody : List Segment

  The stem minus its final vowel.

• v1 : Segment

  The stem-final vowel.

• v2 : Segment

  The suffix-initial vowel.

• suffixBody : List Segment

  The suffix minus its initial vowel.

• v1_isVowel : self.v1.IsVowel

  The stem-final segment is a vowel.

• v2_isVowel : self.v2.IsVowel

  The suffix-initial segment is a vowel.

def Phonology.Hiatus.Juncture.stem (j : Juncture) : List Segment

The stem.

Equations

• j.stem = j.stemBody ++ [j.v1]

def Phonology.Hiatus.Juncture.suffix (j : Juncture) : List Segment

The suffix.

Equations

• j.suffix = j.v2 :: j.suffixBody

def Phonology.Hiatus.Juncture.input (j : Juncture) : List Segment

The underlying concatenation, with v1 and v2 in hiatus.

Equations

• j.input = j.stemBody ++ j.v1 :: j.v2 :: j.suffixBody

theorem Phonology.Hiatus.Juncture.stem_append_suffix (j : Juncture) : j.stem ++ j.suffix = j.input

def Phonology.Hiatus.Juncture.epenthesize (j : Juncture) (c : Segment) : List Segment

Consonant epenthesis: insert c between the two vowels.

Equations

• j.epenthesize c = j.stemBody ++ j.v1 :: c :: j.v2 :: j.suffixBody

def Phonology.Hiatus.Juncture.elideV1 (j : Juncture) : List Segment

V1 elision: the stem-final vowel goes.

Equations

• j.elideV1 = j.stemBody ++ j.suffix

def Phonology.Hiatus.Juncture.elideV2 (j : Juncture) : List Segment

V2 elision: the suffix-initial vowel goes.

Equations

• j.elideV2 = j.stem ++ j.suffixBody

theorem Phonology.Hiatus.Juncture.input_ne_stem (j : Juncture) : j.input ≠ j.stem

The faithful concatenation is longer than the bare stem.

theorem Phonology.Hiatus.Juncture.epenthesize_ne_stem (j : Juncture) (c : Segment) : j.epenthesize c ≠ j.stem

The epenthesized form is longer than the bare stem.

@[simp]

theorem Phonology.Hiatus.Juncture.elideV2_eq_stem_iff (j : Juncture) : j.elideV2 = j.stem ↔ j.suffixBody = []

V2 elision merges the suffixed form with the bare stem exactly when the suffix is monosegmental — the categorical core of suffix-length-conditioned hiatus resolution.

@[simp]

theorem Phonology.Hiatus.Juncture.elideV1_eq_suffix_iff (j : Juncture) : j.elideV1 = j.suffix ↔ j.stemBody = []

V1 elision merges the suffixed form with the bare suffix exactly when the stem is monosegmental.