Vowel hiatus

This file defines vowel hiatus, the adjacency of two vowels, and its repair at a morpheme juncture by eliding one of the vowels, by merging the two into one, or by inserting a consonant between them.

Many languages do not tolerate hiatus. Where a vowel-final morpheme meets a vowel-initial one, they elide one of the two vowels, turn the first into a glide, merge the two into a third vowel, syllabify them together as a diphthong, or insert a consonant, and Casali surveys the variation. Which vowel elides is not free. The first vowel is the usual target, and elision of the second is well attested only before a function word and at the boundary between a stem and a suffix, which is the question of Casali's earlier article.

Like OCP.IsClean, Hiatus.Free is a thin layer over List.IsChain, but over two segments both being vowels, not their being identical, and over adjacency in the string, not on a tier. So neither constraint is an instance of the other.

Main definitions

• Hiatus.Free, Hiatus.count: a form has no two adjacent vowels; the number of adjacent vowel pairs.
• Hiatus.Juncture: hiatus at a morpheme boundary, where a vowel-final stem meets a vowel-initial suffix.
• Juncture.epenthesize, Juncture.elideV1, Juncture.elideV2, Juncture.coalesce: the repairs by insertion of a consonant, by elision of either vowel, and by merger of the two into a given vowel.

Main results

• Hiatus.free_iff_count_eq_zero: the ban and the count agree.
• Juncture.not_free_input: the unrepaired concatenation has a hiatus.
• Juncture.free_epenthesize, Juncture.free_elideV1, Juncture.free_elideV2, Juncture.free_coalesce: a repaired form is free of hiatus exactly when the material on each side of the juncture is.
• Juncture.coalesce_v2, Juncture.coalesce_v1: elision is merger into the surviving vowel.
• Juncture.elideV1_eq_eraseIdx, Juncture.elideV2_eq_eraseIdx, Juncture.epenthesize_eq_insertIdx: the repairs as the deletion of one position of the unrepaired concatenation and the insertion of one segment into it.
• Juncture.elideV2_eq_stem_iff: elision of the second vowel merges the suffixed form with the bare stem exactly for a suffix of one segment.

Implementation notes

Which vowel a merger yields turns on the quality of the two, so Juncture.coalesce takes the result as an argument. Glide formation and diphthong formation are not defined, since they turn on the syllabification of the two vowels and no study yet consumes them.

References

• [Cas97]
• [Cas11]

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

A form is free of hiatus 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) : ℕ

count fm is the number of adjacent vowel pairs in the form, the violation count of the markedness constraint against 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

A juncture is a vowel-final stem stemBody ++ [v1] followed by a vowel-initial suffix v2 :: suffixBody. The repairs below resolve the adjacency of v1 and v2, and apply only here, since a consonant-final stem or a consonant-initial suffix never presents it.

• stemBody : List Segment

  The stem without its final vowel.

• v1 : Segment

  The stem-final vowel.

• v2 : Segment

  The suffix-initial vowel.

• suffixBody : List Segment

  The suffix without 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

j.stem is the stem.

Equations

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

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

j.suffix is the suffix.

Equations

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

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

j.input is the unrepaired 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

j.epenthesize c inserts the consonant 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

j.elideV1 elides the stem-final vowel.

Equations

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

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

j.elideV2 elides the suffix-initial vowel.

Equations

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

def Phonology.Hiatus.Juncture.coalesce (j : Juncture) (v : Segment) : List Segment

j.coalesce v merges the two vowels into v.

Equations

• j.coalesce v = j.stemBody ++ v :: j.suffixBody

@[simp]

theorem Phonology.Hiatus.Juncture.length_stem (j : Juncture) : j.stem.length = j.stemBody.length + 1

@[simp]

theorem Phonology.Hiatus.Juncture.length_input (j : Juncture) : j.input.length = j.stemBody.length + j.suffixBody.length + 2

@[simp]

theorem Phonology.Hiatus.Juncture.length_epenthesize (j : Juncture) (c : Segment) : (j.epenthesize c).length = j.stemBody.length + j.suffixBody.length + 3

@[simp]

theorem Phonology.Hiatus.Juncture.length_elideV1 (j : Juncture) : j.elideV1.length = j.stemBody.length + j.suffixBody.length + 1

@[simp]

theorem Phonology.Hiatus.Juncture.length_elideV2 (j : Juncture) : j.elideV2.length = j.stemBody.length + j.suffixBody.length + 1

@[simp]

theorem Phonology.Hiatus.Juncture.length_coalesce (j : Juncture) (v : Segment) : (j.coalesce v).length = j.stemBody.length + j.suffixBody.length + 1

theorem Phonology.Hiatus.Juncture.coalesce_v2 (j : Juncture) : j.coalesce j.v2 = j.elideV1

Merger into the second vowel is elision of the first.

theorem Phonology.Hiatus.Juncture.coalesce_v1 (j : Juncture) : j.coalesce j.v1 = j.elideV2

Merger into the first vowel is elision of the second.

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

The unrepaired concatenation is longer than the bare stem.

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

The form with an inserted consonant is longer than the bare stem.

@[simp]

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

Elision of the second vowel merges the suffixed form with the bare stem exactly when the suffix has one segment.

@[simp]

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

Elision of the first vowel merges the suffixed form with the bare suffix exactly when the stem has one segment.

The repairs as deletion and insertion

def Phonology.Hiatus.Juncture.v1Idx (j : Juncture) : ℕ

j.v1Idx is the position of the first vowel in the unrepaired concatenation.

Equations

• j.v1Idx = j.stemBody.length

def Phonology.Hiatus.Juncture.v2Idx (j : Juncture) : ℕ

j.v2Idx is the position of the second vowel in the unrepaired concatenation.

Equations

• j.v2Idx = j.stemBody.length + 1

theorem Phonology.Hiatus.Juncture.v1Idx_lt_length_input (j : Juncture) : j.v1Idx < j.input.length

theorem Phonology.Hiatus.Juncture.v2Idx_lt_length_input (j : Juncture) : j.v2Idx < j.input.length

theorem Phonology.Hiatus.Juncture.elideV1_eq_eraseIdx (j : Juncture) : j.elideV1 = j.input.eraseIdx j.v1Idx

Elision of the first vowel deletes its position from the unrepaired concatenation.

theorem Phonology.Hiatus.Juncture.elideV2_eq_eraseIdx (j : Juncture) : j.elideV2 = j.input.eraseIdx j.v2Idx

Elision of the second vowel deletes its position from the unrepaired concatenation.

theorem Phonology.Hiatus.Juncture.epenthesize_eq_insertIdx (j : Juncture) (c : Segment) : j.epenthesize c = j.input.insertIdx j.v2Idx c

Insertion of a consonant puts it at the position of the second vowel.

The repairs remove the hiatus

theorem Phonology.Hiatus.Juncture.not_free_input (j : Juncture) : ¬Free j.input

The unrepaired concatenation has a hiatus.

theorem Phonology.Hiatus.Juncture.free_epenthesize (j : Juncture) {c : Segment} (hc : ¬c.IsVowel) : Free (j.epenthesize c) ↔ Free j.stem ∧ Free j.suffix

The form with an inserted consonant is free of hiatus exactly when the stem and the suffix are.

theorem Phonology.Hiatus.Juncture.free_elideV1 (j : Juncture) : Free j.elideV1 ↔ Free (j.stemBody ++ [j.v2]) ∧ Free j.suffix

The form without the first vowel is free of hiatus exactly when the stem body followed by the second vowel is, and the suffix is.

theorem Phonology.Hiatus.Juncture.free_elideV2 (j : Juncture) : Free j.elideV2 ↔ Free j.stem ∧ Free (j.v1 :: j.suffixBody)

The form without the second vowel is free of hiatus exactly when the stem is, and the first vowel followed by the suffix body is.

theorem Phonology.Hiatus.Juncture.free_coalesce (j : Juncture) (v : Segment) : Free (j.coalesce v) ↔ Free (j.stemBody ++ [v]) ∧ Free (v :: j.suffixBody)

The form with the two vowels merged into v is free of hiatus exactly when the stem body followed by v is, and v followed by the suffix body is.