Metrical feet

[Hay95a] [Sel80] [Kag99]

The canonical metrical foot ([Sel80]; [NV86]; [Hay95a]; [Kag99]): a flat, headed constituent over syllable positions — a non-empty, ordered sequence of syllables with one distinguished head (the stressed daughter / head terminal). Headedness (trochaic/iambic), binarity, and the trochee/iamb/moraic inventory are all derived from the structure, not stored — the moraic/syllabic split is a counting parameter on moraCount, not a different kind of foot. Re-representations into the prosodic tree (Prosody.Tree) and the metrical grid are functions that recover the same head.

Main definitions

• isFootTree / IsFoot — structural foot well-formedness on the prosodic-tree carrier (an f-node over a non-empty list of σ-leaves; the Layeredness core).
• 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).

Main results

• Foot.itl_gap — the Iambic/Trochaic Law ([Hay85]): 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.

Carrier well-formedness

def Prosody.isFootTree : Tree → Bool

The structural Bool foot checker on the prosodic-tree carrier ([Sel80]; matches Foot.toProsTree): an f-node dominating a non-empty list of σ-leaves.

Equations

• Prosody.isFootTree (RoseTree.node a cs) = (a.isFt && !cs.isEmpty && cs.all fun (x : RoseTree Prosody.Constituent) => match x with | RoseTree.node b ds => b.isSyl && ds.isEmpty)

def Prosody.IsFoot (t : Tree) : Prop

A well-formed foot: an f-node dominating a non-empty list of σ-leaves — the inviolable Layeredness + σ-Headedness core ([Sel80]; [Hay95a]). Foot binarity (FtBin) and recursive internally-layered feet (contested — Golston 2021 vs [MPK15]) are violable and deferred; this is flat feet, the sibling of IsWord's Layeredness.

Equations

• Prosody.IsFoot t = (Prosody.isFootTree t = true)

@[implicit_reducible]

instance Prosody.instDecidableIsFoot (t : Tree) : Decidable (IsFoot t)

Equations

• Prosody.instDecidableIsFoot t = Prosody.instDecidableIsFoot._aux_1 t

The canonical foot

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

The canonical metrical foot ([Sel80]; [Hay95a]; [Kag99]): a non-empty, ordered sequence of syllable positions with one distinguished head (the stressed daughter, the head). 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.

@[implicit_reducible]

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

Equations

• Prosody.instDecidableEqFoot = Prosody.instDecidableEqFoot.decEq

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.

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

@[implicit_reducible]

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

Equations

• f.instDecidableIsTrochaic = id inferInstance

@[implicit_reducible]

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

Equations

• f.instDecidableIsIambic = id inferInstance

@[implicit_reducible]

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

Equations

• f.instDecidableIsBinary = id inferInstance

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

Syllabic trochee (σ́σ): head-initial and binary, weight-blind ([Hay95a]).

Equations

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

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

Moraic trochee (H)/(LL): head-initial and bimoraic ([Hay95a]).

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

Canonical iamb over Hayes' right-prominent inventory {(H),(LL),(LH)} ([Hay95a]): head-final, and either a bimoraic monosyllable or an even/right-heavy bi-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.

@[implicit_reducible]

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

Equations

• f.instDecidableIsSyllabicTrochee = id inferInstance

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

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

The Iambic/Trochaic Law ([Hay85], after Bolton 1894): a binary iamb is not characterizable weight-blind — 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). Witness: (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

Re-represent as a prosodic tree ([Sel80]; [IM03]): 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 ℕ

The metrical grid of a foot in isolation ([Hay95a]): the head σ carries 2 grid marks, 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: true at the head σ, false elsewhere ([Hay95a]).

Equations

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

@[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) : Prosody.Foot.childHeadFlags✝ (toProsTree w f) = f.headFlags

The two re-representations carry the same head profile: 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)

Functoriality / well-formedness bridge: a Foot record's prosodic-tree re-representation is always a well-formed foot tree — toProsTree lands in the depth-1 f/σ band that isFootTree 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: a flat sequence of feet and stray (unfooted) syllables, 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]): 1 at each stray σ, 0 at each footed.

Equations

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

Worked examples