MaxEnt Harmonic Grammar @cite{storme-2026}

MaxEnt grammars assign probabilities to input→output mappings using the softmax function over weighted constraint violations — the probabilistic generalization of OT (where α → ∞ recovers categorical optimization; see softmax_argmax_limit).

This module extends the basic MaxEnt setup with systemic constraints (@cite{storme-2026}): constraints that evaluate tuples of mappings jointly (e.g., *HOMOPHONY penalizes distinct inputs that map to the same output). Systemic constraints require evaluating a joint distribution over the product space of all input→output mappings, then marginalizing to recover individual mapping probabilities.

Architecture

• WeightedConstraint extends NamedConstraint with a weight : ℚ field
• harmonyScore computes -Σ wⱼ · Cⱼ(c) in ℚ (computable)
• MaxEntGrammar packages inputs, candidate generation, and weighted constraints
• SystemicConstraint evaluates tuples of outputs (different type signature)
• jointHarmonyScore combines classical + systemic scores over the product space
• marginalProb marginalizes the joint to recover individual mapping probabilities

Key theorem

marginal_eq_classical_when_no_systemic: when systemic constraint weight = 0, the marginalized probability equals classical MaxEnt. This is because the joint score decomposes additively ⇒ the joint distribution factorizes ⇒ each marginal equals its factor.

structure Theories.Phonology.HarmonicGrammar.MaxEntGrammar (Input Output : Type) : Type

A MaxEnt grammar: inputs, candidate generation, and weighted constraints. Probability of mapping input i to output o is proportional to exp(harmonyScore(i, o)).

• inputs : List Input

  The set of inputs (underlying forms).

• gen : Input → List Output

  Candidate generator: produces output candidates for each input.

• constraints : List (WeightedConstraint (Input × Output))

  Weighted constraints evaluating input–output pairs.

noncomputable def Theories.Phonology.HarmonicGrammar.MaxEntGrammar.prob {I O : Type} [Fintype O] (g : MaxEntGrammar I O) (i : I) (o : O) : ℝ

Classical MaxEnt probability: P(o | i) = softmax over gen(i).

This is the standard MaxEnt phonology probability, without systemic constraints. Uses softmax from RationalAction with α = 1.

Equations

• g.prob i o = Core.softmax (fun (o' : O) => Theories.Phonology.HarmonicGrammar.harmonyScoreR g.constraints (i, o')) 1 o

structure Theories.Phonology.HarmonicGrammar.SystemicConstraint (n : ℕ) (O : Type) : Type

A systemic constraint evaluates a tuple of outputs — one per input — rather than individual input→output pairs.

Example: *HOMOPHONY counts pairs of distinct inputs that map to the same output. This cannot be decomposed into per-mapping evaluations.

n is the number of inputs; the tuple Fin n → O assigns an output to each input index.

• name : String

  Constraint name.

• weight : ℚ

  Constraint weight.

• eval : (Fin n → O) → ℕ

  Evaluation function: how many violations does this output tuple incur?

def Theories.Phonology.HarmonicGrammar.homophonyAvoidance {n : ℕ} {O : Type} [DecidableEq O] (w : ℚ) : SystemicConstraint n O

*HOMOPHONY: penalizes output tuples where distinct inputs receive the same output. Counts the number of colliding pairs.

For n inputs, evaluates |{(i,j) : i < j ∧ f(i) = f(j)}|.

Equations

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

def Theories.Phonology.HarmonicGrammar.systemicScore {n : ℕ} {O : Type} (systemicConstraints : List (SystemicConstraint n O)) (f : Fin n → O) : ℚ

Systemic constraint score for an output tuple (ℚ, computable). This is the coupling component: Σₖ (-wₖ · Sₖ(f)).

Equations

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

noncomputable def Theories.Phonology.HarmonicGrammar.systemicScoreR {n : ℕ} {O : Type} (systemicConstraints : List (SystemicConstraint n O)) (f : Fin n → O) : ℝ

Systemic constraint score as ℝ.

Equations

• Theories.Phonology.HarmonicGrammar.systemicScoreR systemicConstraints f = ↑(Theories.Phonology.HarmonicGrammar.systemicScore systemicConstraints f)

def Theories.Phonology.HarmonicGrammar.jointHarmonyScore {n : ℕ} {I O : Type} (inputs : Fin n → I) (classicalConstraints : List (WeightedConstraint (I × O))) (systemicConstraints : List (SystemicConstraint n O)) (f : Fin n → O) : ℚ

Joint harmony score over the product space. Combines classical per-mapping scores with systemic tuple-level scores.

H_joint(f) = Σᵢ H_classical(iᵢ, f(i)) + Σₖ (-wₖ · Sₖ(f))

where f : Fin n → O is the full output tuple.

Equations

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

noncomputable def Theories.Phonology.HarmonicGrammar.maxEntCoupled {n : ℕ} {I O : Type} [Fintype O] [DecidableEq O] (inputs : Fin n → I) (classicalConstraints : List (WeightedConstraint (I × O))) (systemicConstraints : List (SystemicConstraint n O)) : Core.CoupledSoftmax (Fin n) O

MaxEnt grammar with systemic constraints as a CoupledSoftmax.

• componentScore i v = harmonyScoreR(classicalConstraints, (inputs i, v))
• couplingScore f = systemicScoreR(systemicConstraints, f)

The joint probability is softmax(totalScore, 1) over all Fin n → O output tuples. The marginal at position i recovers the individual mapping probability under systemic pressure.

Equations

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

noncomputable def Theories.Phonology.HarmonicGrammar.marginalProb {n : ℕ} {I O : Type} [Fintype O] [DecidableEq O] [Nonempty O] (inputs : Fin n → I) (classicalConstraints : List (WeightedConstraint (I × O))) (systemicConstraints : List (SystemicConstraint n O)) (i : Fin n) (o : O) : ℝ

Marginal probability: marginalize the joint distribution to get the probability of a specific input→output mapping.

P_marginal(oᵢ | iᵢ) = Σ_{f : f(i) = oᵢ} P_joint(f)

This is Storme's key equation: the marginal recovers individual mapping probabilities that reflect systemic pressure. Defined through CoupledSoftmax.marginal so that factorization follows from marginal_eq_independent_when_uncoupled.

Equations

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

theorem Theories.Phonology.HarmonicGrammar.marginal_eq_classical_when_no_systemic {n : ℕ} {I O : Type} [Fintype O] [DecidableEq O] [Nonempty O] (inputs : Fin n → I) (classicalConstraints : List (WeightedConstraint (I × O))) (systemicConstraints : List (SystemicConstraint n O)) (h_zero : ∀ sc ∈ systemicConstraints, sc.weight = 0) (i : Fin n) (o : O) : marginalProb inputs classicalConstraints systemicConstraints i o = Core.softmax (fun (o' : O) => harmonyScoreR classicalConstraints (inputs i, o')) 1 o

Factorization: when systemic constraint weights are all zero, the marginal equals the classical MaxEnt probability.

With zero systemic weights, the coupling score is constant (= 0), so marginal_eq_independent_when_uncoupled applies: the joint factorizes and each marginal equals its independent per-item softmax.