Prosodic words (ω)

A prosodic word ω is a node of the prosodic tree (Prosody.Tree), and well-formedness is a declarative property of that carrier rather than a separate inductive. IsWord carves out the well-formed ω-trees as the Strict-Layer core (Selkirk 1996): an ω-node whose daughters are only feet, recursive sub-words, or stray syllables, the inviolable Layeredness constraint. The OT studies score raw Tree candidates, so theorems take IsWord as a hypothesis on the carrier rather than bundling a subtype.

Exhaustivity and No-Recursion are violable OT constraints, not part of IsWord: a stray σ (a free clitic) and an ω-over-ω (Itô and Mester's 2009 extended prosodic word) are both admitted, and parseInto and noRec score them on the carrier. Headedness, that an ω dominates a foot, is the typical case but is not presupposed: footless languages have ω directly over σ (DeLisi 2015, per Dolatian 2020).

Main definitions

• IsWord — the Layeredness predicate, a tree rooted in an ω-node and licensed by Constituent.Licenses; theorems take it as a hypothesis on the carrier (mathlib's Squarefree-style), there is no bundled subtype.
• noRec / parseInto — the violable OT constraints over the carrier (Constraint Tree).
• maximalProjections / minimalProjections — the topmost / bottommost ℓ-positions, Minimal and Maximal under dominance; NoLevelRecursion — the ℓ-positions form an antichain.
• feet / moraCount / unfootedCount — carrier folds extracting feet, morae, stray σ.
• MinimalWord / MaximalWord / PerfectWord — the word-size notions over the carrier.

Main results

• maximalProjections_eq_minimalProjections — under transitive No-Recursion at ℓ, the maximal and minimal ℓ-projections coincide (every ℓ-node is at once topmost and bottommost).

References

• [Sel80]
• [NV86]
• [LP77]
• [Hay95b]
• [McCP93]
• [PS93]
• [Sel96]
• [IM03]
• [IM09]
• [Dol20]
• [UMR21]

Prosodic OT constraints over the Tree carrier

The violable constraints scoring prosodic candidates are OptimalityTheory.Constraint Tree values ([PS93]); a grammar ranks them and scores with the OT engine (OptimalityTheory.Tableau.ofRanking). They are defined on the carrier Tree (which holds the ill-formed candidates IsWord rules out). List-recursion auxes are local wheres.

def Prosody.noRec : OptimalityTheory.Constraint Tree

No-Recursion ([IM09]) counts parent–child pairs sharing a level, an element parsed into the same category twice.

Equations

• Prosody.noRec t = Prosody.noRec.go t

def Prosody.noRec.go : Tree → ℕ

Equations

• Prosody.noRec.go (RoseTree.node a cs) = (List.filter (fun (c : RoseTree Prosody.Constituent) => decide (c.value.level = a.level)) cs).length + Prosody.noRec.goList cs

def Prosody.noRec.goList : List Tree → ℕ

Equations

• Prosody.noRec.goList [] = 0
• Prosody.noRec.goList (c :: cs) = Prosody.noRec.go c + Prosody.noRec.goList cs

Maximal and minimal projections

The projections of a level ℓ ([IM09]) are its extremal nodes under dominance. The maximal ℓ-projections are the ℓ-nodes no ℓ-node dominates, and the minimal ones are the ℓ-nodes dominating no ℓ-node. Since the root is the least position, these are the Minimal and Maximal members of the ℓ-positions. Transitive No-Recursion at ℓ, that no ℓ-node properly dominates another, says that the ℓ-positions form an antichain, and it collapses the two. noRec scores only a direct ℓ-over-ℓ, so ω(f(ω)), which recurses through an intervening foot, has noRec = 0 while its maximal and minimal ω-projections differ. The intonational utterance υ is the maximal ι-projection.

@[reducible, inline]

abbrev Prosody.levelPositions (ℓ : Level) (t : Tree) : Set Core.Order.TreePath

The positions of t at the level ℓ.

Equations

• Prosody.levelPositions ℓ t = RoseTree.positionsWhere (fun (s : RoseTree Prosody.Constituent) => s.value.level = ℓ) t

@[reducible, inline]

abbrev Prosody.maximalProjections (ℓ : Level) (t : Tree) : Set Core.Order.TreePath

The maximal ℓ-projections of t, its topmost ℓ-nodes.

Equations

• Prosody.maximalProjections ℓ t = {p : Core.Order.TreePath | Minimal (fun (x : Core.Order.TreePath) => x ∈ Prosody.levelPositions ℓ t) p}

@[reducible, inline]

abbrev Prosody.minimalProjections (ℓ : Level) (t : Tree) : Set Core.Order.TreePath

The minimal ℓ-projections of t, its bottommost ℓ-nodes.

Equations

• Prosody.minimalProjections ℓ t = {p : Core.Order.TreePath | Maximal (fun (x : Core.Order.TreePath) => x ∈ Prosody.levelPositions ℓ t) p}

@[reducible, inline]

abbrev Prosody.NoLevelRecursion (ℓ : Level) (t : Tree) : Prop

Transitive No-Recursion at ℓ: no ℓ-node of t properly dominates another.

Equations

• Prosody.NoLevelRecursion ℓ t = IsAntichain (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) (Prosody.levelPositions ℓ t)

theorem Prosody.maximalProjections_eq_minimalProjections {ℓ : Level} {t : Tree} (h : NoLevelRecursion ℓ t) : maximalProjections ℓ t = minimalProjections ℓ t

No-Recursion collapses the projections: under transitive No-Recursion at ℓ, every ℓ-node is at once topmost and bottommost.

def Prosody.parseInto (ℓ : Level) : OptimalityTheory.Constraint Tree

Parse-into-ℓ ([IM03]) counts σ-leaves dominated by no ℓ-node.

Equations

• Prosody.parseInto ℓ t = Prosody.parseInto.go ℓ false t

def Prosody.parseInto.go (ℓ : Level) (under : Bool) : Tree → ℕ

Equations

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

def Prosody.parseInto.goList (ℓ : Level) (under : Bool) : List Tree → ℕ

Equations

• Prosody.parseInto.goList ℓ under [] = 0
• Prosody.parseInto.goList ℓ under (c :: cs) = Prosody.parseInto.go ℓ under c + Prosody.parseInto.goList ℓ under cs

def Prosody.footContent (cs : List Tree) : List Syllable.Weight

The σ-weight content of a foot node's direct σ-daughters.

Equations

• Prosody.footContent cs = List.filterMap (fun (c : Prosody.Tree) => match c with | RoseTree.node a [] => a.weight? | x => none) cs

def Prosody.feet : Tree → List (List Syllable.Weight)

The feet of a prosodic tree are the σ-weight contents of its f-nodes.

Equations

• Prosody.feet t = Prosody.feet.go t

def Prosody.feet.go : Tree → List (List Syllable.Weight)

Equations

• Prosody.feet.go (RoseTree.node a cs) = (if a.level = Prosody.Level.ft then [Prosody.footContent cs] else []) ++ Prosody.feet.goList cs

def Prosody.feet.goList : List Tree → List (List Syllable.Weight)

Equations

• Prosody.feet.goList [] = []
• Prosody.feet.goList (c :: cs) = Prosody.feet.go c ++ Prosody.feet.goList cs

def Prosody.unfootedCount (t : Tree) : ℕ

Syllables parsed into no foot — parseInto .ft.

Equations

• Prosody.unfootedCount t = Prosody.parseInto Prosody.Level.ft t

def Prosody.moraCount : Tree → ℕ

The total mora count is the sum of the tree's σ-weights.

Equations

• Prosody.moraCount t = Prosody.moraCount.go t

def Prosody.moraCount.go : Tree → ℕ

Equations

• Prosody.moraCount.go (RoseTree.node a cs) = a.weight?.getD 0 + Prosody.moraCount.goList cs

def Prosody.moraCount.goList : List Tree → ℕ

Equations

• Prosody.moraCount.goList [] = 0
• Prosody.moraCount.goList (c :: cs) = Prosody.moraCount.go c + Prosody.moraCount.goList cs

The well-formed prosodic word ω

IsWord is the inviolable Layeredness core ([Sel96]): a tree rooted in an ω-node and licensed by Constituent.Licenses. Licensing is decidable by structural recursion, so a winner can be certified IsWord by decide.

@[reducible, inline]

abbrev Prosody.IsWord : Tree → Prop

A well-formed prosodic word is a licensed tree rooted in an ω-node, so an ω-node dominating only feet, recursive ω's, and stray σ, never φ or ι. This is the inviolable Layeredness core. Headedness (a foot daughter, the minimal-word effect of [Sel96]) is the typical case but is not presupposed, since footless languages have ω directly over σ (DeLisi 2015, per [Dol20]) and the OT recursion candidates abstract the foot level. Exhaustivity (a stray σ) and Nonrecursivity (ω-over-ω) are violable OT constraints, so both are admitted here.

Equations

• Prosody.IsWord = Prosody.IsConstituent Prosody.Level.om

theorem Prosody.isWord_children {a : Constituent} {cs : List Tree} (hw : IsWord (RoseTree.node a cs)) (hr : noRec (RoseTree.node a cs) = 0) : a.level = Level.om ∧ ∀ c ∈ cs, IsFoot c ∨ (RoseTree.value c).level = Level.syl ∧ RoseTree.children c = []

A non-recursive word is an ω over well-formed feet and stray σ-leaves, the structural content of IsWord ∧ noRec = 0, used to read the grid off a word.

Word-size predicates

def Prosody.MinimalWord (measure : List Syllable.Weight → ℕ) (t : Tree) : Prop

A minimal word ([McCP93]) contains a well-formed foot (PrWd ⊇ Ft).

Equations

• Prosody.MinimalWord measure t = ∃ f ∈ Prosody.feet t, measure f = 2

@[instance_reducible]

instance Prosody.instDecidableMinimalWord {measure : List Syllable.Weight → ℕ} {t : Tree} : Decidable (MinimalWord measure t)

Equations

• Prosody.instDecidableMinimalWord = id inferInstance

def Prosody.MaximalWord (measure : List Syllable.Weight → ℕ) (t : Tree) : Prop

A maximal word ([UMR21]) has at most one well-formed foot and is exhaustively parsed, the upper size bound.

Equations

• Prosody.MaximalWord measure t = ((Prosody.feet t).length ≤ 1 ∧ Prosody.unfootedCount t = 0 ∧ ∀ f ∈ Prosody.feet t, measure f = 2)

@[instance_reducible]

instance Prosody.instDecidableMaximalWord {measure : List Syllable.Weight → ℕ} {t : Tree} : Decidable (MaximalWord measure t)

Equations

• Prosody.instDecidableMaximalWord = id inferInstance

def Prosody.PerfectWord (measure : List Syllable.Weight → ℕ) (t : Tree) : Prop

The perfect prosodic word ([IM09]) is an ω coextensive with one well-formed foot.

Equations

• Prosody.PerfectWord measure t = ((Prosody.feet t).length = 1 ∧ (∀ f ∈ Prosody.feet t, measure f = 2) ∧ Prosody.unfootedCount t = 0)

@[instance_reducible]

instance Prosody.instDecidablePerfectWord {measure : List Syllable.Weight → ℕ} {t : Tree} : Decidable (PerfectWord measure t)

Equations

• Prosody.instDecidablePerfectWord = id inferInstance

theorem Prosody.PerfectWord.minimal {measure : List Syllable.Weight → ℕ} {t : Tree} (h : PerfectWord measure t) : MinimalWord measure t

A perfect word is minimal.

theorem Prosody.PerfectWord.maximal {measure : List Syllable.Weight → ℕ} {t : Tree} (h : PerfectWord measure t) : MaximalWord measure t

A perfect word is maximal.

theorem Prosody.perfectWord_iff_minimal_and_maximal {measure : List Syllable.Weight → ℕ} {t : Tree} : PerfectWord measure t ↔ MinimalWord measure t ∧ MaximalWord measure t

The perfect word is exactly minimal-and-maximal.

theorem Prosody.MaximalWord.minimal {measure : List Syllable.Weight → ℕ} {t : Tree} (hne : feet t ≠ []) (h : MaximalWord measure t) : MinimalWord measure t

Maximality entails minimality for a footed word ([UMR21]).

Worked examples