Lamont (2022): footing in directional Harmonic Serialism

[Lam22b]

[Lam22b] develops a theory of quantity-insensitive footing in Harmonic Serialism (HS; [PS93]) where CON contains only directionally evaluated constraints ([Lam22d]; Eisner 2000): a constraint maps a candidate to a per-position violation vector, and candidates are ordered lexicographically by the location of violations rather than their total count. The central result is that Parse(σ) — penalising unfooted syllables — under directional evaluation both motivates iterative footing and decides where feet surface, obviating alignment constraints ([McCP93]); having Trochee/Iamb penalise monosyllabic feet additionally obviates FtBin ([MPK15]).

This file formalises the central QI result. GEN parses one foot per step ([Pru10]; [Pru12]): a single unfooted σ into a monosyllabic foot, or two adjacent unfooted σ into a disyllabic foot. We reuse the canonical Prosody.Foot (S = Unit, since QI footing strips weight) assembled flatly — a footing is a sequence of feet and stray syllables with no designated head foot, because Lamont does not distinguish primary from secondary stress (so the headed Prosody.Word ω, which is a footing plus a head foot, is deliberately not the candidate type here). Parse(σ) is a Constraints.directionalBlock over σ-positions; Trochee/Iamb read the foot head off Foot.head.

Main results

• murinbata_exhaustive / pintupi_inexhaustive — the headline contrast: the same 5σ step parses exhaustively under Parse(σ) ≫ Trochee ([SM81]) but stays faithful (final σ unfooted) under Trochee ≫ Parse(σ) ([HH69]).
• ftbin_obviated — a monosyllabic-foot candidate is harmonically bounded with no FtBin in CON ([MPK15]).

Deferred (prose)

The paper's bidirectional Waorani case study (§3 — a head foot at the right edge with secondary feet built left-to-right) is its showcase and the natural next extension; Macedonian (Hd(ω)/NonFinality), Garawa, and Cayuvava ternarity (*FootFoot) each need further constraints; the software-computed factorial typology (§4) is a meta-claim, not a per-string prediction. All are noted here, not formalised.

Footings

A footing here is the canonical Prosody.Footing Unit (quantity-insensitive, so feet are Foot Unit): a flat sequence of feet and unfooted stray σ, no designated head foot ([Lam22b], abstracting from primary stress). Parse(σ) reads Footing.strayMarks; Trochee/Iamb read each foot's head (Foot.head).

def Lamont2022c.mono : Prosody.Foot Unit

A monosyllabic foot (σ́).

Equations

• Lamont2022c.mono = { syllables := [()], head := 0 }

def Lamont2022c.troch : Prosody.Foot Unit

A (left-headed) trochee (σ́σ).

Equations

• Lamont2022c.troch = { syllables := [(), ()], head := 0 }

def Lamont2022c.iamb : Prosody.Foot Unit

A (right-headed) iamb (σσ́).

Equations

• Lamont2022c.iamb = { syllables := [(), ()], head := 1 }

The directional constraints

Parse(σ) ([Lam22b] (10)) is a Constraints.directionalBlock: a per-position block of binary constraints, position i ↦ ⟦σ i is unfooted⟧. Trochee (15) and Iamb (18) penalise feet by head position — Trochee a foot whose head is rightmost (= Foot.IsIambic, true of iambs and monosyllables), Iamb a foot whose head is leftmost (= Foot.IsTrochaic, true of trochees and monosyllables); a monosyllabic foot violates both, doing FtBin's work.

def Lamont2022c.parse (n : ℕ) : List (Constraints.Constraint (Prosody.Footing Unit))

Parse(σ) as a directional block over n σ-positions.

Equations

• Lamont2022c.parse n = Constraints.directionalBlock n fun (i : Fin n) (fc : Prosody.Footing Unit) => fc.strayMarks.getD (↑i) 0 = 1

def Lamont2022c.trochee (fc : Prosody.Footing Unit) : ℕ

Trochee: one violation per foot whose head is rightmost (= Foot.IsIambic).

Equations

• Lamont2022c.trochee fc = (List.filter (fun (f : Prosody.Foot Unit) => decide f.IsIambic) fc.feet).length

def Lamont2022c.iambC (fc : Prosody.Footing Unit) : ℕ

Iamb: one violation per foot whose head is leftmost (= Foot.IsTrochaic).

Equations

• Lamont2022c.iambC fc = (List.filter (fun (f : Prosody.Foot Unit) => decide f.IsTrochaic) fc.feet).length

def Lamont2022c.profile (ranking : List (Constraints.Constraint (Prosody.Footing Unit))) (fc : Prosody.Footing Unit) : List ℕ

The violation vector of a footing under a ranking (a list of constraints), as the concatenated per-constraint violations — ordered lexicographically (LexLE).

Equations

• Lamont2022c.profile ranking fc = List.map (fun (c : Constraints.Constraint (Prosody.Footing Unit)) => c fc) ranking

def Lamont2022c.murinbata (n : ℕ) : List (Constraints.Constraint (Prosody.Footing Unit))

Murinbata ranking Parse(σ) ≫ Trochee ≫ Iamb ([SM81]).

Equations

• Lamont2022c.murinbata n = Lamont2022c.parse n ++ [fun (fc : Prosody.Footing Unit) => Lamont2022c.trochee fc, fun (fc : Prosody.Footing Unit) => Lamont2022c.iambC fc]

def Lamont2022c.pintupi (n : ℕ) : List (Constraints.Constraint (Prosody.Footing Unit))

Pintupi ranking Trochee ≫ Parse(σ) ≫ Iamb ([HH69]).

Equations

• Lamont2022c.pintupi n = (fun (fc : Prosody.Footing Unit) => Lamont2022c.trochee fc) :: Lamont2022c.parse n ++ [fun (fc : Prosody.Footing Unit) => Lamont2022c.iambC fc]

The headline: exhaustive vs inexhaustive (the decisive step)

The same 5σ string at the step from (σ́σ)(σ́σ)σ: GEN can parse the final stray σ into a monosyllabic foot (exhaustive) or leave it (faithful, converged).

def Lamont2022c.faithful : Prosody.Footing Unit

(σ́σ)(σ́σ)σ — two trochees and a final unfooted σ.

Equations

• Lamont2022c.faithful = [Sum.inl Lamont2022c.troch, Sum.inl Lamont2022c.troch, Sum.inr ()]

def Lamont2022c.exhaustive : Prosody.Footing Unit

(σ́σ)(σ́σ)(σ́) — the final σ parsed into a monosyllabic foot.

Equations

• Lamont2022c.exhaustive = [Sum.inl Lamont2022c.troch, Sum.inl Lamont2022c.troch, Sum.inl Lamont2022c.mono]

theorem Lamont2022c.murinbata_exhaustive : Core.Optimization.Evaluation.LexLE (profile (murinbata 5) exhaustive) (profile (murinbata 5) faithful) ∧ ¬Core.Optimization.Evaluation.LexLE (profile (murinbata 5) faithful) (profile (murinbata 5) exhaustive)

Murinbata ([SM81]): under Parse(σ) ≫ Trochee, the exhaustive parse wins — the final σ is footed into a monosyllable (final monosyllabic feet, exhaustive parsing).

theorem Lamont2022c.pintupi_inexhaustive : Core.Optimization.Evaluation.LexLE (profile (pintupi 5) faithful) (profile (pintupi 5) exhaustive) ∧ ¬Core.Optimization.Evaluation.LexLE (profile (pintupi 5) exhaustive) (profile (pintupi 5) faithful)

Pintupi ([HH69]): under Trochee ≫ Parse(σ), the faithful parse wins — parsing a monosyllable would violate the dominant Trochee, so the final σ stays unfooted (inexhaustive parsing). The derivation has converged.

Parsimony: FtBin is obviated

In even-parity /σσσσ/, the monosyllabic-foot candidate (σ́)σσσ is harmonically bounded by the disyllabic (σ́σ)σσ under Parse(σ) ≫ Trochee ≫ Iamb — without any FtBin in CON. Trochee and Iamb both penalising monosyllables do FtBin's work ([MPK15]).

def Lamont2022c.disyll4 : Prosody.Footing Unit

(σ́σ)σσ — one leftmost trochee in /σσσσ/.

Equations

• Lamont2022c.disyll4 = [Sum.inl Lamont2022c.troch, Sum.inr (), Sum.inr ()]

def Lamont2022c.monosyll4 : Prosody.Footing Unit

(σ́)σσσ — one leftmost monosyllable in /σσσσ/.

Equations

• Lamont2022c.monosyll4 = [Sum.inl Lamont2022c.mono, Sum.inr (), Sum.inr (), Sum.inr ()]

theorem Lamont2022c.ftbin_obviated : Core.Optimization.Evaluation.LexLE (profile (murinbata 4) disyll4) (profile (murinbata 4) monosyll4) ∧ ¬Core.Optimization.Evaluation.LexLE (profile (murinbata 4) monosyll4) (profile (murinbata 4) disyll4)

FtBin obviation: the disyllabic-foot candidate strictly beats the monosyllabic-foot candidate with no FtBin in CON — the monosyllable both fails Parse(σ) more and violates Trochee.

The footing functor: head (= stress) survives into grid and tree

Lamont's Trochee/Iamb read each foot's head off Foot.head. Re-representing a foot into the prosodic Tree (Foot.toProsTree) and the head-flag row (Foot.headFlags) recovers exactly that head — Foot.headFlags_toProsTree proves the tree's σ-leaves carry the same head profile — and the tree always lands in the well-formed f/σ band (Foot.isFoot_toProsTree). So the head, the stress these constraints penalise, survives both re-representations. QI footing strips weight, so the tree reads any constant σ-weight.

def Lamont2022c.qiWeight : Unit → Prosody.Syllable.Weight

QI footing is weight-blind: a Foot Unit's σ read one (light) mora.

Equations

• Lamont2022c.qiWeight x✝ = Prosody.Syllable.Weight.light

theorem Lamont2022c.qiFeet_areFootTrees : Prosody.IsFoot (Prosody.Foot.toProsTree qiWeight mono) ∧ Prosody.IsFoot (Prosody.Foot.toProsTree qiWeight troch) ∧ Prosody.IsFoot (Prosody.Foot.toProsTree qiWeight iamb)

Well-formedness through the functor: every QI foot Lamont assembles re-represents as a well-formed prosodic-tree foot (Foot.isFoot_toProsTree) — the flat Footing candidates are built from feet that are legal f-over-σ subtrees of the OT Tree carrier.

theorem Lamont2022c.head_survives : troch.headFlags = [true, false] ∧ iamb.headFlags = [false, true]

Head survives into flags and tree: the head-flag row marks the foot head — leftmost for the trochee (the foot Lamont's Iamb penalises), rightmost for the iamb (the foot Trochee penalises) — and the prosodic tree carries the same head profile, reduced here through Foot.headFlags_toProsTree. The trochaic vs iambic stress survives the functor identically.