Vago (2017): *VV in Hungarian

Vago analyses the vowel sequences that suffixation creates in Hungarian with Casali's position-sensitive MAX constraints and a ban on vowel sequences, *VV. Between a root and a suffix the second vowel usually deletes, under the hierarchy MAX LEX ≫ *VV ≫ MAX MI, and a handful of suffixes are indexed to rerankings that delete the first vowel instead or keep both. Between two suffixes the second vowel deletes after a long vowel or a suffix of one vowel, which high-ranked MAX constraints on long vowels and on morphs of one segment protect, and the first vowel deletes after the infinitival suffix -ni. Vago concludes that Casali's constraints make the right predictions for Hungarian.

Main results

• optimal_regular: between a morph and a suffix that are not roots, the regular hierarchy deletes the second vowel when the first is long or alone in its morph, and the first otherwise.
• tableaux: for every example, the tableau of its four candidates (no deletion, either vowel, both) under the hierarchy of its suffix selects the attested deletion, and its output spells the attested form.
• starVV_dominates_of_erdesz: a ranking that deletes the first vowel of erdő-ész ranks *VV above MAX on long vowels and MAX LEX, since the deleted root vowel is long.

Implementation notes

• Each example is a row of Data/Forms/Vago2017 giving its two morphs, their kinds, the morph before them, the attested deletion and the hierarchy its suffix is indexed to. Long vowels are read off the accents of the spelling, length being prosodic in the Hungarian fragment.
• The hierarchy that deletes the first vowel is taken as Table 2 prints it, without the constraints on long vowels and morphs of one segment, which the paper ranks above the regular hierarchy; with MAX on long vowels on top it would keep the long vowel of erdő (starVV_dominates_of_erdesz).
• Vago derives the deletion after -ni in Table 4 from the reranking (8b), and the row follows him; the regular hierarchy derives it too (optimal_regular), since MAX LEX does not bear on two suffixes.

References

• [Vag17]
• [Cas97]

inductive Vago2017.Con : Type

Vago's constraints are MAX on long vowels (22), MAX on morphs of one segment (24), MAX on lexical material (4), the ban on vowel sequences (5), and MAX on morpheme-initial segments (6).

• maxLong : Con
• maxMS : Con
• maxLex : Con
• starVV : Con
• maxMI : Con

@[instance_reducible]

instance Vago2017.instDecidableEqCon : DecidableEq Con

Equations

• Vago2017.instDecidableEqCon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Vago2017.instFintypeCon : Fintype Con

Equations

• Vago2017.instFintypeCon = { elems := { val := ↑Vago2017.Con.enumList, nodup := Vago2017.Con.enumList_nodup }, complete := Vago2017.instFintypeCon._proof_1 }

def Vago2017.instReprCon.repr : Con → ℕ → Std.Format

Equations

• Vago2017.instReprCon.repr Vago2017.Con.maxLong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Vago2017.Con.maxLong")).group prec✝
• Vago2017.instReprCon.repr Vago2017.Con.maxMS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Vago2017.Con.maxMS")).group prec✝
• Vago2017.instReprCon.repr Vago2017.Con.maxLex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Vago2017.Con.maxLex")).group prec✝
• Vago2017.instReprCon.repr Vago2017.Con.starVV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Vago2017.Con.starVV")).group prec✝
• Vago2017.instReprCon.repr Vago2017.Con.maxMI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Vago2017.Con.maxMI")).group prec✝

@[instance_reducible]

instance Vago2017.instReprCon : Repr Con

Equations

• Vago2017.instReprCon = { reprPrec := Vago2017.instReprCon.repr }

def Vago2017.deleted (c : Phonology.Hiatus.Context) (D : Finset Data.Hiatus.ElidedVowel) : Finset ℕ

A candidate is the set of vowels it deletes, and deleted c D the positions they occupy.

Equations

• Vago2017.deleted c D = Finset.image (Casali1997.position c) D

def Vago2017.resolve (c : Phonology.Hiatus.Context) (D : Finset Data.Hiatus.ElidedVowel) : List Phonology.Segment

The form a candidate gives.

Equations

• Vago2017.resolve c D = ((c.stemBody ++ if Data.Hiatus.ElidedVowel.first ∈ D then [] else [c.v1]) ++ if Data.Hiatus.ElidedVowel.second ∈ D then [] else [c.v2]) ++ c.suffixBody

def Vago2017.marks (c : Phonology.Hiatus.Context) (long : Finset ℕ) (D : Finset Data.Hiatus.ElidedVowel) : Con → ℕ

The violations of a candidate, with the long vowels at the positions long.

Equations

• Vago2017.marks c long D Vago2017.Con.maxLong = OptimalityTheory.maxAt (fun (x : ℕ) => x ∈ long) (Vago2017.deleted c D)
• Vago2017.marks c long D Vago2017.Con.maxMS = OptimalityTheory.maxAt (c.Protects Phonology.Hiatus.Prominence.soleSegment) (Vago2017.deleted c D)
• Vago2017.marks c long D Vago2017.Con.maxLex = OptimalityTheory.maxAt (c.Protects Phonology.Hiatus.Prominence.lexical) (Vago2017.deleted c D)
• Vago2017.marks c long D Vago2017.Con.starVV = Phonology.Hiatus.count (Vago2017.resolve c D)
• Vago2017.marks c long D Vago2017.Con.maxMI = OptimalityTheory.maxAt (c.Protects Phonology.Hiatus.Prominence.morphemeInitial) (Vago2017.deleted c D)

@[reducible, inline]

abbrev Vago2017.tableau (c : Phonology.Hiatus.Context) (long : Finset ℕ) (order : List Con) : OptimalityTheory.Tableau (Finset Data.Hiatus.ElidedVowel) order.length

The tableau of the four candidates under a constraint order, most dominant first.

Equations

• Vago2017.tableau c long order = OptimalityTheory.Tableau.ofOrder order (Vago2017.marks c long)

inductive Vago2017.Hierarchy : Type

The hierarchy a suffix is indexed to.

• regular : Hierarchy

  The regular hierarchy (8a), MAX LEX ≫ *VV ≫ MAX MI, below MAX on long vowels and on morphs of one segment.

• v1Deletion : Hierarchy

  The reranking (8b) that deletes the first vowel, *VV ≫ MAX MI ≫ MAX LEX.

• noDeletion : Hierarchy

  The reranking (9b) that deletes neither vowel, MAX LEX ≫ MAX MI ≫ *VV.

@[instance_reducible]

instance Vago2017.instDecidableEqHierarchy : DecidableEq Hierarchy

Equations

• Vago2017.instDecidableEqHierarchy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Vago2017.instReprHierarchy.repr : Hierarchy → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Vago2017.instReprHierarchy.repr Vago2017.Hierarchy.regular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Vago2017.Hierarchy.regular")).group prec✝

@[instance_reducible]

instance Vago2017.instReprHierarchy : Repr Hierarchy

Equations

• Vago2017.instReprHierarchy = { reprPrec := Vago2017.instReprHierarchy.repr }

def Vago2017.Hierarchy.order : Hierarchy → List Con

The constraint order of a hierarchy, most dominant first.

Equations

• Vago2017.Hierarchy.regular.order = [Vago2017.Con.maxLong, Vago2017.Con.maxMS, Vago2017.Con.maxLex, Vago2017.Con.starVV, Vago2017.Con.maxMI]
• Vago2017.Hierarchy.v1Deletion.order = [Vago2017.Con.starVV, Vago2017.Con.maxMI, Vago2017.Con.maxLex]
• Vago2017.Hierarchy.noDeletion.order = [Vago2017.Con.maxLex, Vago2017.Con.maxMI, Vago2017.Con.starVV]

Between two suffixes

@[simp]

theorem Vago2017.deleted_empty {c : Phonology.Hiatus.Context} : deleted c ∅ = ∅

@[simp]

theorem Vago2017.deleted_first {c : Phonology.Hiatus.Context} : deleted c {Data.Hiatus.ElidedVowel.first} = {c.v1Idx}

@[simp]

theorem Vago2017.deleted_second {c : Phonology.Hiatus.Context} : deleted c {Data.Hiatus.ElidedVowel.second} = {c.v2Idx}

@[simp]

theorem Vago2017.deleted_pair {c : Phonology.Hiatus.Context} : deleted c {Data.Hiatus.ElidedVowel.first, Data.Hiatus.ElidedVowel.second} = {c.v1Idx, c.v2Idx}

theorem Vago2017.resolve_empty {c : Phonology.Hiatus.Context} : resolve c ∅ = c.input

theorem Vago2017.optimal_regular (c : Phonology.Hiatus.Context) (long : Finset ℕ) (hl : c.left ≠ Morphology.Morph.Kind.root) (hr : c.right ≠ Morphology.Morph.Kind.root) (hv₂ : c.v2Idx ∉ long) (hs : c.suffixBody ≠ []) (hfree : ∀ (D : Finset Data.Hiatus.ElidedVowel), D.Nonempty → Phonology.Hiatus.count (resolve c D) = 0) : (tableau c long Hierarchy.regular.order).optimal = {if c.v1Idx ∈ long ∨ c.stemBody = [] then {Data.Hiatus.ElidedVowel.second} else {Data.Hiatus.ElidedVowel.first}}

Between a morph and a suffix that is not a root, under the regular hierarchy, the second vowel deletes when the first is long or the sole segment of its morph, and the first vowel deletes otherwise. This holds when the second vowel is short and not alone in its morph, and deleting either vowel or both leaves no vowel sequence.

The examples

def Vago2017.context? (before : Option Morphology.Morph.Kind) (left right : Morphology.Morph.Kind) (l r : List Phonology.Segment) : Option Phonology.Hiatus.Context

The context of two spelled morphs of the given kinds, if the first ends and the second begins with a vowel.

Equations

• One or more equations did not get rendered due to their size.
• Vago2017.context? before left right l r✝ = none

structure Vago2017.Example : Type

An example records its context, the positions of its long vowels, the segments of the morph before the context, the hierarchy of its suffix and the attested deletion.

• context : Phonology.Hiatus.Context
• long : Finset ℕ
• before : List Phonology.Segment
• hierarchy : Hierarchy
• deletion : Finset Data.Hiatus.ElidedVowel

def Vago2017.kindOf : Forms.Kind → Morphology.Morph.Kind

The morph kind of the paper's label.

Equations

• Vago2017.kindOf Vago2017.Forms.Kind.root = Morphology.Morph.Kind.root
• Vago2017.kindOf Vago2017.Forms.Kind.suffix = Morphology.Morph.Kind.bound Morphology.Morph.Position.after Morphology.Morph.Attachment.affix

def Vago2017.hierarchyOf : Forms.Hierarchy → Hierarchy

The hierarchy of the paper's label.

Equations

• Vago2017.hierarchyOf Vago2017.Forms.Hierarchy.regular = Vago2017.Hierarchy.regular
• Vago2017.hierarchyOf Vago2017.Forms.Hierarchy.v1Deletion = Vago2017.Hierarchy.v1Deletion
• Vago2017.hierarchyOf Vago2017.Forms.Hierarchy.noDeletion = Vago2017.Hierarchy.noDeletion

def Vago2017.deletionOf : Forms.Deleted → Finset Data.Hiatus.ElidedVowel

The deleted vowels of the paper's label.

Equations

• Vago2017.deletionOf Vago2017.Forms.Deleted.neither = ∅
• Vago2017.deletionOf Vago2017.Forms.Deleted.first = {Data.Hiatus.ElidedVowel.first}
• Vago2017.deletionOf Vago2017.Forms.Deleted.second = {Data.Hiatus.ElidedVowel.second}

def Vago2017.example? (a : Forms.Analysis) : Option Example

The example the paper's analysis of a form records.

Equations

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

theorem Vago2017.tableaux (a : Forms.Analysis) : a ∈ Forms.analyses → ∃ x ∈ example? a, (tableau x.context x.long x.hierarchy.order).optimal = {x.deletion} ∧ some (x.before ++ resolve x.context x.deletion) = Hungarian.transcribe? a.form.form

For every example, the tableau of its candidates under the hierarchy of its suffix selects the attested deletion, and the form it gives, after the morph before it, spells the attested form.

The ranking that deletes the first vowel

def Vago2017.con (x : Example) : OptimalityTheory.ConstraintSet (Finset Data.Hiatus.ElidedVowel) Con

Vago's constraints on the candidates of an example.

Equations

• Vago2017.con x i D = Vago2017.marks x.context x.long D i

def Vago2017.erdesz : Example

The example erdő-ész of Table 2.

Equations

• Vago2017.erdesz = (Vago2017.example? Vago2017.Forms.erdesz.analysis).get Vago2017.erdesz._proof_2

theorem Vago2017.starVV_dominates_of_erdesz {r : OptimalityTheory.Ranking Con 5} (h : {Data.Hiatus.ElidedVowel.first} ∈ (OptimalityTheory.Tableau.ofPerm (con erdesz) r [∅, {Data.Hiatus.ElidedVowel.first}, {Data.Hiatus.ElidedVowel.second}, {Data.Hiatus.ElidedVowel.first, Data.Hiatus.ElidedVowel.second}] starVV_dominates_of_erdesz._proof_1).optimal) : r.Dominates Con.starVV Con.maxLong ∧ r.Dominates Con.starVV Con.maxLex

A ranking of Vago's constraints under which erdő-ész deletes its first vowel ranks *VV above MAX on long vowels and above MAX LEX, since that vowel is long and in a root.