Prosodic words (ω)

[Sel80] [NV86] [LP77] [Hay95a] [IM09] [McCP93] [Sel96] [IM03] [PS93] [Dol20]

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 ([Sel96]): an ω-node whose daughters are only feet, recursive sub-words (ω-over-ω), or stray (unfooted) syllables — the inviolable Layeredness constraint (no φ/ι/AP inside an ω). The library's 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-ω (the extended prosodic word of [IM09]) are both admitted. They are scored on the carrier by parseInto/noRec and ranked by a grammar — that is where they belong. Headedness (that an ω dominates a foot, the minimal-word effect of [Sel96]) is the typical case but is not presupposed: footless languages have ω directly over σ (DeLisi 2015, per [Dol20]), and the OT recursion candidates here abstract the foot level. Prominence-head marking is likewise a refinement, not enforced.

Main definitions

• isWordTree — the structural Bool Layeredness checker (decide-reducible; the foot arm reuses Foot.isFootTree).
• IsWord — the Layeredness predicate; 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 / IsMinimalProj — the topmost / bottommost ℓ-nodes of the carrier, and the intrinsic minimal-projection predicate.
• feet / moraCount / unfootedCount — carrier folds extracting feet, morae, stray σ.
• MinimalWord / MaximalWord / PerfectWord — the word-size notions over the carrier.

Main results

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

Prosodic OT constraints over the Tree carrier

The violable constraints scoring prosodic candidates are Constraints.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 : Constraints.Constraint Tree

No-Recursion ([IM09]): 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) => c.value.sameLevel a) 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 the same family of carrier folds as noRec — noRec looks at same-level parent–child pairs, the projections at the extremal same-level nodes. The maximal ℓ-projections are the topmost ℓ-nodes (no ℓ-ancestor), read off by an under-flag fold (cf. parseInto) that prunes a subtree once the first ℓ is hit; the minimal ℓ-projections are the bottommost ℓ-nodes (no ℓ-descendant). The asymmetry is intentional: maximality is context-relative (membership in maximalProjections ℓ root), whereas minimality is intrinsic to a node (IsMinimalProj), so only the latter carries a one-argument predicate. The intonational utterance υ is just the maximal ι-projection. List (not Finset) keeps the duplicate-position counts that Match-style correspondence ([Sel96]) reads.

def Prosody.maximalProjections (p : Constituent → Bool) (t : Tree) : List Tree

The maximal projections of t selected by p: the topmost p-nodes (those with no p-ancestor), in tree order. A top-down under-flag fold (cf. parseInto) pruning a subtree once the first p-node is hit.

Equations

• Prosody.maximalProjections p t = Prosody.maximalProjections.go p false t

def Prosody.maximalProjections.go (p : Constituent → Bool) (under : Bool) : Tree → List Tree

Equations

• Prosody.maximalProjections.go p under (RoseTree.node a cs) = if (!under && p a) = true then [RoseTree.node a cs] else Prosody.maximalProjections.goList p (under || p a) cs

def Prosody.maximalProjections.goList (p : Constituent → Bool) (under : Bool) : List Tree → List Tree

Equations

• Prosody.maximalProjections.goList p under [] = []
• Prosody.maximalProjections.goList p under (c :: cs) = Prosody.maximalProjections.go p under c ++ Prosody.maximalProjections.goList p under cs

def Prosody.anyAtLevel (p : Constituent → Bool) : Tree → Bool

A p-node occurs somewhere in t (the root included).

Equations

• Prosody.anyAtLevel p = Prosody.anyAtLevel.go p

def Prosody.anyAtLevel.go (p : Constituent → Bool) : Tree → Bool

Equations

• Prosody.anyAtLevel.go p (RoseTree.node a cs) = (p a || Prosody.anyAtLevel.goList p cs)

def Prosody.anyAtLevel.goList (p : Constituent → Bool) : List Tree → Bool

Equations

• Prosody.anyAtLevel.goList p [] = false
• Prosody.anyAtLevel.goList p (c :: cs) = (Prosody.anyAtLevel.go p c || Prosody.anyAtLevel.goList p cs)

def Prosody.isMinimalProj (p : Constituent → Bool) : Tree → Bool

The intrinsic minimal-p test: a p-node no proper descendant of which is a p-node.

Equations

• Prosody.isMinimalProj p (RoseTree.node a cs) = (p a && !cs.any (Prosody.anyAtLevel p))

def Prosody.minimalProjections (p : Constituent → Bool) (t : Tree) : List Tree

The minimal projections of t selected by p: the bottommost p-nodes (those with no p-descendant), in tree order.

Equations

• Prosody.minimalProjections p t = Prosody.minimalProjections.go p t

def Prosody.minimalProjections.go (p : Constituent → Bool) : Tree → List Tree

Equations

• Prosody.minimalProjections.go p (RoseTree.node a cs) = (if Prosody.isMinimalProj p (RoseTree.node a cs) = true then [RoseTree.node a cs] else []) ++ Prosody.minimalProjections.goList p cs

def Prosody.minimalProjections.goList (p : Constituent → Bool) : List Tree → List Tree

Equations

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

def Prosody.IsMinimalProj (p : Constituent → Bool) (t : Tree) : Prop

A minimal p-projection: a p-node none of whose proper descendants is a p-node — the intrinsic, context-free dual of (context-relative) maximality.

Equations

• Prosody.IsMinimalProj p t = (Prosody.isMinimalProj p t = true)

@[implicit_reducible]

instance Prosody.instDecidableIsMinimalProj (p : Constituent → Bool) (t : Tree) : Decidable (IsMinimalProj p t)

Equations

• Prosody.instDecidableIsMinimalProj p t = Prosody.instDecidableIsMinimalProj._aux_1 p t

def Prosody.noLevelRec (p : Constituent → Bool) : Tree → Bool

Transitive No-Recursion at ℓ: no ℓ-node properly dominates an ℓ-node — every ℓ-node is a minimal projection. This — not noRec — is what collapses the maximal and minimal ℓ-projections (noLevelRec_imp_max_eq_min): noRec t = 0 forbids only direct ℓ-over-ℓ, while ω(f(ω)) recurses through an intervening foot (noRec = 0, yet maximal ≠ minimal); the one-step noRec is the shadow this casts on the strictly-layered trees IsWord carves out.

Equations

• Prosody.noLevelRec p = Prosody.noLevelRec.go p

def Prosody.noLevelRec.go (p : Constituent → Bool) : Tree → Bool

Equations

• Prosody.noLevelRec.go p (RoseTree.node a cs) = ((!p a || Prosody.isMinimalProj p (RoseTree.node a cs)) && Prosody.noLevelRec.goList p cs)

def Prosody.noLevelRec.goList (p : Constituent → Bool) : List Tree → Bool

Equations

• Prosody.noLevelRec.goList p [] = true
• Prosody.noLevelRec.goList p (c :: cs) = (Prosody.noLevelRec.go p c && Prosody.noLevelRec.goList p cs)

Properties

Each where-aux goList is the matching List combinator over its go (flatMap/any/all), proved once below so every projection lemma is a single Branching.inductionOn over the carrier (the principle Tree already rides, Core/Order/Branching.lean) plus standard List reasoning.

theorem Prosody.mem_maximalProjections_level {p : Constituent → Bool} {s t : Tree} (h : s ∈ maximalProjections p t) : p (RoseTree.value s) = true

Every maximal p-projection is a p-node.

theorem Prosody.isMinimalProj_of_mem_minimalProjections {p : Constituent → Bool} {s t : Tree} (h : s ∈ minimalProjections p t) : IsMinimalProj p s

Minimality is intrinsic: a node returned as a minimal ℓ-projection of any tree is itself a minimal ℓ-projection (IsMinimalProj) — it does not depend on the ambient tree. The maximal/minimal asymmetry: a node is maximal only relative to an ambient tree (its ℓ-ancestors), but minimal in itself.

theorem Prosody.isMinimalProj_level {p : Constituent → Bool} {s : Tree} (h : IsMinimalProj p s) : p (RoseTree.value s) = true

A minimal p-projection is a p-node.

theorem Prosody.mem_minimalProjections_level {p : Constituent → Bool} {s t : Tree} (h : s ∈ minimalProjections p t) : p (RoseTree.value s) = true

Every minimal p-projection is a p-node.

theorem Prosody.noLevelRec_imp_max_eq_min {p : Constituent → Bool} {t : Tree} (h : noLevelRec p t = true) : maximalProjections p t = minimalProjections p t

No-Recursion collapses the projections. Under transitive No-Recursion at ℓ (noLevelRec: no ℓ-node properly dominates an ℓ-node), the topmost and bottommost ℓ-nodes coincide — every ℓ-node is at once maximal and minimal. The naive noRec t = 0 (no direct ℓ-over-ℓ) does not suffice — ω(f(ω)) has noRec = 0 yet maximal ≠ minimal — but on the strictly-layered words IsWord cuts out, the two conditions agree.

def Prosody.parseInto (p : Constituent → Bool) : Constraints.Constraint Tree

Parse-into-p ([IM03]): σ-leaves dominated by no p-node.

Equations

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

def Prosody.parseInto.go (p : Constituent → Bool) (under : Bool) : Tree → ℕ

Equations

• Prosody.parseInto.go p under (RoseTree.node a cs) = (if (a.isSyl && cs.isEmpty && !(under || p a)) = true then 1 else 0) + Prosody.parseInto.goList p (under || p a) cs

def Prosody.parseInto.goList (p : Constituent → Bool) (under : Bool) : List Tree → ℕ

Equations

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

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

The feet of a prosodic tree: the σ-weight content of every f-node.

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.isFt = true 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 (·.isFt).

Equations

• Prosody.unfootedCount t = Prosody.parseInto (fun (x : Prosody.Constituent) => x.isFt) t

def Prosody.moraCount : Tree → ℕ

Total mora count: 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 ω

isWordTree is the structural Bool realization of the inviolable Layeredness core ([Sel96]); IsWord is the declarative predicate it backs, and Word the carrier subtype. Both checkers mirror the go/goList structural recursion of noRec, so they are decide-reducible — a winner can be certified IsWord by decide.

def Prosody.isWordTree : Tree → Bool

The structural Layeredness checker: an ω-node every daughter of which is a well-formed foot (isFootTree, in Foot), a recursive ω (the ω-over-ω arm), or a stray σ-leaf.

Equations

• Prosody.isWordTree t = Prosody.isWordTree.go t

def Prosody.isWordTree.go : Tree → Bool

Equations

• Prosody.isWordTree.go (RoseTree.node a cs) = (a.isOm && Prosody.isWordTree.goList cs)

def Prosody.isWordTree.goList : List Tree → Bool

Equations

• Prosody.isWordTree.goList [] = true
• Prosody.isWordTree.goList (c :: cs) = ((Prosody.isFootTree c || Prosody.isWordTree.go c || (RoseTree.value c).isSyl && (RoseTree.children c).isEmpty) && Prosody.isWordTree.goList cs)

def Prosody.IsWord (t : Tree) : Prop

A well-formed prosodic word: an ω-node dominating only feet, recursive ω's, and stray σ — never φ/ι. This is the inviolable Layeredness core. Headedness (a foot daughter — the minimal-word effect, [Sel96]) is the typical case but is not presupposed: 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 t = (Prosody.isWordTree t = true)

@[implicit_reducible]

instance Prosody.instDecidableIsWord (t : Tree) : Decidable (IsWord t)

Equations

• Prosody.instDecidableIsWord t = Prosody.instDecidableIsWord._aux_1 t

theorem Prosody.isWordTree.goList_all (cs : List Tree) : goList cs = cs.all fun (c : Tree) => isFootTree c || go c || (RoseTree.value c).isSyl && (RoseTree.children c).isEmpty

isWordTree.goList as a List.all over children.

theorem Prosody.isWord_children {a : Constituent} {cs : List Tree} (hw : IsWord (RoseTree.node a cs)) (hr : noRec (RoseTree.node a cs) = 0) : a.isOm = true ∧ ∀ c ∈ cs, isFootTree c = true ∨ (RoseTree.value c).isSyl = true ∧ 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

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

Equations

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

@[implicit_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

Maximal word ([UMR21]): ≤ one well-formed foot, 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)

@[implicit_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]): ω 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)

@[implicit_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