Casali (1997): Vowel Elision in Hiatus Contexts: Which Vowel Goes?

Casali observes that elision of the first of two vowels in hiatus is possible everywhere, while elision of the second is found only where a lexical word or root precedes a function word or suffix. He derives this from MAX constraints that protect segments in prominent positions: the beginning of a word, a lexical word or root, the beginning of a morpheme, and a morpheme of one segment. An elision deletes one vowel, so it violates the constraints that protect the position of that vowel, and an elision can be optimal exactly when the constraints it violates are not a proper superset of those the other elision violates.

Main definitions

• con: Casali's constraints, MAX restricted to each prominent position and general MAX, on the two elisions.
• violations: the constraints an elision violates, a row of the paper's table of violations.
• tableau: the tableau of the two elisions under a ranking.

Main results

• exists_mem_optimal_iff: an elision is optimal under some ranking iff the constraints it violates are not a proper superset of those the other elision violates.
• exists_mem_optimal_second_iff: where the first vowel begins no morpheme, the second can elide iff the first morph is a root and the second is not.
• survey_allowed, survey_second_iff: every elision the survey of Section 2 reports is allowed, and the survey reports an elision of the second vowel at exactly the kinds of juncture where one is allowed.

Implementation notes

• The constraints are indexed by Option Prominence: some p is MAX restricted to the position p, and none is general MAX (con_none). Every elision violates general MAX once, so it never decides between them, and the universal ranking of the positional constraints above it is not imposed.
• Lexical status and word boundaries are read off the kinds of the two morphs: roots are lexical, and affixes, clitics and free function words are not.
• A word-initial vowel is also morpheme-initial, so the second vowel violates the morpheme-initial constraint at a word boundary too, which the paper's table of violations leaves out and which changes no prediction.
• schematic k is the paper's schematic juncture /CV₁ + V₂C/ at the survey's kind k, with C and V the natural classes [+consonantal] and [+syllabic]; it witnesses that every kind of juncture has a context.

References

• [Cas97]
• [McCP95]

def Casali1997.position (c : Phonology.Hiatus.Context) : Data.Hiatus.ElidedVowel → ℕ

position c e is the position of the vowel that e elides.

Equations

• Casali1997.position c Data.Hiatus.ElidedVowel.first = c.v1Idx
• Casali1997.position c Data.Hiatus.ElidedVowel.second = c.v2Idx

theorem Casali1997.position_lt_length_input (c : Phonology.Hiatus.Context) (e : Data.Hiatus.ElidedVowel) : position c e < c.input.length

def Casali1997.protects (c : Phonology.Hiatus.Context) : Option Phonology.Hiatus.Prominence → ℕ → Prop

protects c i k holds when the constraint i protects position k. General MAX (none) protects every position, and MAX restricted to a prominent position (some p) the positions that lie in it.

Equations

• Casali1997.protects c none x✝ = True
• Casali1997.protects c (some p) x✝ = c.Protects p x✝

@[instance_reducible]

instance Casali1997.instDecidablePredNatProtects (c : Phonology.Hiatus.Context) (i : Option Phonology.Hiatus.Prominence) : DecidablePred (protects c i)

Equations

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

def Casali1997.con (c : Phonology.Hiatus.Context) : OptimalityTheory.ConstraintSet Data.Hiatus.ElidedVowel (Option Phonology.Hiatus.Prominence)

Casali's constraints on the two elisions, each of which deletes the position of the elided vowel.

Equations

• Casali1997.con c = OptimalityTheory.positionalMax (Casali1997.protects c) fun (e : Data.Hiatus.ElidedVowel) => {Casali1997.position c e}

def Casali1997.corr (c : Phonology.Hiatus.Context) (e : Data.Hiatus.ElidedVowel) : OptimalityTheory.Correspondence OptimalityTheory.BinaryRole Phonology.Segment

corr c e is the correspondence between the unrepaired concatenation and the form that the elision e gives.

Equations

• Casali1997.corr c e = OptimalityTheory.Correspondence.eraseIdx c.input (Casali1997.position c e)

def Casali1997.resolve (c : Phonology.Hiatus.Context) (e : Data.Hiatus.ElidedVowel) : List Phonology.Segment

resolve c e is the form that the elision e gives.

Equations

• Casali1997.resolve c e = (Casali1997.corr c e).form OptimalityTheory.BinaryRole.rhs

theorem Casali1997.resolve_first (c : Phonology.Hiatus.Context) : resolve c Data.Hiatus.ElidedVowel.first = c.elideV1

theorem Casali1997.resolve_second (c : Phonology.Hiatus.Context) : resolve c Data.Hiatus.ElidedVowel.second = c.elideV2

theorem Casali1997.con_eq_maxViolAt (c : Phonology.Hiatus.Context) (i : Option Phonology.Hiatus.Prominence) (e : Data.Hiatus.ElidedVowel) : con c i e = OptimalityTheory.Correspondence.maxViolAt (protects c i) (corr c e) OptimalityTheory.BinaryRole.lhs OptimalityTheory.BinaryRole.rhs

Each constraint counts the input segments it protects that have no correspondent in the output.

theorem Casali1997.con_none (c : Phonology.Hiatus.Context) (e : Data.Hiatus.ElidedVowel) : con c none e = (corr c e).maxViol OptimalityTheory.BinaryRole.lhs OptimalityTheory.BinaryRole.rhs

General MAX counts the input segments that have no correspondent in the output.

def Casali1997.violations (c : Phonology.Hiatus.Context) (e : Data.Hiatus.ElidedVowel) : Set (Option Phonology.Hiatus.Prominence)

violations c e is the set of constraints that the elision e violates, those protecting the position of the elided vowel. It is a row of the paper's table of violations.

Equations

• Casali1997.violations c e = {i : Option Phonology.Hiatus.Prominence | Casali1997.protects c i (Casali1997.position c e)}

@[simp]

theorem Casali1997.none_mem_violations {c : Phonology.Hiatus.Context} (e : Data.Hiatus.ElidedVowel) : none ∈ violations c e

@[simp]

theorem Casali1997.some_mem_violations_first {c : Phonology.Hiatus.Context} {p : Phonology.Hiatus.Prominence} : some p ∈ violations c Data.Hiatus.ElidedVowel.first ↔ c.Protects p c.v1Idx

@[simp]

theorem Casali1997.some_mem_violations_second {c : Phonology.Hiatus.Context} {p : Phonology.Hiatus.Prominence} : some p ∈ violations c Data.Hiatus.ElidedVowel.second ↔ c.Protects p c.v2Idx

theorem Casali1997.soleSegment_mem_violations_second_iff {c : Phonology.Hiatus.Context} : some Phonology.Hiatus.Prominence.soleSegment ∈ violations c Data.Hiatus.ElidedVowel.second ↔ resolve c Data.Hiatus.ElidedVowel.second = c.stem

The second vowel occupies a morph of one segment exactly when eliding it leaves the bare stem, so that no segment of the second morph remains.

Which vowel elides

@[reducible, inline]

abbrev Casali1997.tableau (c : Phonology.Hiatus.Context) (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5) : OptimalityTheory.Tableau Data.Hiatus.ElidedVowel 5

The tableau of the two elisions under the ranking r.

Equations

• Casali1997.tableau c r = OptimalityTheory.Tableau.ofPerm (Casali1997.con c) r [Data.Hiatus.ElidedVowel.first, Data.Hiatus.ElidedVowel.second] Casali1997.tableau._proof_1

theorem Casali1997.exists_mem_optimal_iff {c : Phonology.Hiatus.Context} {e e' : Data.Hiatus.ElidedVowel} (hne : e ≠ e') : (∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), e ∈ (tableau c r).optimal) ↔ ¬violations c e' ⊂ violations c e

An elision is optimal under some ranking exactly when the constraints it violates are not a proper superset of those the other elision violates.

theorem Casali1997.exists_optimal_eq_singleton_iff {c : Phonology.Hiatus.Context} {e e' : Data.Hiatus.ElidedVowel} (hne : e ≠ e') : (∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), (tableau c r).optimal = {e}) ↔ ¬violations c e' ⊆ violations c e

An elision is the sole optimum under some ranking exactly when the other elision violates a constraint it does not.

theorem Casali1997.optimal_eq_singleton_iff {c : Phonology.Hiatus.Context} {e e' : Data.Hiatus.ElidedVowel} (hne : e ≠ e') (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5) : (tableau c r).optimal = {e} ↔ ∃ i ∈ violations c e', i ∉ violations c e ∧ ∀ j ∈ violations c e, j ∉ violations c e' → r.Dominates i j

One elision is the sole optimum under a ranking exactly when some constraint violated only by the other outranks every constraint violated only by it.

theorem Casali1997.optimal_eq_singleton_of_forall_dominates {c : Phonology.Hiatus.Context} {e e' : Data.Hiatus.ElidedVowel} (hne : e ≠ e') {r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5} {i : Option Phonology.Hiatus.Prominence} (hi : i ∉ violations c e) (hi' : i ∈ violations c e') (hr : ∀ (j : Option Phonology.Hiatus.Prominence), j ≠ i → r.Dominates i j) : (tableau c r).optimal = {e}

A constraint violated only by the other elision and ranked on top makes an elision the sole optimum.

theorem Casali1997.exists_optimal_eq_first {c : Phonology.Hiatus.Context} (h : c.stemBody ≠ []) : ∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), (tableau c r).optimal = {Data.Hiatus.ElidedVowel.first}

The first vowel can elide alone in every context where it begins no morph.

theorem Casali1997.exists_mem_optimal_second_iff {c : Phonology.Hiatus.Context} (h : c.stemBody ≠ []) : (∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), Data.Hiatus.ElidedVowel.second ∈ (tableau c r).optimal) ↔ c.left = Morphology.Morph.Kind.root ∧ c.right ≠ Morphology.Morph.Kind.root

Where the first vowel begins no morph, the second vowel elides under some ranking exactly when the first morph is a root and the second is not. This covers the boundary between two lexical words, between a lexical and a function word in either order, between a prefix of more than one segment and a root, between a root and a suffix, and between two affixes or clitics.

theorem Casali1997.exists_optimal_eq_of_vowelPrefix {c : Phonology.Hiatus.Context} (h : c.stemBody = []) (hs : c.suffixBody ≠ []) (hl : c.left ≠ Morphology.Morph.Kind.root) (hr : c.right = Morphology.Morph.Kind.root) (e : Data.Hiatus.ElidedVowel) : ∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), (tableau c r).optimal = {e}

After a prefix of one vowel, either vowel can elide alone, since only eliding the first violates the constraint on morphs of one segment and only eliding the second violates the constraint on lexical material, as in the paper's tableaux (15) and (16).

The kinds of juncture of the survey

def Casali1997.kinds : Data.Hiatus.Juncture → Morphology.Morph.Kind × Morphology.Morph.Kind

The kinds of the two morphs at a kind of juncture of the survey. A lexical word is a root, and a function word is free and not a root.

Equations

• One or more equations did not get rendered due to their size.
• Casali1997.kinds Data.Hiatus.Juncture.lexicalLexical = (Morphology.Morph.Kind.root, Morphology.Morph.Kind.root)
• Casali1997.kinds Data.Hiatus.Juncture.lexicalFunction = (Morphology.Morph.Kind.root, Morphology.Morph.Kind.free)
• Casali1997.kinds Data.Hiatus.Juncture.prefixRoot = (Morphology.Morph.Kind.bound Morphology.Morph.Position.before Morphology.Morph.Attachment.affix, Morphology.Morph.Kind.root)
• Casali1997.kinds Data.Hiatus.Juncture.rootSuffix = (Morphology.Morph.Kind.root, Morphology.Morph.Kind.bound Morphology.Morph.Position.after Morphology.Morph.Attachment.affix)

structure Casali1997.IsOfKind (c : Phonology.Hiatus.Context) (k : Data.Hiatus.Juncture) : Prop

IsOfKind c k holds when the context c is a juncture of the survey's kind k at which the first vowel begins no morph.

• stemBody_ne_nil : c.stemBody ≠ []
• left : c.left = (kinds k).1
• right : c.right = (kinds k).2

def Casali1997.C : Phonology.Segment

The paper's schematic consonant, the natural class [+consonantal].

Equations

• Casali1997.C = Phonology.Segment.ofSpecs [(Phonology.Feature.consonantal, true)]

def Casali1997.V : Phonology.Segment

The paper's schematic vowel, the natural class [+syllabic].

Equations

• Casali1997.V = Phonology.Segment.ofSpecs [(Phonology.Feature.syllabic, true)]

def Casali1997.schematic (k : Data.Hiatus.Juncture) : Phonology.Hiatus.Context

The paper's schematic juncture /CV₁ + V₂C/ at the survey's kind k, at the start of an utterance.

Equations

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

theorem Casali1997.isOfKind_schematic (k : Data.Hiatus.Juncture) : IsOfKind (schematic k) k

theorem Casali1997.exists_mem_optimal_iff_of_isOfKind {c : Phonology.Hiatus.Context} {k : Data.Hiatus.Juncture} (hc : IsOfKind c k) {e : Data.Hiatus.ElidedVowel} : (∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), e ∈ (tableau c r).optimal) ↔ e = Data.Hiatus.ElidedVowel.first ∨ (kinds k).1 = Morphology.Morph.Kind.root ∧ (kinds k).2 ≠ Morphology.Morph.Kind.root

At a juncture of the survey's kind k, the first vowel can always elide, and the second exactly when the first morph is a root and the second is not.

theorem Casali1997.schematic_second : (¬∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), Data.Hiatus.ElidedVowel.second ∈ (tableau (schematic Data.Hiatus.Juncture.lexicalLexical) r).optimal) ∧ ∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), Data.Hiatus.ElidedVowel.second ∈ (tableau (schematic Data.Hiatus.Juncture.lexicalFunction) r).optimal

At the paper's schematic juncture of two lexical words no ranking elides the second vowel, as in its tableau (10), while before a function word some ranking does, as in its tableau (12).

theorem Casali1997.lexical_on_top {r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5} (hr : ∀ (j : Option Phonology.Hiatus.Prominence), j ≠ some Phonology.Hiatus.Prominence.lexical → r.Dominates (some Phonology.Hiatus.Prominence.lexical) j) {c c' : Phonology.Hiatus.Context} (hc : IsOfKind c Data.Hiatus.Juncture.prefixRoot) (hc' : IsOfKind c' Data.Hiatus.Juncture.rootSuffix) : (tableau c r).optimal = {Data.Hiatus.ElidedVowel.first} ∧ (tableau c' r).optimal = {Data.Hiatus.ElidedVowel.second}

With the constraint on lexical material on top, the first vowel elides after a prefix and the second before a suffix of any length, the asymmetry within one language that the paper reports for Chichewa.

theorem Casali1997.soleSegment_over_lexical {c : Phonology.Hiatus.Context} {r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5} (h₁ : r.Dominates (some Phonology.Hiatus.Prominence.soleSegment) (some Phonology.Hiatus.Prominence.lexical)) (h₂ : r.Dominates (some Phonology.Hiatus.Prominence.lexical) (some Phonology.Hiatus.Prominence.morphemeInitial)) (hc : IsOfKind c Data.Hiatus.Juncture.rootSuffix) : (tableau c r).optimal = {if c.suffixBody = [] then Data.Hiatus.ElidedVowel.first else Data.Hiatus.ElidedVowel.second}

With the constraint on morphs of one segment over the constraint on lexical material, and that over the morpheme-initial constraint, the first vowel elides before a suffix of one segment and the second before a longer one, as in the paper's tableaux (19) and (20).

The survey

theorem Casali1997.survey_allowed (row : Data.Hiatus.ElisionRow) : row ∈ Data.Hiatus.Casali1997.rows → ∀ (c : Phonology.Hiatus.Context), IsOfKind c row.juncture → ∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), row.elided ∈ (tableau c r).optimal

Every elision the survey reports is one the analysis allows, in that some ranking elides the reported vowel at a juncture of the reported kind.

theorem Casali1997.survey_second_iff {c : Phonology.Hiatus.Context} {k : Data.Hiatus.Juncture} (hc : IsOfKind c k) : (∃ row ∈ Data.Hiatus.Casali1997.rows, row.juncture = k ∧ row.elided = Data.Hiatus.ElidedVowel.second) ↔ ∃ (r : OptimalityTheory.Ranking (Option Phonology.Hiatus.Prominence) 5), Data.Hiatus.ElidedVowel.second ∈ (tableau c r).optimal

The survey reports an elision of the second vowel at exactly the kinds of juncture where the analysis allows one, before a function word and before a suffix.