Metrical Foot Structure

@cite{hayes-1995} @cite{kager-2007}

Foot types, metrical parsing, and OT constraints on metrical structure.

A metrical foot is a prosodic constituent grouping syllables into a rhythmic unit. @cite{hayes-1995} identifies three canonical foot types:

Type	Well-formed shapes	Stress system
Moraic trochee	(H), (LL)	Weight-sensitive
Syllabic trochee	(σσ)	Weight-insensitive
Iamb	(LH), (LL), (H)	Right-prominent

The foot's head (prominent syllable) determines stress: initial in trochees, final in iambs.

Definitions

• SyllWeight.morae: mora count from weight class
• FootType: the three canonical foot types
• ParseElement: element in a metrical parse (footed or unfooted)
• MetricalParse: a complete metrical parse of a prosodic domain
• OT constraints: ftBinViolations, parseSylViolations, allFtLeftViolations

inductive Phonology.Syllable.FootType : Type

The three canonical foot types (@cite{hayes-1995}, Ch. 3).

• moraicTrochee : FootType

  Moraic trochee: bimoraic with initial prominence. Well-formed shapes: (H) = 2μ, (LL) = 2μ. Used in weight-sensitive stress (Turkish, Latin, Telugu).

• syllabicTrochee : FootType

  Syllabic trochee: bisyllabic with initial prominence. Well-formed shape: (σσ) regardless of weight. Used in weight-insensitive stress (Czech, Pintupi).

• iamb : FootType

  Iamb: prominence on the heavier/final syllable. Well-formed shapes: (LH), (LL), (H). Used in right-prominent stress (Creek, Yupik).

@[implicit_reducible]

instance Phonology.Syllable.instDecidableEqFootType : DecidableEq FootType

Equations

• Phonology.Syllable.instDecidableEqFootType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Syllable.instReprFootType.repr : FootType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Syllable.instReprFootType : Repr FootType

Equations

• Phonology.Syllable.instReprFootType = { reprPrec := Phonology.Syllable.instReprFootType.repr }

inductive Phonology.Syllable.ParseElement : Type

An element in a metrical parse: either a foot grouping syllables or an unparsed (stray) syllable. The list preserves left-to-right linear order within the prosodic domain.

• foot : List SyllWeight → ParseElement

  A foot containing one or more syllables (represented by weight).

• unfooted : SyllWeight → ParseElement

  An unparsed syllable not dominated by any foot.

@[implicit_reducible]

instance Phonology.Syllable.instDecidableEqParseElement : DecidableEq ParseElement

Equations

• Phonology.Syllable.instDecidableEqParseElement = Phonology.Syllable.instDecidableEqParseElement.decEq

def Phonology.Syllable.instDecidableEqParseElement.decEq (x✝ x✝¹ : ParseElement) : Decidable (x✝ = x✝¹)

Equations

• Phonology.Syllable.instDecidableEqParseElement.decEq (Phonology.Syllable.ParseElement.foot a) (Phonology.Syllable.ParseElement.foot b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Phonology.Syllable.instDecidableEqParseElement.decEq (Phonology.Syllable.ParseElement.foot a) (Phonology.Syllable.ParseElement.unfooted a_1) = isFalse ⋯
• Phonology.Syllable.instDecidableEqParseElement.decEq (Phonology.Syllable.ParseElement.unfooted a) (Phonology.Syllable.ParseElement.foot a_1) = isFalse ⋯
• Phonology.Syllable.instDecidableEqParseElement.decEq (Phonology.Syllable.ParseElement.unfooted a) (Phonology.Syllable.ParseElement.unfooted b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Phonology.Syllable.instReprParseElement.repr : ParseElement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Syllable.instReprParseElement : Repr ParseElement

Equations

• Phonology.Syllable.instReprParseElement = { reprPrec := Phonology.Syllable.instReprParseElement.repr }

@[reducible, inline]

abbrev Phonology.Syllable.MetricalParse : Type

A metrical parse: a prosodic domain represented as a linear sequence of footed and unfooted syllables.

Equations

• Phonology.Syllable.MetricalParse = List Phonology.Syllable.ParseElement

def Phonology.Syllable.MetricalParse.feet (p : MetricalParse) : List (List SyllWeight)

Extract all feet from a parse.

Equations

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

def Phonology.Syllable.footMorae (ws : List SyllWeight) : ℕ

Mora count of a single foot.

Equations

• Phonology.Syllable.footMorae ws = List.foldl (fun (x1 : ℕ) (x2 : Phonology.Syllable.SyllWeight) => x1 + x2.morae) 0 ws

def Phonology.Syllable.MetricalParse.syllableCount (p : MetricalParse) : ℕ

Total syllable count in a parse.

Equations

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

def Phonology.Syllable.MetricalParse.unparsedCount (p : MetricalParse) : ℕ

Number of unparsed syllables in a parse.

Equations

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

def Phonology.Syllable.isDegenerate (ws : List SyllWeight) : Prop

Is a foot degenerate (subminimal)? A monomoraic foot (L) is degenerate — it fails to meet the bimoraic minimum.

Equations

• Phonology.Syllable.isDegenerate ws = (Phonology.Syllable.footMorae ws < 2)

@[implicit_reducible]

instance Phonology.Syllable.instDecidableIsDegenerate (ws : List SyllWeight) : Decidable (isDegenerate ws)

Equations

• Phonology.Syllable.instDecidableIsDegenerate ws = id inferInstance

def Phonology.Syllable.isWellFormedFoot (ft : FootType) (ws : List SyllWeight) : Prop

Is a foot well-formed for the given foot type?

Equations

• Phonology.Syllable.isWellFormedFoot Phonology.Syllable.FootType.moraicTrochee ws = (Phonology.Syllable.footMorae ws = 2)
• Phonology.Syllable.isWellFormedFoot Phonology.Syllable.FootType.syllabicTrochee ws = (ws.length = 2)
• Phonology.Syllable.isWellFormedFoot Phonology.Syllable.FootType.iamb ws = (Phonology.Syllable.footMorae ws ≥ 1 ∧ Phonology.Syllable.footMorae ws ≤ 3 ∧ ws.length ≤ 2)

@[implicit_reducible]

instance Phonology.Syllable.instDecidableIsWellFormedFoot (ft : FootType) (ws : List SyllWeight) : Decidable (isWellFormedFoot ft ws)

Equations

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

def Phonology.Syllable.ftBinViolations (p : MetricalParse) : ℕ

FT-BIN(μ): assign one violation for each foot that does not consist of exactly two morae (@cite{kager-2007}).

Well-formed moraic trochees: (H) = 2μ, (LL) = 2μ. Violations: degenerate (L) = 1μ, superheavy (SH) = 3μ.

Equations

• Phonology.Syllable.ftBinViolations p = (List.filter (fun (ws : List Phonology.Syllable.SyllWeight) => Phonology.Syllable.footMorae ws != 2) p.feet).length

def Phonology.Syllable.parseSylViolations (p : MetricalParse) : ℕ

PARSE-SYL: assign one violation for each syllable not parsed into a foot (@cite{kager-2007}). Drives exhaustive parsing.

Equations

• Phonology.Syllable.parseSylViolations p = p.unparsedCount

def Phonology.Syllable.allFtLeftViolations (p : MetricalParse) : ℕ

ALL-FT-LEFT: for each foot, count the number of syllables intervening between the left edge of the prosodic domain and the left edge of the foot (@cite{kager-2007}). Sum over all feet.

A foot at syllable position k (0-indexed) incurs k violations. Drives left-to-right iterative footing.

Equations

• Phonology.Syllable.allFtLeftViolations p = Phonology.Syllable.allFtLeftViolations.go p 0

def Phonology.Syllable.allFtLeftViolations.go : List ParseElement → ℕ → ℕ

Equations

• Phonology.Syllable.allFtLeftViolations.go [] a✝ = 0
• Phonology.Syllable.allFtLeftViolations.go (Phonology.Syllable.ParseElement.foot ws :: rest) a✝ = a✝ + Phonology.Syllable.allFtLeftViolations.go rest (a✝ + ws.length)
• Phonology.Syllable.allFtLeftViolations.go (Phonology.Syllable.ParseElement.unfooted a :: rest) a✝ = Phonology.Syllable.allFtLeftViolations.go rest (a✝ + 1)

def Phonology.Syllable.allFtRightViolations (p : MetricalParse) : ℕ

ALL-FT-RIGHT: for each foot, count the number of syllables intervening between the right edge of the foot and the right edge of the prosodic domain. Sum over all feet.

Drives right-to-left iterative footing.

Equations

• Phonology.Syllable.allFtRightViolations p = Phonology.Syllable.allFtRightViolations.go p.syllableCount p 0

def Phonology.Syllable.allFtRightViolations.go (total : ℕ) : List ParseElement → ℕ → ℕ

Equations

• One or more equations did not get rendered due to their size.
• Phonology.Syllable.allFtRightViolations.go total [] a✝ = 0
• Phonology.Syllable.allFtRightViolations.go total (Phonology.Syllable.ParseElement.unfooted a :: rest) a✝ = Phonology.Syllable.allFtRightViolations.go total rest (a✝ + 1)

theorem Phonology.Syllable.heavy_foot_bimoraic : footMorae [SyllWeight.heavy] = 2

theorem Phonology.Syllable.ll_foot_bimoraic : footMorae [SyllWeight.light, SyllWeight.light] = 2

theorem Phonology.Syllable.light_foot_monomoraic : footMorae [SyllWeight.light] = 1

theorem Phonology.Syllable.superheavy_foot_trimoraic : footMorae [SyllWeight.superheavy] = 3

theorem Phonology.Syllable.heavy_wellformed_mt : isWellFormedFoot FootType.moraicTrochee [SyllWeight.heavy]

theorem Phonology.Syllable.ll_wellformed_mt : isWellFormedFoot FootType.moraicTrochee [SyllWeight.light, SyllWeight.light]

theorem Phonology.Syllable.l_not_wellformed_mt : ¬isWellFormedFoot FootType.moraicTrochee [SyllWeight.light]

theorem Phonology.Syllable.light_degenerate : isDegenerate [SyllWeight.light]

theorem Phonology.Syllable.heavy_not_degenerate : ¬isDegenerate [SyllWeight.heavy]

theorem Phonology.Syllable.ll_not_degenerate : ¬isDegenerate [SyllWeight.light, SyllWeight.light]

theorem Phonology.Syllable.llU_ftbin : ftBinViolations Phonology.Syllable.parse_llU✝ = 0

theorem Phonology.Syllable.llU_parsesyl : parseSylViolations Phonology.Syllable.parse_llU✝ = 1

theorem Phonology.Syllable.llU_allftleft : allFtLeftViolations Phonology.Syllable.parse_llU✝ = 0

theorem Phonology.Syllable.llH_ftbin : ftBinViolations Phonology.Syllable.parse_llH✝ = 0

theorem Phonology.Syllable.llH_parsesyl : parseSylViolations Phonology.Syllable.parse_llH✝ = 0

theorem Phonology.Syllable.llH_allftleft : allFtLeftViolations Phonology.Syllable.parse_llH✝ = 2

theorem Phonology.Syllable.llU_heavy_parsesyl : parseSylViolations Phonology.Syllable.parse_llU_heavy✝ = 1

theorem Phonology.Syllable.lllH_ftbin : ftBinViolations Phonology.Syllable.parse_lllH✝ = 2