Uchihara and Mendoza Ruiz (2021): Minimality, Maximality and Perfect Prosodic Word in Alcozauca Mixtec

This file formalizes [UMR21], on the size of the prosodic word in Alcozauca Mixtec. The word is at least bimoraic: monosyllabic stems lengthen, (15), loans acquire a mora, and syncope is accompanied by prothesis. Especially in casual speech it is also at most bimoraic: loans truncate, (45), the perfective prefix is realized by tone alone where a segmental prefix would leave a mora unfooted, (64), and the vowel-initial allomorphs of the enclitics fuse with the stem. The paper's reductionist claim is that both effects follow from the three prosodic-word size restrictor constraints of [McCP94], FOOT-BINARITY, PARSE(µ) and ALL-FEET-RIGHT, ftBin, parseMora, allFeetRight, so that the ideal word is the perfect prosodic word of [IM15], coextensive with one binary foot, IsPerfect: the perfect words are exactly the non-empty words the three restrictors accept, isPerfect_iff, hence a perfect candidate wins under every ranking of the restrictors, isPerfect_mem_optimal, and nothing else does, isPerfect_of_mem_optimal; (15) and (45) are the instances lengthening and truncation. Two asymmetries between the effects follow. PARSE(µ) is gradient in the unfooted moras where FOOT-BINARITY is categorical in each foot, parseMora_cons_inr and ftBin_singleton_le, so [ndi(kiʔĩ)] beats [nindi(kiʔĩ)], and the factorial typology of the restrictors with a general faithfulness constraint yields maximality only together with minimality, (110), while a ranking with ALL-FEET-RIGHT below faithfulness yields minimality and foot alignment without maximality, (111): minimality_of_maximality and exists_minimality_not_maximality.

Implementation notes

Candidates are Prosody.Footings over mora weights, flat parses into feet and stray syllables, and the constraints read them as in [Kag07]; ALL-FEET-RIGHT is categorical, one violation per foot not at the right edge however much intervenes. Faithfulness constraints relate input to output, so the tableaux of the paper are formalized over the restrictors alone, where the paper's optimum is the sole violation-free candidate; the register difference, PARSE(µ) and ALL-FEET-RIGHT dominated by MAXroot, MAX(µ) and NOHIATUS in careful speech and dominating them in casual speech, is not represented. The factorial typology uses the paper's single general faithfulness constraint F, read as the number of moras added to or removed from an input of n moras, faith, over a candidate space of light-syllable footings of up to four moras. The tree-level Prosody.PerfectWord is the headed counterpart of IsPerfect. The forms are the rows of Data.Forms.UchiharaMendozaRuiz2021.

References

• [UMR21]
• [McCP94]
• [IM15]
• [Kag07]
• [dL03]

@[reducible, inline]

abbrev UchiharaMendozaRuiz2021.Word : Type

A syllable is its mora count.

Equations

• UchiharaMendozaRuiz2021.Word = Prosody.Footing Prosody.Syllable.Weight

The prosodic-word size restrictor constraints

def UchiharaMendozaRuiz2021.ftBin : OptimalityTheory.Constraint Word

FOOT-BINARITY: one violation per foot that is not bimoraic.

Equations

• UchiharaMendozaRuiz2021.ftBin fc = (Prosody.Footing.nonBimoraicFeet id fc).length

def UchiharaMendozaRuiz2021.parseMora : OptimalityTheory.Constraint Word

PARSE(µ): one violation per mora parsed into no foot.

Equations

• UchiharaMendozaRuiz2021.parseMora fc = (Prosody.Footing.strays fc).sum

def UchiharaMendozaRuiz2021.allFeetRight : OptimalityTheory.Constraint Word

ALL-FEET-RIGHT: one violation per foot not at the right edge of the word, whatever intervenes.

Equations

• UchiharaMendozaRuiz2021.allFeetRight fc = (Prosody.Footing.feet (List.dropLast fc)).length

def UchiharaMendozaRuiz2021.restrictors : OptimalityTheory.ConstraintSet Word (Fin 3)

The three prosodic-word size restrictor constraints.

Equations

• UchiharaMendozaRuiz2021.restrictors = ![UchiharaMendozaRuiz2021.ftBin, UchiharaMendozaRuiz2021.parseMora, UchiharaMendozaRuiz2021.allFeetRight]

def UchiharaMendozaRuiz2021.IsPerfect (fc : Word) : Prop

The perfect prosodic word: a single bimoraic foot and nothing else.

Equations

• UchiharaMendozaRuiz2021.IsPerfect fc = (Prosody.Footing.strays fc = [] ∧ (Prosody.Footing.feet fc).length = 1 ∧ ∀ f ∈ Prosody.Footing.feet fc, Prosody.Foot.moraCount id f = 2)

@[instance_reducible]

instance UchiharaMendozaRuiz2021.instDecidableIsPerfect (fc : Word) : Decidable (IsPerfect fc)

Equations

• UchiharaMendozaRuiz2021.instDecidableIsPerfect fc = id inferInstance

theorem UchiharaMendozaRuiz2021.IsPerfect.ftBin {fc : Word} (h : IsPerfect fc) : UchiharaMendozaRuiz2021.ftBin fc = 0

theorem UchiharaMendozaRuiz2021.IsPerfect.parseMora {fc : Word} (h : IsPerfect fc) : UchiharaMendozaRuiz2021.parseMora fc = 0

theorem UchiharaMendozaRuiz2021.IsPerfect.allFeetRight {fc : Word} (h : IsPerfect fc) : UchiharaMendozaRuiz2021.allFeetRight fc = 0

theorem UchiharaMendozaRuiz2021.isPerfect_iff {fc : Word} (hpos : ∀ s ∈ Prosody.Footing.strays fc, s ≠ 0) : IsPerfect fc ↔ fc ≠ [] ∧ ftBin fc = 0 ∧ parseMora fc = 0 ∧ allFeetRight fc = 0

The perfect words are exactly the non-empty words the three restrictors accept, given that every stray syllable weighs a mora.

theorem UchiharaMendozaRuiz2021.IsPerfect.restrictors_eq_zero {fc : Word} (h : IsPerfect fc) (i : Fin 3) : restrictors i fc = 0

A perfect word violates none of the restrictors.

theorem UchiharaMendozaRuiz2021.isPerfect_mem_optimal {cands : List Word} {fc : Word} (hc : fc ∈ cands) (h : IsPerfect fc) (r : OptimalityTheory.Ranking (Fin 3) 3) (hne : cands ≠ []) : fc ∈ (OptimalityTheory.Tableau.ofPerm restrictors r cands hne).optimal

A perfect candidate is optimal under every ranking of the restrictors.

theorem UchiharaMendozaRuiz2021.isPerfect_of_mem_optimal {cands : List Word} {fc₀ fc : Word} (hc₀ : fc₀ ∈ cands) (h₀ : IsPerfect fc₀) (hfc : fc ≠ []) (hpos : ∀ s ∈ Prosody.Footing.strays fc, s ≠ 0) (r : OptimalityTheory.Ranking (Fin 3) 3) (hne : cands ≠ []) (hc : fc ∈ (OptimalityTheory.Tableau.ofPerm restrictors r cands hne).optimal) : IsPerfect fc

When some candidate is perfect, only perfect candidates are optimal under the restrictors, whatever their ranking.

Lengthening and truncation

@[reducible, inline]

abbrev UchiharaMendozaRuiz2021.light : Prosody.Syllable.Weight

A light syllable.

Equations

• UchiharaMendozaRuiz2021.light = 1

@[reducible, inline]

abbrev UchiharaMendozaRuiz2021.heavy : Prosody.Syllable.Weight

A heavy syllable.

Equations

• UchiharaMendozaRuiz2021.heavy = 2

def UchiharaMendozaRuiz2021.lengtheningCandidates : List Word

(15): the candidates for /ja/ 'white', the lengthened bimoraic foot (jaa), the degenerate foot (ja) and the unfooted syllable ja.

Equations

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

theorem UchiharaMendozaRuiz2021.lengthening : (OptimalityTheory.Tableau.ofPerm restrictors (Equiv.refl (Fin 3)) lengtheningCandidates lengthening._proof_1).optimal = {[Sum.inl (Prosody.Foot.monosyllable heavy)]}

(15): the lengthened bimoraic foot is the sole optimum.

def UchiharaMendozaRuiz2021.truncationCandidates : List Word

(45): the candidates for Spanish hamaca 'hammock', the truncated bimoraic foot (ma.ka), a(ma.ka) with an unfooted mora, (a.ma)ka with a foot off the right edge, and the trimoraic foot (a.ma.ka).

Equations

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

theorem UchiharaMendozaRuiz2021.truncation : (OptimalityTheory.Tableau.ofPerm restrictors (Equiv.refl (Fin 3)) truncationCandidates truncation._proof_1).optimal = {[Sum.inl (Prosody.Foot.trochee light light)]}

(45): the truncated bimoraic foot is the sole optimum.

Two asymmetries between maximality and minimality

theorem UchiharaMendozaRuiz2021.parseMora_cons_inr (s : Prosody.Syllable.Weight) (fc : Word) : parseMora (Sum.inr s :: fc) = s + parseMora fc

PARSE(µ) is gradient: each unfooted syllable adds its moras.

theorem UchiharaMendozaRuiz2021.ftBin_singleton_le (f : Prosody.Foot Prosody.Syllable.Weight) : ftBin [Sum.inl f] ≤ 1

FOOT-BINARITY is categorical in each foot: a single foot violates it at most once, however far from binary it is.

def UchiharaMendozaRuiz2021.faith (n : ℕ) : OptimalityTheory.Constraint Word

The general faithfulness constraint F of the factorial typology: the moras added to or removed from an input of n moras.

Equations

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

def UchiharaMendozaRuiz2021.constraintsF (n : ℕ) : Fin 4 → OptimalityTheory.Constraint Word

The restrictors with F, for an input of n moras, in the order indexed by a ranking.

Equations

• UchiharaMendozaRuiz2021.constraintsF n = ![UchiharaMendozaRuiz2021.ftBin, UchiharaMendozaRuiz2021.parseMora, UchiharaMendozaRuiz2021.allFeetRight, UchiharaMendozaRuiz2021.faith n]

def UchiharaMendozaRuiz2021.typologyCandidates : List Word

The light-syllable candidates of up to four moras of the tableaux (110) and (111).

Equations

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

def UchiharaMendozaRuiz2021.typologyOptimal (n : ℕ) (r : List (Fin 4)) : Finset Word

The optima for an input of n moras under the ranking r of the four constraints.

Equations

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

def UchiharaMendozaRuiz2021.rankings : List (List (Fin 4))

The rankings of the four constraints.

Equations

• UchiharaMendozaRuiz2021.rankings = [0, 1, 2, 3].permutations'

theorem UchiharaMendozaRuiz2021.minimality_of_maximality (r : List (Fin 4)) : r ∈ rankings → (∀ fc ∈ typologyOptimal 3 r, IsPerfect fc) → (∀ fc ∈ typologyOptimal 4 r, IsPerfect fc) → ∀ fc ∈ typologyOptimal 1 r, IsPerfect fc

(110): every ranking that truncates trimoraic and quadrimoraic inputs to the bimoraic foot lengthens the monomoraic input to it: maximality entails minimality.

theorem UchiharaMendozaRuiz2021.exists_minimality_not_maximality : ∃ r ∈ rankings, (∀ fc ∈ typologyOptimal 1 r, IsPerfect fc) ∧ ¬∀ fc ∈ typologyOptimal 4 r, IsPerfect fc

(111): a ranking with ALL-FEET-RIGHT below faithfulness lengthens the monomoraic input but keeps a quadrimoraic input as two feet: minimality without maximality.