Lamont (2022): A Restrictive, Parsimonious Theory of Footing in Directional Harmonic Serialism

This file formalizes the theory of quantity-insensitive footing of [Lam22b]: Harmonic Serialism ([PS93]) with a GEN that parses one foot per step ([Pru10], [Pru12]) and a CON of directionally evaluated constraints ([Eis00], [Lam22d]), whose violation vectors record where violations fall and are compared lexicographically. Under directional evaluation Parse(σ) both motivates iterative footing and decides where feet surface, so that the alignment constraints of [McCP93] are unnecessary, and with Trochee and Iamb both penalizing monosyllabic feet FtBin is unnecessary too ([MPK15]). The paper's tableaux are run as HSDerivations over footings: the four-syllable step that parses a leftmost trochee (23), the odd-parity step that parses a final monosyllable when Parse(σ) dominates Trochee and leaves it unfooted otherwise ((24), (25), Murinbata ([SM81]) against Pintupi ([HH69])), antepenultimate stress placed by Iamb where Hd(ω) is active (29), bidirectional footing from a FootLeft foot (33), ternary rhythm from *FootFoot (36), and the exhaustive bidirectional footing of Waorani (43), which parses its suffix string first under indexed constraints (44). A monosyllabic foot is never optimal while a disyllabic foot can be parsed (monosyllable_never_optimal), and Parse(σ) orders the placements of a foot type ((13), (14)).

Implementation notes

A footing is the library's Prosody.Footing, a flat sequence of feet and stray syllables with no head foot, since the paper does not distinguish primary from secondary stress; a syllable carries no weight, and for Waorani only its affiliation to stem or suffix. Directional constraints are OptimalityTheory.directionalBlocks, one binary constraint per syllable position, the block reversed for right-to-left evaluation; a foot-form violation is charged at the rightmost syllable of its foot, as under left-to-right evaluation, which the paper shows is the only direction that matters for these constraints in iterative footing. The prosodic-word constraints Hd(ω), NonFinality, FootLeft, FootRight, and *FootFoot are counted, their direction being irrelevant to a word. Each tableau is a stepOptimum computation with convergence checked at the last step; the factorial typology of §4 is not formalized.

References

• [Lam22b]
• [Lam22d], [Eis00], [PS93], [Pru10], [Pru12]
• [McCP93], [MPK15]
• [SM81], [HH69]

GEN (§2.1)

def Lamont2022c.parseOne {S : Type u_1} : Prosody.Footing S → List (Prosody.Footing S)

The footings that parse exactly one more foot: a stray syllable into a monosyllabic foot, or two adjacent stray syllables into a trochee or an iamb ((9)); feet are never altered.

Equations

• One or more equations did not get rendered due to their size.
• Lamont2022c.parseOne [] = []
• Lamont2022c.parseOne (Sum.inl f :: rest) = List.map (fun (x : List (Prosody.Foot S ⊕ S)) => Sum.inl f :: x) (Lamont2022c.parseOne rest)
• Lamont2022c.parseOne (Sum.inr a :: rest) = [Sum.inl (Prosody.Foot.monosyllable a) :: rest] ++ List.map (fun (x : List (Prosody.Foot S ⊕ S)) => Sum.inr a :: x) (Lamont2022c.parseOne rest)

def Lamont2022c.gen {S : Type u_1} [DecidableEq S] (fc : Prosody.Footing S) : Finset (Prosody.Footing S)

GEN: the faithful candidate and the parses of one more foot.

Equations

• Lamont2022c.gen fc = (fc :: Lamont2022c.parseOne fc).toFinset

Constraints (§2.2)

def Lamont2022c.parseLR {S : Type u_1} (n : ℕ) : List (OptimalityTheory.Constraint (Prosody.Footing S))

Parse(σ) evaluated left to right ((10)): one violation at each unfooted syllable.

Equations

• Lamont2022c.parseLR n = OptimalityTheory.directionalBlock n fun (i : Fin n) (fc : Prosody.Footing S) => fc.strayMarks.getD (↑i) 0 = 1

def Lamont2022c.parseRL {S : Type u_1} (n : ℕ) : List (OptimalityTheory.Constraint (Prosody.Footing S))

Parse(σ) evaluated right to left: the block reversed.

Equations

• Lamont2022c.parseRL n = (Lamont2022c.parseLR n).reverse

def Lamont2022c.footMarks {S : Type u_1} (P : Prosody.Foot S → Bool) (fc : Prosody.Footing S) : List ℕ

The violation vector of a foot-form constraint: a foot with the property P is charged at its rightmost syllable, the left-to-right convention.

Equations

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

def Lamont2022c.trochee {S : Type u_1} (n : ℕ) : List (OptimalityTheory.Constraint (Prosody.Footing S))

Trochee ((15)): one violation per foot whose rightmost syllable is its head, a monosyllabic foot included.

Equations

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

def Lamont2022c.iamb {S : Type u_1} (n : ℕ) : List (OptimalityTheory.Constraint (Prosody.Footing S))

Iamb ((18)): one violation per foot whose leftmost syllable is its head, a monosyllabic foot included.

Equations

• Lamont2022c.iamb n = OptimalityTheory.directionalBlock n fun (i : Fin n) (fc : Prosody.Footing S) => (Lamont2022c.footMarks (fun (f : Prosody.Foot S) => decide f.IsTrochaic) fc).getD (↑i) 0 = 1

def Lamont2022c.hdWord {S : Type u_1} : OptimalityTheory.Constraint (Prosody.Footing S)

Hd(ω) ((26)): the word dominates no foot.

Equations

• Lamont2022c.hdWord = OptimalityTheory.Constraint.binary fun (x : Prosody.Footing S) => x.feet = []

def Lamont2022c.nonFinality {S : Type u_1} : OptimalityTheory.Constraint (Prosody.Footing S)

NonFinality ((28)): the rightmost syllable is footed.

Equations

• Lamont2022c.nonFinality = OptimalityTheory.Constraint.binary fun (x : Prosody.Footing S) => x.strayMarks.getLast? = some 0

def Lamont2022c.footLeft {S : Type u_1} : OptimalityTheory.Constraint (Prosody.Footing S)

FootLeft ((30)): the leftmost syllable is not leftmost in a foot.

Equations

• Lamont2022c.footLeft = OptimalityTheory.Constraint.binary fun (x : Prosody.Footing S) => x.strayMarks.head? = some 1

def Lamont2022c.footRight {S : Type u_1} : OptimalityTheory.Constraint (Prosody.Footing S)

FootRight ((31)): the rightmost syllable is not rightmost in a foot.

Equations

• Lamont2022c.footRight = OptimalityTheory.Constraint.binary fun (x : Prosody.Footing S) => x.strayMarks.getLast? = some 1

def Lamont2022c.starFootFoot {S : Type u_1} : OptimalityTheory.Constraint (Prosody.Footing S)

*FootFoot ((34)): one violation per pair of adjacent feet.

Equations

• Lamont2022c.starFootFoot fc = (List.filter (fun (p : (Prosody.Foot S ⊕ S) × (Prosody.Foot S ⊕ S)) => p.1.isLeft && p.2.isLeft) (List.zip fc (List.tail fc))).length

def Lamont2022c.vec {S : Type u_1} (block : List (OptimalityTheory.Constraint (Prosody.Footing S))) (fc : Prosody.Footing S) : List ℕ

The violation vector of a block of constraints on a footing.

Equations

• Lamont2022c.vec block fc = List.map (fun (x : OptimalityTheory.Constraint (Prosody.Footing S)) => x fc) block

Iterative footing (§2.2)

Quantity-insensitive words are strings of syllables of type Unit.

@[reducible, inline]

abbrev Lamont2022c.stray : Prosody.Foot Unit ⊕ Unit

An unfooted syllable.

Equations

• Lamont2022c.stray = Sum.inr ()

@[reducible, inline]

abbrev Lamont2022c.troch : Prosody.Foot Unit ⊕ Unit

A trochee (σ́σ).

Equations

• Lamont2022c.troch = Sum.inl (Prosody.Foot.trochee () ())

@[reducible, inline]

abbrev Lamont2022c.mono : Prosody.Foot Unit ⊕ Unit

A monosyllabic foot (σ́).

Equations

• Lamont2022c.mono = Sum.inl (Prosody.Foot.monosyllable ())

def Lamont2022c.strays (n : ℕ) : Prosody.Footing Unit

A string of n unfooted syllables.

Equations

• Lamont2022c.strays n = List.replicate n Lamont2022c.stray

theorem Lamont2022c.parseLR_orders_trochees : vec (parseLR 4) [troch, stray, stray] < vec (parseLR 4) [stray, troch, stray] ∧ vec (parseLR 4) [stray, troch, stray] < vec (parseLR 4) [stray, stray, troch]

Parse(σ)⇒ orders the placements of a trochee, the leftmost best ((13a)).

theorem Lamont2022c.parseRL_orders_trochees : vec (parseRL 4) [stray, stray, troch] < vec (parseRL 4) [stray, troch, stray] ∧ vec (parseRL 4) [stray, troch, stray] < vec (parseRL 4) [troch, stray, stray]

Parse(σ)⇐ orders them the other way, the rightmost best ((14a)).

def Lamont2022c.murinbata (n : ℕ) : OptimalityTheory.HSDerivation (Prosody.Footing Unit)

Parse(σ)⇒ ≫ Trochee ≫ Iamb: Murinbata's exhaustive left-to-right trochees ((21), (23), (24)).

Equations

• Lamont2022c.murinbata n = { gen := Lamont2022c.gen, ranking := Lamont2022c.parseLR n ++ Lamont2022c.trochee n ++ Lamont2022c.iamb n }

def Lamont2022c.pintupi (n : ℕ) : OptimalityTheory.HSDerivation (Prosody.Footing Unit)

Trochee ≫ Parse(σ)⇒ ≫ Iamb: Pintupi's inexhaustive left-to-right trochees ((22), (25)).

Equations

• Lamont2022c.pintupi n = { gen := Lamont2022c.gen, ranking := Lamont2022c.trochee n ++ Lamont2022c.parseLR n ++ Lamont2022c.iamb n }

theorem Lamont2022c.step_23i : (murinbata 4).stepOptimum (strays 4) = {[troch, stray, stray]}

(23i): the first step parses a trochee at the left edge.

theorem Lamont2022c.step_23m : (murinbata 4).stepOptimum [troch, stray, stray] = {[troch, troch]}

(23m): the second step foots the remaining two syllables.

theorem Lamont2022c.converged_23 : (murinbata 4).Converged [troch, troch]

The even-parity derivation converges without a monosyllabic foot.

def Lamont2022c.monoParses : List (Prosody.Footing Unit)

The monosyllabic-foot parses of /σσσσ/ ((23b–e)).

Equations

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

def Lamont2022c.rankings (n : ℕ) : List (List (OptimalityTheory.Constraint (Prosody.Footing Unit)))

The six rankings of Parse(σ), Trochee, and Iamb, evaluated left to right.

Equations

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

theorem Lamont2022c.monosyllable_never_optimal (r : List (OptimalityTheory.Constraint (Prosody.Footing Unit))) : r ∈ rankings 4 → ∀ m ∈ monoParses, m ∉ { gen := gen, ranking := r }.stepOptimum (strays 4)

A monosyllabic foot is never optimal while a disyllabic foot can be parsed ((23)): under every ranking of the three constraints, no monosyllabic parse of /σσσσ/ is in the step optimum, so FtBin is unnecessary.

theorem Lamont2022c.step_24 : (murinbata 5).stepOptimum [troch, troch, stray] = {[troch, troch, mono]}

(24): with Parse(σ) dominant, the final syllable of an odd-parity word is footed.

theorem Lamont2022c.converged_25 : (pintupi 5).Converged [troch, troch, stray]

(25): with Trochee dominant, it stays unfooted and the derivation has converged.

Non-iterative footing (§2.2)

Where Hd(ω) alone motivates a foot, Iamb⇒ places a trochee as far right as NonFinality allows: antepenultimate stress ((27), (29)).

def Lamont2022c.macedonian (n : ℕ) : OptimalityTheory.HSDerivation (Prosody.Footing Unit)

Hd(ω) ≫ Trochee ≫ NonFinality ≫ Iamb⇒ ≫ Parse(σ): Macedonian antepenultimate stress.

Equations

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

theorem Lamont2022c.step_29f : (macedonian 4).stepOptimum (strays 4) = {[stray, troch, stray]}

(29f): the trochee surfaces one syllable from the right edge.

theorem Lamont2022c.converged_29 : (macedonian 4).Converged [stray, troch, stray]

No further foot is parsed, Trochee and Iamb dominating Parse(σ).

Bidirectional and ternary footing (§2.2)

A foot is first parsed at one edge, satisfying FootLeft, then feet are parsed from the other edge by Parse(σ)⇐, with word-internal lapse in odd-parity words ((32), (33)); *FootFoot above Parse(σ) leaves a syllable between feet ((35), (36)).

def Lamont2022c.garawa (n : ℕ) : OptimalityTheory.HSDerivation (Prosody.Footing Unit)

FootLeft ≫ Trochee ≫ Parse(σ)⇐ ≫ Iamb: Garawa's bidirectional trochees.

Equations

• Lamont2022c.garawa n = { gen := Lamont2022c.gen, ranking := Lamont2022c.footLeft :: Lamont2022c.trochee n ++ Lamont2022c.parseRL n ++ Lamont2022c.iamb n }

theorem Lamont2022c.step_33b : (garawa 7).stepOptimum (strays 7) = {troch :: strays 5}

theorem Lamont2022c.step_33g : (garawa 7).stepOptimum (troch :: strays 5) = {troch :: strays 3 ++ [troch]}

theorem Lamont2022c.step_33i : (garawa 7).stepOptimum (troch :: strays 3 ++ [troch]) = {[troch, stray, troch, troch]}

theorem Lamont2022c.converged_33 : (garawa 7).Converged [troch, stray, troch, troch]

(33j): the third syllable stays unfooted, Trochee dominating Parse(σ).

def Lamont2022c.cayuvava (n : ℕ) : OptimalityTheory.HSDerivation (Prosody.Footing Unit)

NonFinality ≫ *FootFoot ≫ Parse(σ)⇐ ≫ Trochee ≫ Iamb: Cayuvava's dactyls.

Equations

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

theorem Lamont2022c.step_36h : (cayuvava 9).stepOptimum (strays 9) = {strays 6 ++ [troch, stray]}

theorem Lamont2022c.step_36n : (cayuvava 9).stepOptimum (strays 6 ++ [troch, stray]) = {strays 3 ++ [troch, stray, troch, stray]}

theorem Lamont2022c.step_36q : (cayuvava 9).stepOptimum (strays 3 ++ [troch, stray, troch, stray]) = {[troch, stray, troch, stray, troch, stray]}

theorem Lamont2022c.converged_36 : (cayuvava 9).Converged [troch, stray, troch, stray, troch, stray]

The stray syllables cannot be footed without violating NonFinality or *FootFoot.

Waorani (§3)

The head foot is parsed at the right edge under FootRight, then the suffix string is footed under the indexed Parse(σ)ₛᵤffix, then the stem from the left, with a monosyllabic foot surfacing only in the stem, since the indexed Trocheeₛᵤffix dominates Parse(σ)ₛᵤffix while Parse(σ) dominates Trochee ((37)–(44)).

inductive Lamont2022c.Morph : Type

A syllable's affiliation.

• stem : Morph
• suffix : Morph

@[instance_reducible]

instance Lamont2022c.instDecidableEqMorph : DecidableEq Morph

Equations

• Lamont2022c.instDecidableEqMorph x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lamont2022c.instReprMorph.repr : Morph → ℕ → Std.Format

Equations

• Lamont2022c.instReprMorph.repr Lamont2022c.Morph.stem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lamont2022c.Morph.stem")).group prec✝
• Lamont2022c.instReprMorph.repr Lamont2022c.Morph.suffix prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lamont2022c.Morph.suffix")).group prec✝

@[instance_reducible]

instance Lamont2022c.instReprMorph : Repr Morph

Equations

• Lamont2022c.instReprMorph = { reprPrec := Lamont2022c.instReprMorph.repr }

def Lamont2022c.Morph.isSuffix : Morph → Bool

The suffix syllables.

Equations

• Lamont2022c.Morph.suffix.isSuffix = true
• Lamont2022c.Morph.stem.isSuffix = false

def Lamont2022c.parseSuffixLR (n : ℕ) : List (OptimalityTheory.Constraint (Prosody.Footing Morph))

Parse(σ) indexed to the suffix string, evaluated left to right.

Equations

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

def Lamont2022c.trocheeSuffix (n : ℕ) : List (OptimalityTheory.Constraint (Prosody.Footing Morph))

Trochee indexed to the suffix string: charged to a foot dominating a suffix syllable.

Equations

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

def Lamont2022c.waorani (n : ℕ) : OptimalityTheory.HSDerivation (Prosody.Footing Morph)

FootRight ≫ Parse(σ)⇒ ≫ Trochee ≫ Iamb ((43)), with the indexed Trocheeₛᵤffix ≫ Parse(σ)ₛᵤffix between FootRight and Parse(σ) ((44)).

Equations

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

@[reducible, inline]

abbrev Lamont2022c.st : Prosody.Foot Morph ⊕ Morph

An unfooted stem syllable.

Equations

• Lamont2022c.st = Sum.inr Lamont2022c.Morph.stem

@[reducible, inline]

abbrev Lamont2022c.sf : Prosody.Foot Morph ⊕ Morph

An unfooted suffix syllable.

Equations

• Lamont2022c.sf = Sum.inr Lamont2022c.Morph.suffix

@[reducible, inline]

abbrev Lamont2022c.trochSt : Prosody.Foot Morph ⊕ Morph

A trochee over two stem syllables.

Equations

• Lamont2022c.trochSt = Sum.inl (Prosody.Foot.trochee Lamont2022c.Morph.stem Lamont2022c.Morph.stem)

@[reducible, inline]

abbrev Lamont2022c.trochSf : Prosody.Foot Morph ⊕ Morph

A trochee over two suffix syllables.

Equations

• Lamont2022c.trochSf = Sum.inl (Prosody.Foot.trochee Lamont2022c.Morph.suffix Lamont2022c.Morph.suffix)

@[reducible, inline]

abbrev Lamont2022c.monoSt : Prosody.Foot Morph ⊕ Morph

A monosyllabic foot over a stem syllable.

Equations

• Lamont2022c.monoSt = Sum.inl (Prosody.Foot.monosyllable Lamont2022c.Morph.stem)

theorem Lamont2022c.steps_43 : (waorani 5).stepOptimum [st, st, st, st, st] = {[st, st, st, trochSt]} ∧ (waorani 5).stepOptimum [st, st, st, trochSt] = {[trochSt, st, trochSt]} ∧ (waorani 5).stepOptimum [trochSt, st, trochSt] = {[trochSt, monoSt, trochSt]} ∧ (waorani 5).Converged [trochSt, monoSt, trochSt]

(43): a pentasyllabic stem is footed from the right edge, then from the left, and a monosyllabic foot surfaces word-medially.

theorem Lamont2022c.steps_44 : (waorani 10).stepOptimum [st, st, st, st, st, sf, sf, sf, sf, sf] = {[st, st, st, st, st, sf, sf, sf, trochSf]} ∧ (waorani 10).stepOptimum [st, st, st, st, st, sf, sf, sf, trochSf] = {[st, st, st, st, st, trochSf, sf, trochSf]} ∧ (waorani 10).stepOptimum [st, st, st, st, st, trochSf, sf, trochSf] = {[trochSt, st, st, st, trochSf, sf, trochSf]} ∧ (waorani 10).stepOptimum [trochSt, st, st, st, trochSf, sf, trochSf] = {[trochSt, trochSt, st, trochSf, sf, trochSf]} ∧ (waorani 10).stepOptimum [trochSt, trochSt, st, trochSf, sf, trochSf] = {[trochSt, trochSt, monoSt, trochSf, sf, trochSf]} ∧ (waorani 10).Converged [trochSt, trochSt, monoSt, trochSf, sf, trochSf]

(44): with a pentasyllabic suffix string, the head foot is parsed at the right edge, the suffix string is footed from its left edge before the stem, the stem is exhaustively footed, and the remaining suffix syllable stays unfooted.