Metrical feet

The canonical metrical foot (Selkirk 1980; Nespor and Vogel 1986; Hayes 1995; Kager 1999) is a flat, headed constituent over syllable positions: a non-empty, ordered sequence of syllables with one distinguished head, the stressed daughter. Headedness (trochaic or iambic), binarity, and the trochee, iamb and moraic inventory are derived from the structure, not stored, and the moraic versus syllabic split is a counting parameter on moraCount. Re-representations into the prosodic tree (Prosody.Tree) and the metrical grid are functions that recover the same head.

Main definitions

• IsConstituent — well-formedness at a prosodic level on the prosodic-tree carrier: a tree rooted at that level and licensed by the Layeredness relation Constituent.Licenses; IsFoot is the f level, an f-node over a non-empty list of σ-leaves.
• Foot — a headed constituent over syllable positions (head : Fin _, so non-empty).
• Foot.IsTrochaic / IsIambic / IsBinary / IsDegenerate — derived shape predicates.
• Foot.moraCount — mora count under a weight reading (the quantity axis).
• Foot.IsSyllabicTrochee / IsMoraicTrochee / IsCanonicalIamb — the derived inventory.
• Foot.toProsTree / Foot.toGrid / Foot.headFlags — re-representations that preserve the head (the prosodic tree, its metrical grid, and its head-flag row).
• footMorae — mora count of a Tree-extracted weight-list foot (the flat metrical parse is now Prosody.Footing).
• Footing.footOffsets / Footing.nonBimoraicFeet — each foot's left-edge position and the feet failing bimoraicity: what the alignment and binarity constraints count.

Main results

• Foot.itl_gap — the Iambic/Trochaic Law (Hayes 1985): a binary iamb need not be weight-blind-characterizable, unlike a binary (syllabic) trochee.
• Foot.headFlags_toProsTree — the prosodic-tree re-representation carries the same head profile as headFlags (head-preservation, the functorial spine).
• Foot.isFoot_toProsTree — every Foot's prosodic tree is a well-formed foot tree (IsFoot): the functoriality/well-formedness bridge onto the carrier.

References

• [Sel80]
• [NV86]
• [Hay85]
• [Hay95b]
• [Kag99]
• [Kag07]
• [IM03]
• [MPK15]
• [Lam22b]

Carrier well-formedness

def Prosody.IsConstituent (ℓ : Level) (t : Tree) : Prop

A well-formed prosodic constituent at the level ℓ is a tree rooted in an ℓ-node and licensed by Constituent.Licenses, so every node dominates only the levels Layeredness allows under it.

Equations

• Prosody.IsConstituent ℓ t = ((RoseTree.value t).level = ℓ ∧ RoseTree.Licensed Prosody.Constituent.Licenses t)

@[instance_reducible]

instance Prosody.instDecidableIsConstituent (ℓ : Level) (t : Tree) : Decidable (IsConstituent ℓ t)

Equations

• Prosody.instDecidableIsConstituent ℓ t = { decide := decide ((RoseTree.value t).level = ℓ) && decide (RoseTree.Licensed Prosody.Constituent.Licenses t), reflects_decide := ⋯ }

@[reducible, inline]

abbrev Prosody.IsFoot : Tree → Prop

A well-formed foot is a licensed tree rooted in an f-node, so an f-node dominating a non-empty list of σ-leaves, the inviolable Layeredness and σ-Headedness core ([Sel80]; [Hay95b]). Foot binarity (FtBin) and recursive internally-layered feet (contested, Golston 2021 against [MPK15]) are violable and deferred; these are flat feet, the sibling of IsWord's Layeredness.

Equations

• Prosody.IsFoot = Prosody.IsConstituent Prosody.Level.ft

theorem Prosody.IsFoot.syl_leaf {t : Tree} (h : IsFoot t) {c : Tree} (hc : c ∈ RoseTree.children t) : (RoseTree.value c).level = Level.syl ∧ RoseTree.children c = []

The daughters of a well-formed foot are σ-leaves.

The canonical foot

structure Prosody.Foot (S : Type u_1) : Type u_1

The canonical metrical foot ([Sel80]; [Hay95b]; [Kag99]) is a non-empty, ordered sequence of syllable positions with one distinguished head, the stressed daughter. The Fin index forces non-emptiness by construction. The inventory and headedness are derived below, not stored.

• syllables : List S

  The dominated syllable positions, left to right.

• head : Fin self.syllables.length

  The distinguished (stressed) daughter; the Fin index forces non-emptiness.

def Prosody.instDecidableEqFoot.decEq {S✝ : Type u_1} [DecidableEq S✝] (x✝ x✝¹ : Foot S✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Prosody.instDecidableEqFoot {S✝ : Type u_1} [DecidableEq S✝] : DecidableEq (Foot S✝)

Equations

• Prosody.instDecidableEqFoot = Prosody.instDecidableEqFoot.decEq

@[instance_reducible]

instance Prosody.instReprFoot {S✝ : Type u_1} [Repr S✝] : Repr (Foot S✝)

Equations

• Prosody.instReprFoot = { reprPrec := Prosody.instReprFoot.repr }

def Prosody.instReprFoot.repr {S✝ : Type u_1} [Repr S✝] : Foot S✝ → ℕ → Std.Format

Equations

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

def Prosody.Foot.length {S : Type u_1} (f : Foot S) : ℕ

The number of dominated syllables.

Equations

• f.length = f.syllables.length

def Prosody.Foot.monosyllable {S : Type u_1} (a : S) : Foot S

A monosyllabic foot (σ́).

Equations

• Prosody.Foot.monosyllable a = { syllables := [a], head := 0 }

def Prosody.Foot.trochee {S : Type u_1} (a b : S) : Foot S

A head-initial disyllable (σ́σ) — trochaic.

Equations

• Prosody.Foot.trochee a b = { syllables := [a, b], head := 0 }

def Prosody.Foot.iamb {S : Type u_1} (a b : S) : Foot S

A head-final disyllable (σσ́) — iambic.

Equations

• Prosody.Foot.iamb a b = { syllables := [a, b], head := 1 }

Derived shape predicates

def Prosody.Foot.IsTrochaic {S : Type u_1} (f : Foot S) : Prop

Head-initial (trochaic).

Equations

• f.IsTrochaic = (↑f.head = 0)

def Prosody.Foot.IsIambic {S : Type u_1} (f : Foot S) : Prop

Head-final (iambic).

Equations

• f.IsIambic = (↑f.head + 1 = f.syllables.length)

def Prosody.Foot.IsBinary {S : Type u_1} (f : Foot S) : Prop

A binary (disyllabic) foot.

Equations

• f.IsBinary = (f.syllables.length = 2)

def Prosody.Foot.IsDegenerate {S : Type u_1} (f : Foot S) : Prop

A degenerate (monosyllabic) foot.

Equations

• f.IsDegenerate = (f.syllables.length = 1)

@[instance_reducible]

instance Prosody.Foot.instDecidableIsTrochaic {S : Type u_1} (f : Foot S) : Decidable f.IsTrochaic

Equations

• f.instDecidableIsTrochaic = id inferInstance

@[instance_reducible]

instance Prosody.Foot.instDecidableIsIambic {S : Type u_1} (f : Foot S) : Decidable f.IsIambic

Equations

• f.instDecidableIsIambic = id inferInstance

@[instance_reducible]

instance Prosody.Foot.instDecidableIsBinary {S : Type u_1} (f : Foot S) : Decidable f.IsBinary

Equations

• f.instDecidableIsBinary = id inferInstance

@[instance_reducible]

instance Prosody.Foot.instDecidableIsDegenerate {S : Type u_1} (f : Foot S) : Decidable f.IsDegenerate

Equations

• f.instDecidableIsDegenerate = id inferInstance

theorem Prosody.Foot.not_trochaic_and_iambic {S : Type u_1} (f : Foot S) (h : 1 < f.syllables.length) : ¬(f.IsTrochaic ∧ f.IsIambic)

Above the monosyllable headedness is exclusive, so a foot is not both trochaic and iambic (at length 1 the sole σ is both head-initial and head-final).

Quantity and the derived inventory

def Prosody.Foot.moraCount {S : Type u_1} (w : S → ℕ) (f : Foot S) : ℕ

Mora count under a weight reading w — the quantity axis the moraic/syllabic split parameterizes (FtBin-by-μ).

Equations

• Prosody.Foot.moraCount w f = (List.map w f.syllables).sum

def Prosody.Foot.IsSyllabicTrochee {S : Type u_1} (f : Foot S) : Prop

A syllabic trochee (σ́σ) is head-initial and binary, weight-blind ([Hay95b]).

Equations

• f.IsSyllabicTrochee = (f.IsTrochaic ∧ f.IsBinary)

def Prosody.Foot.IsMoraicTrochee {S : Type u_1} (w : S → ℕ) (f : Foot S) : Prop

A moraic trochee (H) or (LL) is head-initial and bimoraic ([Hay95b]).

Equations

• Prosody.Foot.IsMoraicTrochee w f = (f.IsTrochaic ∧ Prosody.Foot.moraCount w f = 2)

def Prosody.Foot.IsCanonicalIamb {S : Type u_1} (w : S → ℕ) (f : Foot S) : Prop

A canonical iamb over Hayes' right-prominent inventory {(H),(LL),(LH)} ([Hay95b]) is head-final, and either a bimoraic monosyllable or an even or right-heavy bimoraic or trimoraic disyllable. Unlike the trochee, the iamb references weight — the quantity-sensitivity the Iambic/Trochaic Law predicts.

Equations

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

@[instance_reducible]

instance Prosody.Foot.instDecidableIsSyllabicTrochee {S : Type u_1} (f : Foot S) : Decidable f.IsSyllabicTrochee

Equations

• f.instDecidableIsSyllabicTrochee = id inferInstance

@[instance_reducible]

instance Prosody.Foot.instDecidableIsMoraicTrochee {S : Type u_1} (w : S → ℕ) (f : Foot S) : Decidable (IsMoraicTrochee w f)

Equations

• Prosody.Foot.instDecidableIsMoraicTrochee w f = id inferInstance

@[instance_reducible]

instance Prosody.Foot.instDecidableIsCanonicalIamb {S : Type u_1} (w : S → ℕ) (f : Foot S) : Decidable (IsCanonicalIamb w f)

Equations

• Prosody.Foot.instDecidableIsCanonicalIamb w f = id inferInstance

theorem Prosody.Foot.itl_gap : ∃ (f : Foot ℕ), (f.IsIambic ∧ f.IsBinary) ∧ ¬IsCanonicalIamb id f

By the Iambic/Trochaic Law ([Hay85], after Bolton 1894) a binary iamb is not characterizable weight-blind, since the head-final binary cell admits the left-heavy (H L̗) that Hayes' canonical inventory excludes, whereas a binary trochee is exactly IsSyllabicTrochee (weight-blind). The witness is (H L̗).

Re-representations (preserving the head)

def Prosody.Foot.toProsTree {S : Type u_1} (w : S → Syllable.Weight) (f : Foot S) (isHead : Bool := false) : Tree

As a prosodic tree ([Sel80]; [IM03]) a foot is a depth-1 .f node over .σ leaves, the head σ marked via Constituent.isHead. The .f node itself is marked isHead when the foot heads its ω (the isHead argument, set by the caller building the word tree).

Equations

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

def Prosody.Foot.toGrid {S : Type u_1} (f : Foot S) : List ℕ

In the metrical grid of a foot in isolation ([Hay95b]) the head σ carries 2 grid marks and every other σ 1.

Equations

• f.toGrid = List.map (fun (i : Fin f.syllables.length) => if i = f.head then 2 else 1) (List.finRange f.syllables.length)

def Prosody.Foot.headFlags {S : Type u_1} (f : Foot S) : List Bool

The σ-leaves' head flags are true at the head σ and false elsewhere ([Hay95b]).

Equations

• f.headFlags = List.map (fun (i : Fin f.syllables.length) => decide (i = f.head)) (List.finRange f.syllables.length)

def Prosody.Foot.childHeadFlags : Tree → List Bool

The σ-leaves' head flags read off a tree.

Equations

• Prosody.Foot.childHeadFlags (RoseTree.node value cs) = List.map (fun (x : RoseTree Prosody.Constituent) => match x with | RoseTree.node a children => a.isHead) cs

@[simp]

theorem Prosody.Foot.toGrid_length {S : Type u_1} (f : Foot S) : f.toGrid.length = f.syllables.length

theorem Prosody.Foot.headFlags_toProsTree {S : Type u_1} (w : S → Syllable.Weight) (f : Foot S) : childHeadFlags (toProsTree w f) = f.headFlags

The two re-representations carry the same head profile, since the prosodic tree's σ-leaf head flags are exactly headFlags f, so both recover the foot's head.

theorem Prosody.Foot.isFoot_toProsTree {S : Type u_1} (w : S → Syllable.Weight) (f : Foot S) : IsFoot (toProsTree w f)

A Foot record's prosodic-tree re-representation is always a well-formed foot tree, since toProsTree lands in the depth-1 f/σ band that IsFoot carves out. With headFlags_toProsTree (head-preservation) this is the load-bearing half of the Foot S ≃ {t // IsFoot t} embedding that bridges footing-on-Foot to OT-on-Tree.

Foot mora count

def Prosody.footMorae (ws : List Syllable.Weight) : ℕ

Mora count of a foot given as a weight-list (each weight is a mora count). The moraic measure for Tree-extracted feet (Prosody.feet, in Word.lean); for a headed Foot S, use Foot.moraCount.

Equations

• Prosody.footMorae ws = List.foldl (fun (x1 x2 : ℕ) => x1 + x2) 0 ws

Footings

[Lam22b] [Kag07]

A footing: a flat parse into feet and stray (unfooted) syllables, no designated head ([Lam22b]); the σ-type S carries quantity (Unit insensitive, Syllable.Weight not). A prosodic word ω (an IsWord tree, Prosody/Word.lean) is the headed refinement of a footing.

@[reducible, inline]

abbrev Prosody.Footing (S : Type u_1) : Type u_1

A footing is a flat sequence of feet and stray (unfooted) syllables, with no designated head ([Lam22b]).

Equations

• Prosody.Footing S = List (Prosody.Foot S ⊕ S)

def Prosody.Footing.feet {S : Type u_1} (fc : Footing S) : List (Foot S)

The feet, left to right.

Equations

• fc.feet = List.filterMap Sum.getLeft? fc

def Prosody.Footing.strays {S : Type u_1} (fc : Footing S) : List S

The stray (unfooted) syllables, left to right.

Equations

• fc.strays = List.filterMap Sum.getRight? fc

def Prosody.Footing.size {S : Type u_1} (fc : Footing S) : ℕ

The total number of syllables, footed and stray.

Equations

• fc.size = (List.map (Sum.elim Prosody.Foot.length fun (x : S) => 1) fc).sum

def Prosody.Footing.strayMarks {S : Type u_1} (fc : Footing S) : List ℕ

The Parse(σ) violation profile ([Lam22b]) is 1 at each stray σ and 0 at each footed one.

Equations

• fc.strayMarks = List.flatMap (Sum.elim (fun (x : Prosody.Foot S) => List.replicate x.length 0) fun (x : S) => [1]) fc

Foot positions and quantity

The structural readings the metrical alignment and binarity constraints count ([Kag07]): ALL-FT-LEFT is footOffsets.sum, ALL-FT-RIGHT the same on the reversed footing, FT-BIN(μ) the length of nonBimoraicFeet, and PARSE-SYL the length of strays.

def Prosody.Footing.footOffsets {S : Type u_1} (fc : Footing S) : List ℕ

The left-edge position of each foot, in syllables from the left edge of the footing.

Equations

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

def Prosody.Footing.nonBimoraicFeet {S : Type u_1} (w : S → ℕ) (fc : Footing S) : List (Foot S)

The feet that are not bimoraic under the weight reading w (for the syllabic reading, read every syllable as one mora).

Equations

• Prosody.Footing.nonBimoraicFeet w fc = List.filter (fun (f : Prosody.Foot S) => decide (Prosody.Foot.moraCount w f ≠ 2)) fc.feet

Worked examples