Prominent positions at a juncture of two morphs

Where two vowels meet at the boundary of two morphs, eliding either removes the hiatus, and which one goes depends on the positions the two vowels occupy. Casali identifies the positions whose segments resist deletion as the beginning of a word, a lexical word or root, the beginning of a morph, and a morph of one segment. A juncture whose two sides are adjacent morphs of known kinds fixes all four: a morph is lexical when it is a root, and a morph begins a word unless it is joined as an affix or clitic to the morph before it.

Main definitions

• Phonology.Hiatus.Context: a juncture of two adjacent morphs, with their kinds and the kind of the morph before them.
• Phonology.Hiatus.Prominence, Phonology.Hiatus.Context.Protects: the prominent positions, and the positions of the unrepaired concatenation that lie in each.

Main results

• Phonology.Hiatus.Context.protects_v1Idx, Phonology.Hiatus.Context.protects_v2Idx: the prominent positions of each vowel, read off the kinds of the morphs and the length of each.

References

• [Cas97]
• [Has20]

inductive Phonology.Hiatus.Prominence : Type

A prominent position, whose segments a faithfulness constraint can protect from deletion.

• wordInitial : Prominence

  The beginning of a word.

• lexical : Prominence

  A lexical word or a root.

• morphemeInitial : Prominence

  The beginning of a morph.

• soleSegment : Prominence

  A morph of one segment.

@[instance_reducible]

instance Phonology.Hiatus.instDecidableEqProminence : DecidableEq Prominence

Equations

• Phonology.Hiatus.instDecidableEqProminence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Phonology.Hiatus.instFintypeProminence : Fintype Prominence

Equations

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

@[instance_reducible]

instance Phonology.Hiatus.instReprProminence : Repr Prominence

Equations

• Phonology.Hiatus.instReprProminence = { reprPrec := Phonology.Hiatus.instReprProminence.repr }

def Phonology.Hiatus.instReprProminence.repr : Prominence → ℕ → Std.Format

Equations

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

structure Phonology.Hiatus.Contextextends Phonology.Hiatus.Juncture : Type

A context is a juncture whose stem and suffix are the forms of two adjacent morphs, together with the kinds of the two morphs and of the morph before them, if there is one.

• stemBody : List Segment
• v1 : Segment
• v2 : Segment
• suffixBody : List Segment
• v1_isVowel : self.v1.IsVowel
• v2_isVowel : self.v2.IsVowel
• before : Option Morphology.Morph.Kind

  The kind of the morph before the first, if there is one.

• left : Morphology.Morph.Kind

  The kind of the first morph.

• right : Morphology.Morph.Kind

  The kind of the second morph.

def Phonology.Hiatus.Context.Protects (c : Context) : Prominence → ℕ → Prop

c.Protects p k holds when position k of the unrepaired concatenation lies in the prominent position p. The first position and the position of the second vowel each begin a morph, and begin a word unless that morph is joined as an affix or clitic to the morph before it. A position is lexical when its morph is a root, and is a sole segment when its morph has no other.

Equations

• One or more equations did not get rendered due to their size.
• c.Protects Phonology.Hiatus.Prominence.lexical x✝ = (x✝ ≤ c.v1Idx ∧ c.left = Morphology.Morph.Kind.root ∨ c.v2Idx ≤ x✝ ∧ c.right = Morphology.Morph.Kind.root)
• c.Protects Phonology.Hiatus.Prominence.morphemeInitial x✝ = (x✝ = 0 ∨ x✝ = c.v2Idx)
• c.Protects Phonology.Hiatus.Prominence.soleSegment x✝ = (x✝ = 0 ∧ c.stemBody = [] ∨ x✝ = c.v2Idx ∧ c.suffixBody = [])

@[instance_reducible]

instance Phonology.Hiatus.Context.instDecidablePredNatProtects (c : Context) (p : Prominence) : DecidablePred (c.Protects p)

Equations

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

@[simp]

theorem Phonology.Hiatus.Context.protects_v1Idx {c : Context} {p : Prominence} : c.Protects p c.v1Idx ↔ match p with | Prominence.wordInitial => c.stemBody = [] ∧ ∀ b ∈ c.before, ¬Morphology.Morph.Kind.JoinsAt Morphology.Morph.Attachment.clitic b c.left | Prominence.lexical => c.left = Morphology.Morph.Kind.root | Prominence.morphemeInitial => c.stemBody = [] | Prominence.soleSegment => c.stemBody = []

The first vowel begins a word when it is the whole of its morph and that morph begins a word, is lexical when its morph is a root, and begins a morph or makes it up when it is the whole of it.

@[simp]

theorem Phonology.Hiatus.Context.protects_v2Idx {c : Context} {p : Prominence} : c.Protects p c.v2Idx ↔ match p with | Prominence.wordInitial => ¬Morphology.Morph.Kind.JoinsAt Morphology.Morph.Attachment.clitic c.left c.right | Prominence.lexical => c.right = Morphology.Morph.Kind.root | Prominence.morphemeInitial => True | Prominence.soleSegment => c.suffixBody = []

The second vowel always begins a morph, begins a word when its morph is not joined to the first, is lexical when its morph is a root, and makes up its morph when that has no other segment.