Expressivity: OT, Harmonic Grammar, and MaxEnt

How the frameworks' expressive powers relate ([PS93]; [SL06] ch. 14; [Pat09]; [CP11b]): with exponentially separated weights HG's argmax agrees with OT's lexicographic comparison, so OT ⊆ HG; as the rationality parameter α → ∞, MaxEnt recovers categorical OT; and the containment is strict — cumulativity, summed low-weight violations overpowering a single high-weight one, is HG-expressible but not OT-expressible.

Main definitions

• expWeights, ExponentiallySeparated: the HG reading of an OT ranking.
• RealizationProblem: inputs, per-input candidates, violation profiles, and the target mapping a grammar must realize; IsHGRealizable, IsOTRealizable — realizability by a non-negative weighting / a ranking.
• RealizationProblem.ercs: the problem's winner–loser ERCs ([Pri02]).

Main results

• ot_lex_imp_higher_harmony: lex dominance gives higher harmony under exponentially separated weights.
• maxent_ot_limit: as α → ∞, MaxEnt concentrates on the OT winner.
• RealizationProblem.realizedByRanking_iff_satisfiedBy: OT-realization is ERC satisfaction, so OT-realizability is consistency of the problem's ERC set (isOTRealizable_iff_linearExtensions_nonempty; [Pri02]).
• RealizationProblem.IsOTRealizable.isHGRealizable and hg_strictly_contains_ot: OT ⊆ HG, strictly — the witness is [CP11b]'s abstract Lyman's Law instance (eq 18-19, after [IM86]).
• RealizationProblem.isOTRealizable_iff_isPartialOrderRealizable: categorically, partially ordered grammars add nothing over OT — their advantage is probabilistic (OptimalityTheory.winProb).

OT → HG weights

An OT ranking is a List (Constraint C); as a CON C ranking.length it is just ranking.get. The Harmonic-Grammar reading of that ranking with violation bound M weights coordinate i (0 = highest) by (M+1)^(n−1−i) — the expWeights vector below. So the HG harmony of an OT ranking is harmonyScore ranking.get (expWeights ranking.length M), with no separate weighted-constraint object.

Exponentially separated weights

def HarmonicGrammar.ExponentiallySeparated {n : ℕ} (w : Fin n → ℝ) (M : ℕ) : Prop

Weights are exponentially separated with violation bound M: each weight exceeds M times the sum of all lower-ranked weights.

This ensures that no combination of lower-constraint violations can override a single higher-constraint violation difference, matching OT's strict ranking semantics.

Equations

• HarmonicGrammar.ExponentiallySeparated w M = ((∀ (i : Fin n), 0 < w i) ∧ ∀ (k : Fin n), ↑M * {x : Fin n | x > k}.sum w < w k)

def HarmonicGrammar.expWeights (n M : ℕ) : Fin n → ℝ

Concrete exponential weights: wᵢ = (M+1)^(n−1−i). Constraint 0 (highest-ranked) gets the largest weight (M+1)^(n−1).

Equations

• HarmonicGrammar.expWeights n M i = (↑M + 1) ^ (n - 1 - ↑i)

theorem HarmonicGrammar.expWeights_pos (n M : ℕ) (i : Fin n) : 0 < expWeights n M i

Exponential weights are positive.

theorem HarmonicGrammar.expWeights_separated (n M : ℕ) (hM : 0 < M) : ExponentiallySeparated (expWeights n M) M

Exponential weights are exponentially separated.

Ganging (complement of exponential separation)

def HarmonicGrammar.Ganging (w₁ w₂ w₃ : ℝ) : Prop

Ganging: two constraints with individual weights w₁, w₂ each weaker than a third weight w₃, but jointly stronger.

This is the hallmark of weighted constraint interaction that distinguishes MaxEnt/HG from OT ([HW08]). In OT (strict ranking), a lower-ranked constraint can never override a higher-ranked one regardless of how many violations accumulate. In MaxEnt, constraint effects are additive, so multiple weak constraints can "gang up" to outweigh a strong one.

Equations

• HarmonicGrammar.Ganging w₁ w₂ w₃ = (0 < w₁ ∧ 0 < w₂ ∧ 0 < w₃ ∧ w₁ < w₃ ∧ w₂ < w₃ ∧ w₃ < w₁ + w₂)

theorem HarmonicGrammar.ganging_example : Ganging 2 2 3

Ganging is achievable: weights (2, 2, 3) exhibit ganging.

theorem HarmonicGrammar.no_ganging_when_separated {n : ℕ} (w : Fin n → ℝ) (hw : ExponentiallySeparated w 1) (k : Fin n) : {x : Fin n | x > k}.sum w < w k

With exponentially separated weights (M = 1), each constraint outweighs the total of all lower weights.

theorem HarmonicGrammar.exponential_separation_precludes_ganging {n : ℕ} (w : Fin n → ℝ) (hw : ExponentiallySeparated w 1) (k i j : Fin n) (hi : k < i) (hj : k < j) (hij : i ≠ j) : ¬Ganging (w i) (w j) (w k)

Ganging is precluded by exponential separation: with exponentially separated weights (M = 1), no two distinct lower-ranked constraints i, j can gang up against a higher-ranked k. Their combined weight is at most the total lower weight, which no_ganging_when_separated bounds strictly below w k — contradicting ganging's w k < w i + w j.

HG–OT agreement

theorem HarmonicGrammar.lex_imp_lower_violations {n : ℕ} (w : Fin n → ℝ) (M : ℕ) (va vb : Fin n → ℕ) (hM : ∀ (i : Fin n), va i ≤ M ∧ vb i ≤ M) (hw : ExponentiallySeparated w M) (hlex : toLex va < toLex vb) : Constraints.weightedViolations w va < Constraints.weightedViolations w vb

HG–OT agreement lemma ([SL06]): with exponentially separated weights and bounded violations, lexicographic dominance implies strictly lower weighted violations.

Since harmonyScore = -weightedViolations, this means the lexicographically better candidate has strictly higher harmony.

Proof sketch: decompose the violation-difference sum at the first differing position k.

• For i < k: terms cancel (va(i) = vb(i) by hlex)
• At i = k: wₖ · (vb(k) − va(k)) ≥ wₖ (since vb(k) > va(k))
• For i > k: |wᵢ · (vb(i) − va(i))| ≤ wᵢ · M (by hM)
• Net: ≥ wₖ − M · Σᵢ₍ᵢ>ₖ₎ wᵢ > 0 (by hw)

theorem HarmonicGrammar.strictMonoOn_weightedViolations {n : ℕ} {w : Fin n → ℝ} {M : ℕ} (hw : ExponentiallySeparated w M) : StrictMonoOn (fun (v : Constraints.ViolationProfile n) => Constraints.weightedViolations w (ofLex v)) {v : Constraints.ViolationProfile n | ∀ (i : Fin n), ofLex v i ≤ M}

The algebraic form of the agreement kernel: an exponentially separated weighting reads the M-bounded fragment of the lex order strictly monotonically — [Rig09b]'s order-preserving weight map from the violation semiring to tropical costs, in concrete form.

theorem HarmonicGrammar.ot_lex_imp_higher_harmony {C : Type u_1} (ranking : List (Constraints.Constraint C)) (M : ℕ) (hM : 0 < M) (a b : C) (hbound : ∀ con ∈ ranking, con a ≤ M ∧ con b ≤ M) (hlex : (toLex fun (i : Fin ranking.length) => ranking.get i a) < toLex fun (i : Fin ranking.length) => ranking.get i b) : Constraints.harmonyScore ranking.get (expWeights ranking.length M) a > Constraints.harmonyScore ranking.get (expWeights ranking.length M) b

HG–OT agreement for a concrete candidate type: if candidate a lexicographically beats b on the violation profile induced by ranking, then a has strictly higher harmony than b under the ranking's exponential weights expWeights ranking.length M, provided M bounds all violations. With harmonyScore con w c = -weightedViolations w (· c), the bridge to lex_imp_lower_violations is definitional.

MaxEnt → OT limit

theorem HarmonicGrammar.maxent_concentrates_on_hg_winner {C : Type u_1} [Fintype C] [Nonempty C] [DecidableEq C] {n : ℕ} (con : Constraints.CON C n) (w : Fin n → ℝ) (c_opt : C) (h_opt : ∀ (c : C), c ≠ c_opt → Constraints.harmonyScore con w c < Constraints.harmonyScore con w c_opt) : Filter.Tendsto (fun (α : ℝ) => softmax (α • Constraints.harmonyScore con w) c_opt) Filter.atTop (nhds 1)

MaxEnt concentration on HG winner: as α → ∞, MaxEnt probability concentrates on the candidate with the highest harmony score.

This is softmax_argmax_limit instantiated with harmony scores. The interesting content is in the hypotheses: showing that the HG winner equals the OT winner (§4).

theorem HarmonicGrammar.maxent_ot_limit {C : Type u_1} [Fintype C] [Nonempty C] [DecidableEq C] (ranking : List (Constraints.Constraint C)) (M : ℕ) (hM : 0 < M) (c_opt : C) (hbound : ∀ (c : C), ∀ con ∈ ranking, con c ≤ M) (hlex : ∀ (c : C), c ≠ c_opt → (toLex fun (i : Fin ranking.length) => ranking.get i c_opt) < toLex fun (i : Fin ranking.length) => ranking.get i c) : Filter.Tendsto (fun (α : ℝ) => softmax (α • Constraints.harmonyScore ranking.get (expWeights ranking.length M)) c_opt) Filter.atTop (nhds 1)

MaxEnt → OT limit ([SL06]): as α → ∞, MaxEnt probability concentrates on the OT winner.

Given a constraint ranking with violation bound M and a candidate c_opt that lexicographically beats all competitors, Tendsto (softmax (α • H) c_opt) atTop (𝓝 1).

The proof combines:

1. ot_lex_imp_higher_harmony: lex-better ⟹ higher harmony (HG–OT agreement)
2. softmax_argmax_limit: MaxEnt concentrates on harmony maximizer

The warped-semiring view of the limit

theorem HarmonicGrammar.lse_aggregator_tendsto_winner_harmony {C : Type u_1} [DecidableEq C] (ranking : List (Constraints.Constraint C)) (M : ℕ) (hM : 0 < M) (cands : Finset C) (c_opt : C) (hc_opt : c_opt ∈ cands) (hbound : ∀ c ∈ cands, ∀ con ∈ ranking, con c ≤ M) (hlex : ∀ c ∈ cands, c ≠ c_opt → (toLex fun (i : Fin ranking.length) => ranking.get i c_opt) < toLex fun (i : Fin ranking.length) => ranking.get i c) : Filter.Tendsto (fun (α : ℝ) => Core.Optimization.lseFinset α cands (Constraints.harmonyScore ranking.get (expWeights ranking.length M))) Filter.atTop (nhds (Constraints.harmonyScore ranking.get (expWeights ranking.length M) c_opt))

The lseFinset α aggregator on harmony scores converges to the OT winner's harmony as α → ∞ — the warped-semiring restatement of maxent_ot_limit ([Lit05]'s Maslov dequantization applied to the constraint-framework family): where maxent_ot_limit concentrates the softmax probability on the OT winner, this realises the winner's harmony as the dequantized limit of the warped semiring's additive operator. Composes ot_lex_imp_higher_harmony with argmax_winner_iff_lse_max_limit.

Realizability

Which target mappings each framework realizes.

Realization problems

structure HarmonicGrammar.RealizationProblem (Input : Type u_3) (Output : Type u_4) (n : ℕ) : Type (max u_3 u_4)

A multi-input optimization problem: a target mapping that a single grammar must realize for every input simultaneously (for OT, the data of [TS95]'s ranking problem).

• inputs : Finset Input

  The set of inputs the grammar handles.

• cands : Input → Finset Output

  Candidate set for each input.

• vp : Input → Output → Fin n → ℕ

  Violation profile: vp i o k is the count of constraint k violations incurred by output o from input i.

• target : Input → Output

  The output the grammar must select for each input.

• target_mem (i : Input) : i ∈ self.inputs → self.target i ∈ self.cands i

  Each target output is in its input's candidate set.

def HarmonicGrammar.RealizationProblem.realizedByWeighting {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) (w : Fin n → ℝ) : Prop

w HG-realizes the target: for every input, the target strictly minimizes the weighted violation sum among candidates.

Equations

• P.realizedByWeighting w = ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → Constraints.weightedViolations w (P.vp i (P.target i)) < Constraints.weightedViolations w (P.vp i o)

def HarmonicGrammar.RealizationProblem.IsHGRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) : Prop

Some non-negative weighting realizes the target. Non-negativity is [Pat09]'s standard HG; [CP11b] §4.4 discusses negative weights.

Equations

• P.IsHGRealizable = ∃ (w : Fin n → ℝ), (∀ (k : Fin n), 0 ≤ w k) ∧ P.realizedByWeighting w

def HarmonicGrammar.RealizationProblem.realizedByRanking {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) (σ : OptimalityTheory.Ranking n) : Prop

σ OT-realizes the target: for every input, the target strictly lex-dominates every alternative under the ranking σ.

Equations

• P.realizedByRanking σ = ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → (toLex fun (k : Fin n) => P.vp i (P.target i) (σ k)) < toLex fun (k : Fin n) => P.vp i o (σ k)

def HarmonicGrammar.RealizationProblem.IsOTRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) : Prop

Some constraint ranking realizes the target.

Equations

• P.IsOTRealizable = ∃ (σ : OptimalityTheory.Ranking n), P.realizedByRanking σ

@[instance_reducible]

instance HarmonicGrammar.RealizationProblem.instDecidableRealizedByRankingOfDecidableEq {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] (P : RealizationProblem Input Output n) (σ : OptimalityTheory.Ranking n) : Decidable (P.realizedByRanking σ)

Equations

• P.instDecidableRealizedByRankingOfDecidableEq σ = id inferInstance

@[instance_reducible]

instance HarmonicGrammar.RealizationProblem.instDecidableIsOTRealizableOfDecidableEq {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] (P : RealizationProblem Input Output n) : Decidable P.IsOTRealizable

Equations

• P.instDecidableIsOTRealizableOfDecidableEq = id inferInstance

theorem HarmonicGrammar.RealizationProblem.realizedByRanking_iff_optimal {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] (P : RealizationProblem Input Output n) (σ : OptimalityTheory.Ranking n) : P.realizedByRanking σ ↔ ∀ (i : Input) (hi : i ∈ P.inputs), OptimalityTheory.Tableau.optimal { candidates := P.cands i, profile := fun (o : Output) => toLex fun (k : Fin n) => P.vp i o (σ k), nonempty := ⋯ } = {P.target i}

σ OT-realizes P iff for every input the target is the unique Tableau.optimal of the σ-permuted tableau.

OT-realization is ERC satisfaction

def HarmonicGrammar.RealizationProblem.ercs {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] (P : RealizationProblem Input Output n) : Finset (OptimalityTheory.ERC n)

The winner–loser ERCs of a systemic problem: one comparative row per input and non-target candidate ([Pri02]).

Equations

• P.ercs = P.inputs.biUnion fun (i : Input) => Finset.image (fun (o : Output) => OptimalityTheory.ercOfProfiles (P.vp i (P.target i)) (P.vp i o)) ((P.cands i).erase (P.target i))

theorem HarmonicGrammar.RealizationProblem.mem_ercs {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] {P : RealizationProblem Input Output n} {α : OptimalityTheory.ERC n} : α ∈ P.ercs ↔ ∃ i ∈ P.inputs, ∃ o ∈ P.cands i, o ≠ P.target i ∧ OptimalityTheory.ercOfProfiles (P.vp i (P.target i)) (P.vp i o) = α

theorem HarmonicGrammar.RealizationProblem.realizedByRanking_iff_satisfiedBy {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] {P : RealizationProblem Input Output n} {σ : OptimalityTheory.Ranking n} (hvp : ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → P.vp i (P.target i) ≠ P.vp i o) : P.realizedByRanking σ ↔ ∀ α ∈ P.ercs, OptimalityTheory.ERC.SatisfiedBy σ α

OT-realization is ERC satisfaction ([Pri02]): provided no competitor ties the target's violation profile, σ realizes the target iff σ satisfies every winner–loser ERC.

theorem HarmonicGrammar.RealizationProblem.isOTRealizable_iff_linearExtensions_nonempty {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] {P : RealizationProblem Input Output n} (hvp : ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → P.vp i (P.target i) ≠ P.vp i o) : P.IsOTRealizable ↔ (OptimalityTheory.ERC.linearExtensions P.ercs).Nonempty

OT-realizability is consistency of the problem's ERC set ([Pri02]).

Forward containment — OT ⊆ HG

theorem HarmonicGrammar.RealizationProblem.IsOTRealizable.isHGRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} {P : RealizationProblem Input Output n} (h : P.IsOTRealizable) : P.IsHGRealizable

Forward containment: an OT-realizable problem is HG-realizable, via exponentially separated weights permuted by the ranking (lex_imp_lower_violations, with separation bound the supremum of the finitely many violation counts).

Strict containment — the cumulativity gap

theorem HarmonicGrammar.hg_strictly_contains_ot : ∃ (Input : Type) (Output : Type) (n : ℕ) (P : RealizationProblem Input Output n), P.IsHGRealizable ∧ ¬P.IsOTRealizable

The cumulativity gap: HG with non-negative weights strictly contains OT. The inline witness is [CP11b]'s abstract Lyman's Law instance (eq 18-19, after [IM86]): faithful candidates violating {M1}, {M2}, {M1, M2} against an unfaithful {F}, with the third input alone targeted unfaithful. Weights [3, 2, 2] realize this (2 + 2 > 3 on the third input only), while the winner–loser ERCs F ≫ M1, F ≫ M2, and "some markedness constraint above F" are inconsistent.

Realizability by a partial order

def HarmonicGrammar.RealizationProblem.realizedByPartialOrder {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) (r : Fin n → Fin n → Prop) : Prop

A grammar r POC-realizes the target if every consistent extension realizes it. Since consistent extensions always exist (exists_isConsistent), this is never vacuous.

Equations

• P.realizedByPartialOrder r = ∀ (σ : OptimalityTheory.Ranking n), OptimalityTheory.IsConsistent r σ → P.realizedByRanking σ

def HarmonicGrammar.RealizationProblem.IsPartialOrderRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) : Prop

A RealizationProblem is POC-realizable if some partial order categorically realizes the target.

Equations

• P.IsPartialOrderRealizable = ∃ (r : Fin n → Fin n → Prop), IsPartialOrder (Fin n) r ∧ P.realizedByPartialOrder r

Containments — OT ⊆ POC, POC ⊆ OT (categorical)

theorem HarmonicGrammar.RealizationProblem.IsPartialOrderRealizable.isOTRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} {P : RealizationProblem Input Output n} (h : P.IsPartialOrderRealizable) : P.IsOTRealizable

Every partial-order-realized target is OT-realized, since any single consistent extension realizes it.

theorem HarmonicGrammar.RealizationProblem.IsOTRealizable.isPartialOrderRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} {P : RealizationProblem Input Output n} (h : P.IsOTRealizable) : P.IsPartialOrderRealizable

Every OT-realized target is partial-order-realized — the witness is the σ-induced total ranking, whose unique consistent extension is σ itself.

theorem HarmonicGrammar.RealizationProblem.isOTRealizable_iff_isPartialOrderRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output n) : P.IsOTRealizable ↔ P.IsPartialOrderRealizable

Under categorical realizability, OT and partial orders coincide; the partial order's advantage is probabilistic, captured by winProb.