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

def Theories.Phonology.Syllable.SyllWeight.morae : SyllWeight → Nat

Mora count derived from syllable weight class. Light = 1μ (CV), heavy = 2μ (CVV, CVC), superheavy = 3μ (CVVC, CVCC). Assumes Weight-by-Position (@cite{hayes-1989}): coda consonants are moraic.

Equations

• Theories.Phonology.Syllable.SyllWeight.light.morae = 1
• Theories.Phonology.Syllable.SyllWeight.heavy.morae = 2
• Theories.Phonology.Syllable.SyllWeight.superheavy.morae = 3

inductive Theories.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).

instance Theories.Phonology.Syllable.instDecidableEqFootType : DecidableEq FootType

Equations

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

def Theories.Phonology.Syllable.instBEqFootType.beq : FootType → FootType → Bool

Equations

• Theories.Phonology.Syllable.instBEqFootType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.Syllable.instBEqFootType : BEq FootType

Equations

• Theories.Phonology.Syllable.instBEqFootType = { beq := Theories.Phonology.Syllable.instBEqFootType.beq }

instance Theories.Phonology.Syllable.instReprFootType : Repr FootType

Equations

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

def Theories.Phonology.Syllable.instReprFootType.repr : FootType → Nat → Std.Format

Equations

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

inductive Theories.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.

instance Theories.Phonology.Syllable.instDecidableEqParseElement : DecidableEq ParseElement

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Syllable.instDecidableEqParseElement.decEq (Theories.Phonology.Syllable.ParseElement.foot a) (Theories.Phonology.Syllable.ParseElement.unfooted a_1) = isFalse ⋯
• Theories.Phonology.Syllable.instDecidableEqParseElement.decEq (Theories.Phonology.Syllable.ParseElement.unfooted a) (Theories.Phonology.Syllable.ParseElement.foot a_1) = isFalse ⋯

def Theories.Phonology.Syllable.instBEqParseElement.beq : ParseElement → ParseElement → Bool

Equations

• Theories.Phonology.Syllable.instBEqParseElement.beq (Theories.Phonology.Syllable.ParseElement.foot a) (Theories.Phonology.Syllable.ParseElement.foot b) = (a == b)
• Theories.Phonology.Syllable.instBEqParseElement.beq (Theories.Phonology.Syllable.ParseElement.unfooted a) (Theories.Phonology.Syllable.ParseElement.unfooted b) = (a == b)
• Theories.Phonology.Syllable.instBEqParseElement.beq x✝¹ x✝ = false

instance Theories.Phonology.Syllable.instBEqParseElement : BEq ParseElement

Equations

• Theories.Phonology.Syllable.instBEqParseElement = { beq := Theories.Phonology.Syllable.instBEqParseElement.beq }

instance Theories.Phonology.Syllable.instReprParseElement : Repr ParseElement

Equations

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

def Theories.Phonology.Syllable.instReprParseElement.repr : ParseElement → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Theories.Phonology.Syllable.MetricalParse : Type

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

Equations

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

def Theories.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 Theories.Phonology.Syllable.footMorae (ws : List SyllWeight) : Nat

Mora count of a single foot.

Equations

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

def Theories.Phonology.Syllable.MetricalParse.syllableCount (p : MetricalParse) : Nat

Total syllable count in a parse.

Equations

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

def Theories.Phonology.Syllable.MetricalParse.unparsedCount (p : MetricalParse) : Nat

Number of unparsed syllables in a parse.

Equations

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

def Theories.Phonology.Syllable.isDegenerate (ws : List SyllWeight) : Bool

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

Equations

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Syllable.isWellFormedFoot Theories.Phonology.Syllable.FootType.moraicTrochee ws = (Theories.Phonology.Syllable.footMorae ws == 2)
• Theories.Phonology.Syllable.isWellFormedFoot Theories.Phonology.Syllable.FootType.syllabicTrochee ws = (ws.length == 2)

def Theories.Phonology.Syllable.ftBinViolations (p : MetricalParse) : Nat

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

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

def Theories.Phonology.Syllable.parseSylViolations (p : MetricalParse) : Nat

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

Equations

• Theories.Phonology.Syllable.parseSylViolations p = p.unparsedCount

def Theories.Phonology.Syllable.allFtLeftViolations (p : MetricalParse) : Nat

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

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

def Theories.Phonology.Syllable.allFtLeftViolations.go : List ParseElement → Nat → Nat

Equations

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

def Theories.Phonology.Syllable.allFtRightViolations (p : MetricalParse) : Nat

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Syllable.allFtRightViolations.go total [] x✝ = 0

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

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

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

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

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

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

theorem Theories.Phonology.Syllable.l_not_wellformed_mt : isWellFormedFoot FootType.moraicTrochee [SyllWeight.light] = false

theorem Theories.Phonology.Syllable.light_degenerate : isDegenerate [SyllWeight.light] = true

theorem Theories.Phonology.Syllable.heavy_not_degenerate : isDegenerate [SyllWeight.heavy] = false

theorem Theories.Phonology.Syllable.ll_not_degenerate : isDegenerate [SyllWeight.light, SyllWeight.light] = false

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

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

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

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

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

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

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

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