Bennett 2018: recursive prosodic words in Kaqchikel

This file formalizes Bennett's argument that the prosodic word recurses in Kaqchikel. Prefixes fall into two prosodic classes: low-attaching prefixes are parsed into their stem's prosodic word, [ω Pref Stem], and high-attaching prefixes outside it, [ω Pref [ω Stem]]. Two diagnostics converge on the split — an onsetless syllable at the left edge of an ω receives epenthetic [ʔ], so a vowel-initial stem keeps its glottal stop after a high prefix but loses it after a low one, and the OCP that fuses adjacent identical consonants is inert across an ω boundary, so degemination applies across a low-prefix juncture but not a high one. Stacked high prefixes each receive their own glottal stop, which a non-recursive prosodic hierarchy could only reproduce by positing one new prosodic category per prefix. The recursion follows from a lexical subcategorization frame on the high prefixes, ranked above the constraint that every prosodic word correspond to a morphological word.

Main definitions

• flat, nested: the two parses of a prefix sequence over a stem.
• omegaInitial, OmegaSeparates: the structural side of the two diagnostics — the ω-initial leaves, and whether an ω boundary separates two leaves.
• matchWord, matchOmega, subCat: Match (X⁰, ω), Match (ω, X⁰), and the subcategorization frame, as constraints on prosodic trees.

Main results

• omegaInitial_nested, omegaInitial_flat: every stacked high prefix is ω-initial in the recursive parse; only the first prefix is in the flat parse.
• high_prefix_recursive, low_prefix_flat: under SubCat ≫ Match (ω, X⁰) a high-attaching prefix is parsed recursively and a low-attaching one flat.

References

• [Ben18]
• [Sel11]: the Match constraints.
• [Ink90]: prosodic subcategorization.
• [NV86]: the Strict Layer Hypothesis and the Clitic Group.

Parses

def Bennett2018.flat (prefs : List Prosody.Constituent) (stem : Prosody.Constituent) : Prosody.Tree

The flat parse [ω Pref₁ … Prefₙ Stem], the structure of low-attaching prefixes (4a).

Equations

• Bennett2018.flat prefs stem = Prosody.Tree.om (List.map RoseTree.leaf (prefs ++ [stem]))

def Bennett2018.nested : List Prosody.Constituent → Prosody.Constituent → Prosody.Tree

The recursive parse [ω Pref₁ [ω … [ω Prefₙ [ω Stem]]]], one ω per high-attaching prefix ((19a), (23)).

Equations

• Bennett2018.nested [] x✝ = Prosody.Tree.om [RoseTree.leaf x✝]
• Bennett2018.nested (p :: ps) x✝ = Prosody.Tree.om [RoseTree.leaf p, Bennett2018.nested ps x✝]

def Bennett2018.pref : Prosody.Constituent

A light prefix syllable.

Equations

• Bennett2018.pref = Prosody.Constituent.syl 1

def Bennett2018.stem : Prosody.Constituent

A heavy stem syllable.

Equations

• Bennett2018.stem = Prosody.Constituent.syl 2

def Bennett2018.phrasal : Prosody.Tree

Each high-attaching prefix as an independent ω under a higher category (25a), the carrier's φ standing in for a Clitic Group.

Equations

• Bennett2018.phrasal = Prosody.Tree.ph [Prosody.Tree.om [RoseTree.leaf Bennett2018.pref], Prosody.Tree.om [RoseTree.leaf Bennett2018.stem]]

Diagnostics

def Bennett2018.leftmost (t : Prosody.Tree) : Prosody.Constituent

The leftmost leaf of a tree.

Equations

• Bennett2018.leftmost t = (RoseTree.leafList t).head ⋯

def Bennett2018.omegaInitial (t : Prosody.Tree) : List Prosody.Constituent

The ω-initial leaves, one per ω node: the left edge of an ω is where an onsetless syllable receives epenthetic [ʔ], the ω being the domain of syllabification.

Equations

• Bennett2018.omegaInitial t = List.map Bennett2018.leftmost (List.filter (fun (x : RoseTree Prosody.Constituent) => decide (x.value.level = Prosody.Level.om)) (RoseTree.subtrees t))

def Bennett2018.OmegaSeparates (a b : Prosody.Constituent) (t : Prosody.Tree) : Prop

Some ω dominates the leaf b but not the leaf a: an ω boundary between them, across which OCP(X)ω (18) is inert.

Equations

• Bennett2018.OmegaSeparates a b t = ∃ s ∈ RoseTree.subtrees t, s.value.level = Prosody.Level.om ∧ b ∈ s.leafList ∧ a ∉ s.leafList

@[instance_reducible]

instance Bennett2018.instDecidableOmegaSeparates (a b : Prosody.Constituent) (t : Prosody.Tree) : Decidable (OmegaSeparates a b t)

Equations

• Bennett2018.instDecidableOmegaSeparates a b t = Bennett2018.instDecidableOmegaSeparates._aux_1 a b t

theorem Bennett2018.omegaInitial_nested {ps : List Prosody.Constituent} {s : Prosody.Constituent} (hps : ∀ p ∈ ps, p.level ≠ Prosody.Level.om) (hs : s.level ≠ Prosody.Level.om) : omegaInitial (nested ps s) = ps ++ [s]

In the recursive parse every stacked prefix and the stem is ω-initial: n high prefixes over a vowel-initial stem give n + 1 loci of [ʔ]-insertion ((21)–(23)).

theorem Bennett2018.omegaInitial_flat {p : Prosody.Constituent} {ps : List Prosody.Constituent} {s : Prosody.Constituent} (hp : p.level ≠ Prosody.Level.om) (hps : ∀ q ∈ ps, q.level ≠ Prosody.Level.om) (hs : s.level ≠ Prosody.Level.om) : omegaInitial (flat (p :: ps) s) = [p]

In the flat parse only the first prefix is ω-initial: one locus of [ʔ]-insertion.

Constraints and the ranking

def Bennett2018.matchWord : OptimalityTheory.Constraint Prosody.Tree

Match (X⁰, ω) (13) for a single morphological word: a violation unless one ω dominates all of its segments, i.e. unless the root is an ω. Undominated in Kaqchikel.

Equations

• Bennett2018.matchWord t = if (RoseTree.value t).level = Prosody.Level.om then 0 else 1

def Bennett2018.matchOmega : OptimalityTheory.Constraint Prosody.Tree

Match (ω, X⁰) for a single morphological word: every ω other than a root ω fails to correspond to a morphological word.

Equations

• Bennett2018.matchOmega t = List.countP (fun (x : Prosody.Constituent) => decide (x.level = Prosody.Level.om)) (RoseTree.values t) - if (RoseTree.value t).level = Prosody.Level.om then 1 else 0

def Bennett2018.hasFrame (p : Prosody.Constituent) (t : Prosody.Tree) : Bool

Whether the leaf p is the left sister of an ω inside an ω: the subcategorization frame [ω p [ω ]] (30) is realised.

Equations

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

def Bennett2018.subCat (prefs : List Prosody.Constituent) : OptimalityTheory.Constraint Prosody.Tree

SubCat: one violation per high-attaching prefix whose frame (30) is not realised.

Equations

• Bennett2018.subCat prefs t = (List.filter (fun (p : Prosody.Constituent) => !Bennett2018.hasFrame p t) prefs).length

theorem Bennett2018.high_prefix_recursive : (OptimalityTheory.Tableau.ofRanking [nested [pref] stem, flat [pref] stem, phrasal] [matchWord, subCat [pref], matchOmega] high_prefix_recursive._proof_1).optimal = {nested [pref] stem}

A high-attaching prefix is parsed recursively: under SubCat ≫ Match (ω, X⁰), with Match (X⁰, ω) undominated, the recursive parse is the unique optimum.

theorem Bennett2018.low_prefix_flat : (OptimalityTheory.Tableau.ofRanking [nested [pref] stem, flat [pref] stem, phrasal] [matchWord, matchOmega] high_prefix_recursive._proof_1).optimal = {flat [pref] stem}

A low-attaching prefix, carrying no frame, is parsed flat: Match (ω, X⁰) alone rules out the extra ω.