Expressivity of OT, Harmonic Grammar, and MaxEnt

This file compares the expressive power of Optimality Theory (OT), Harmonic Grammar (HG), and maximum-entropy grammar (MaxEnt). With exponentially separated weights the harmony order of HG agrees with the lexicographic comparison of OT, so every OT grammar is an HG grammar, and as the weights are scaled up MaxEnt concentrates on the OT winner. The containment of OT in HG is strict because of cumulativity, in which several low-weight violations together outweigh a single high-weight one. The comparison follows Smolensky and Legendre, Pater, and Coetzee and Pater, and the cumulativity witness is Coetzee and Pater's version of Itô and Mester's Lyman's Law data.

Main definitions

• ExponentiallySeparated, expWeights: the HG reading of an OT ranking.
• RealizationProblem: a target mapping that one grammar must realize on every input.
• RealizationProblem.IsHGRealizable, RealizationProblem.IsOTRealizable: realizability by a non-negative weighting and by a ranking.
• RealizationProblem.ercs: the winner–loser ERCs of a problem.

Main results

• ot_lex_imp_higher_harmony: lexicographic dominance gives higher harmony under exponentially separated weights.
• maxent_ot_limit: MaxEnt concentrates on the OT winner as the weights are scaled up.
• RealizationProblem.realizedByRanking_iff_satisfiedBy: OT-realization is ERC satisfaction.
• RealizationProblem.IsOTRealizable.isHGRealizable, hg_strictly_contains_ot: OT is strictly contained in HG.
• RealizationProblem.isOTRealizable_iff_isPartialOrderRealizable: partially ordered grammars realize exactly the OT-realizable targets, so their advantage is probabilistic.

References

• A. Prince and P. Smolensky, Optimality Theory: Constraint Interaction in Generative Grammar (1993)
• P. Smolensky and G. Legendre, The Harmonic Mind: From Neural Computation to Optimality-Theoretic Grammar (2006)
• J. Pater, Morpheme-specific phonology: Constraint indexation and inconsistency resolution (2009)
• A. W. Coetzee and J. Pater, The Place of Variation in Phonological Theory (2011)
• J. Itô and A. Mester, The Phonology of Voicing in Japanese (1986)
• B. Hayes and C. Wilson, A Maximum Entropy Model of Phonotactics and Phonotactic Learning (2008)
• B. Tesar and P. Smolensky, The Learnability of Optimality Theory (1995)
• A. Prince, Entailed Ranking Arguments (2002)
• J. Riggle, Violation Semirings in Optimality Theory (2009)

OT → HG weights

An OT ranking is a List (Constraint C); as a ConstraintSet C (Fin 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 when each weight exceeds M times the sum of all lower-ranked weights. No combination of lower-ranked violations can then override a single higher-ranked violation difference, as under OT's strict ranking.

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 → ℝ

The exponential weights give constraint i the weight (M+1)^(n−1−i), so the highest-ranked constraint 0 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

Two constraints with weights w₁ and w₂ gang against a third with weight w₃ when each is weaker than w₃ but together they are stronger. Under OT's strict ranking a lower-ranked constraint never overrides a higher-ranked one, however many violations accumulate.

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

The weights 2, 2, and 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)

With exponentially separated weights (M = 1), no two distinct lower-ranked constraints i and j gang against a higher-ranked k, since their combined weight is at most the total lower weight, which no_ganging_when_separated bounds strictly below w k.

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) : w ⬝ᵥ Nat.cast ∘ va < w ⬝ᵥ Nat.cast ∘ vb

The HG–OT agreement lemma states that with exponentially separated weights and bounded violations, lexicographic dominance implies strictly lower weighted violations, so the lexicographically better candidate has strictly higher harmony. The proof splits the difference of the weighted sums at the first coordinate k where the profiles differ. Earlier terms cancel, the term at k contributes at least wₖ, and the later terms total at most M times the sum of the lower weights, which separation bounds below wₖ.

theorem HarmonicGrammar.strictMonoOn_dotProduct {n : ℕ} {w : Fin n → ℝ} {M : ℕ} (hw : ExponentiallySeparated w M) : StrictMonoOn (fun (v : OptimalityTheory.ViolationProfile n) => w ⬝ᵥ Nat.cast ∘ ofLex v) {v : OptimalityTheory.ViolationProfile n | ∀ (i : Fin n), ofLex v i ≤ M}

An exponentially separated weighting is strictly monotone on the M-bounded part of the lexicographic order. This is a concrete form of [Rig09b]'s order-preserving map from the violation semiring to tropical costs.

theorem HarmonicGrammar.ot_lex_imp_higher_harmony {C : Type u_1} (ranking : List (OptimalityTheory.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) : harmonyScore ranking.get (expWeights ranking.length M) a > harmonyScore ranking.get (expWeights ranking.length M) b

If candidate a lexicographically beats b on the violation profile induced by ranking and M bounds all violations, then a has strictly higher harmony than b under the exponential weights expWeights ranking.length M.

MaxEnt → OT limit

theorem HarmonicGrammar.maxent_ot_limit {C : Type u_1} [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C] (ranking : List (OptimalityTheory.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 (α : ℝ) => (maxEnt (OptimalityTheory.ConstraintSet.violations ranking.get) (α • expWeights ranking.length M)).real {c_opt}) Filter.atTop (nhds 1)

Scaling exponentially separated weights concentrates the MaxEnt distribution on a candidate that lexicographically beats every competitor under a ranking with violation bound M, since it has the greatest harmony (ot_lex_imp_higher_harmony).

Realizability

A framework realizes a target mapping when one of its grammars selects the target output on every input.

Realization problems

structure HarmonicGrammar.RealizationProblem (Input : Type u_4) (Output : Type u_5) (ι : Type u_6) : Type (max (max u_4 u_5) u_6)

A realization problem is a target mapping that a single grammar over the constraint set con must realize on every input at once. For OT it is the data of [TS95]'s ranking problem.

• inputs : Finset Input

  The grammar handles a finite set of inputs.

• cands : Input → Finset Output

  Each input has a finite candidate set.

• con : OptimalityTheory.ConstraintSet (Input × Output) ι

  The constraints, evaluated on input–output mappings.

• target : Input → Output

  The grammar must select the target output on 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} {ι : Type u_3} [Fintype ι] (P : RealizationProblem Input Output ι) (w : ι → ℝ) : Prop

The weighting w HG-realizes the target when on every input the target harmonically dominates every other candidate.

Equations

• P.realizedByWeighting w = ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → HarmonicGrammar.harmonyDominates P.con w (i, P.target i) (i, o)

def HarmonicGrammar.RealizationProblem.IsHGRealizable {Input : Type u_1} {Output : Type u_2} {ι : Type u_3} [Fintype ι] (P : RealizationProblem Input Output ι) : Prop

A problem is HG-realizable when some non-negative weighting realizes its target. Non-negativity is [Pat09]'s standard HG; [CP11b] also discuss negative weights.

Equations

• P.IsHGRealizable = ∃ (w : ι → ℝ), 0 ≤ w ∧ P.realizedByWeighting w

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

The ranking σ OT-realizes the target when on every input it picks the target, which strictly lex-dominates every alternative under σ.

Equations

• P.realizedByRanking σ = ∀ i ∈ P.inputs, OptimalityTheory.PicksAt P.cands P.con σ i (P.target i)

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

A problem is OT-realizable when some constraint ranking realizes its target.

Equations

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

@[instance_reducible]

instance HarmonicGrammar.RealizationProblem.instDecidableRealizedByRankingOfDecidableEq {Input : Type u_1} {Output : Type u_2} {ι : Type u_3} {n : ℕ} [DecidableEq Output] (P : RealizationProblem Input Output ι) (σ : 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 (Fin n)) : Decidable P.IsOTRealizable

Equations

• P.instDecidableIsOTRealizableOfDecidableEq = id inferInstance

theorem HarmonicGrammar.RealizationProblem.realizedByRanking_iff_optimal {Input : Type u_1} {Output : Type u_2} {ι : Type u_3} {n : ℕ} [DecidableEq Output] (P : RealizationProblem Input Output ι) (σ : OptimalityTheory.Ranking ι n) : P.realizedByRanking σ ↔ ∀ (i : Input) (hi : i ∈ P.inputs), { candidates := P.cands i, profile := fun (o : Output) => toLex fun (p : Fin n) => P.con (σ p) (i, o), nonempty := ⋯ }.optimal = {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} {ι : Type u_3} [Fintype ι] [DecidableEq Output] (P : RealizationProblem Input Output ι) : Finset (OptimalityTheory.ERC ι)

The winner–loser ERCs of a problem have one comparative row for each input and non-target candidate ([Pri02]).

Equations

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

theorem HarmonicGrammar.RealizationProblem.mem_ercs {Input : Type u_1} {Output : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq Output] {P : RealizationProblem Input Output ι} {α : OptimalityTheory.ERC ι} : α ∈ P.ercs ↔ ∃ i ∈ P.inputs, ∃ o ∈ P.cands i, o ≠ P.target i ∧ (OptimalityTheory.ercOfProfiles (fun (x : ι) => P.con x (i, P.target i)) fun (x : ι) => P.con x (i, o)) = α

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

Provided no competitor ties the target's violation profile, σ realizes the target iff σ satisfies every winner–loser ERC ([Pri02]).

theorem HarmonicGrammar.RealizationProblem.isOTRealizable_iff_linearExtensions_nonempty {Input : Type u_1} {Output : Type u_2} {n : ℕ} [DecidableEq Output] {P : RealizationProblem Input Output (Fin n)} (hvp : ∀ i ∈ P.inputs, ∀ o ∈ P.cands i, o ≠ P.target i → (fun (x : Fin n) => P.con x (i, P.target i)) ≠ fun (x : Fin n) => P.con x (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 (Fin n)} (h : P.IsOTRealizable) : P.IsHGRealizable

An OT-realizable problem is HG-realizable by exponentially separated weights permuted by the ranking, with the largest violation count as the separation bound.

Strict containment — the cumulativity gap

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

HG with non-negative weights strictly contains OT. The witness is [CP11b]'s abstract Lyman's Law instance after [IM86], in which faithful candidates violate {M1}, {M2}, and {M1, M2} against an unfaithful {F} and only the third input targets the unfaithful output. The weights [3, 2, 2] realize it, since 2 + 2 > 3 holds 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 (Fin 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 (Fin n) n), OptimalityTheory.IsConsistent r σ → P.realizedByRanking σ

def HarmonicGrammar.RealizationProblem.IsPartialOrderRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : RealizationProblem Input Output (Fin 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 (Fin 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 (Fin 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 (Fin n)) : P.IsOTRealizable ↔ P.IsPartialOrderRealizable

Under categorical realizability, OT and partial orders coincide; the partial order's advantage is probabilistic, the uniform measure on its linear extensions.