Magri (2025): Constraint Interaction in Probabilistic Phonology

Hayes and Zuraw observed that the rates of a variable process on four forms crossing two independent factors lie on two sigmoids shifted against each other at shared abscissas, which is to say that their logits differ by a constant along each factor (§2.2, exists_shiftedSigmoids_iff). Magri asks which modes of constraint interaction predict this. In harmony-based probabilistic phonology a form's candidates have probabilities proportional to a positive harmony of their violation profiles (23) (grammar), and the answer is a characterization (§5.5): the grammar predicts the generalization (24) iff its harmony is separable, a product of powers of positive unary functions each fed the violations of a single constraint (30) (predictsHZ_iff_separable). Equivalently the harmony of any profile is the product of the harmonies of its single-constraint profiles (32).

The maximum entropy grammar (14) is the MaxEnt distribution of the form's candidates (grammar_meHarmony), and any separable grammar is the maximum entropy grammar of the constraints rescaled by Ĉₖ = −log hₖ(Cₖ) (33), whose violations are no longer integers (35) (grammar_prod_rpow). Feeding the weighted violations to the inverse function instead of the exponential (27) is not separable: on the Tagalog square, whose rows and columns are independent relative to six of Zuraw and Hayes's constraints (§2.3), it satisfies the constant difference only when the two prefix constraints have equal weights or the two stem-nasal constraints have none (§4.4, inverseHarmony_hz_tagalog_iff).

Implementation notes

• A harmony is a function (Fin n → ℕ) → ℝ of violation profiles, positive and normalized as §4.1 assumes; decreasingness is not needed. PredictsHZ is (24) for forms with the two candidates YES and NO, read as true and false. Its log-odds form holds exactly for any number of candidates (Separable.interaction_logOdds_eq_zero), where §3.5 states the logits only approximately.
• The converse direction takes one square per constraint. Letting constraint k vary along the rows and the others along the columns gives H (update u k c) = H (single k c) * H (update u k 0), whence (32) by induction on the constraints.
• The Tagalog square crosses the prefix constructions maŋ- OTHER and maŋ- RED-, which the paper calls maŋ- and paŋ- (footnote 1), with the stems /b/ and /k/. Its constraints are Zuraw and Hayes's less *[root m/n/ŋ, which penalizes every substitution (footnote 3).
• The weights of (30) add no generality to the class of separable harmonies, since hₖ ^ wₖ is itself a unary function (separable_iff_exists_prod); they matter to the grammars a learner can reach, not to the characterization.

References

• [magri-2025]
• [ZH17]
• [Hay22]

Shifted sigmoids (§2.1–2.2)

theorem Magri2025.exists_shiftedSigmoids_iff {X : Type u_1} (sq : HarmonicGrammar.Square X) {r : X → ℝ} (hr : ∀ (x : X), r x ∈ Set.Ioo 0 1) : (∃ (x₁ : ℝ) (x₂ : ℝ) (δ : ℝ), r sq.tl = x₁.sigmoid ∧ r sq.tr = x₂.sigmoid ∧ r sq.bl = (x₁ + δ).sigmoid ∧ r sq.br = (x₂ + δ).sigmoid) ↔ (sq.interaction fun (x : X) => (r x).logit) = 0

Hayes and Zuraw's generalization (7). Four rates lie on two sigmoids at shared abscissas, the bottom one shifted by δ, exactly when the differences of their logits along the two rows agree ((9), §2.2).

Harmony-based grammars (§4)

noncomputable def Magri2025.logOdds {n : ℕ} {X : Type u_1} {Y : Type u_2} (H : (Fin n → ℕ) → ℝ) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (a b : Y) (x : X) : ℝ

The log-odds of candidate a against b for form x under harmony H, the log of the ratio of their harmonies, which is the log of the ratio of their probabilities (log_grammar_div).

Equations

• Magri2025.logOdds H con a b x = Real.log ((H fun (x_1 : Fin n) => con x_1 (x, a)) / H fun (x_1 : Fin n) => con x_1 (x, b))

noncomputable def Magri2025.grammar {n : ℕ} {X : Type u_1} {Y : Type u_2} [MeasurableSpace Y] (H : (Fin n → ℕ) → ℝ) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (x : X) : MeasureTheory.Measure Y

The harmony-based grammar (23) realizes form x as candidate y with probability proportional to the harmony of the violation profile of (x, y).

Equations

• Magri2025.grammar H con x = MeasureTheory.Measure.count.tilted fun (y : Y) => Real.log (H fun (x_1 : Fin n) => con x_1 (x, y))

theorem Magri2025.grammar_real_singleton {n : ℕ} {H : (Fin n → ℕ) → ℝ} {X : Type u_1} {Y : Type u_2} [MeasurableSpace Y] [Fintype Y] [MeasurableSingletonClass Y] (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (x : X) (y : Y) : (grammar H con x).real {y} = (H fun (x_1 : Fin n) => con x_1 (x, y)) / ∑ z : Y, H fun (x_1 : Fin n) => con x_1 (x, z)

theorem Magri2025.log_grammar_div {n : ℕ} {H : (Fin n → ℕ) → ℝ} {X : Type u_1} {Y : Type u_2} [MeasurableSpace Y] [Fintype Y] [MeasurableSingletonClass Y] (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (x : X) (a b : Y) : Real.log ((grammar H con x).real {a} / (grammar H con x).real {b}) = logOdds H con a b x

The log-odds of two candidates are the log of the ratio of their probabilities, the normalizing constant cancelling.

theorem Magri2025.logit_grammar_of_pair {n : ℕ} {H : (Fin n → ℕ) → ℝ} {X : Type u_1} {Y : Type u_2} [MeasurableSpace Y] [Fintype Y] [MeasurableSingletonClass Y] [DecidableEq Y] (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (x : X) {a b : Y} (hab : a ≠ b) (huniv : Finset.univ = {a, b}) : ((grammar H con x).real {a}).logit = logOdds H con a b x

When the form has only the two candidates, the logit of the first is its log-odds (17).

def Magri2025.PredictsHZ {n : ℕ} (H : (Fin n → ℕ) → ℝ) : Prop

A harmony predicts HZ's generalization (24) when, on every square of forms with the two candidates YES and NO whose rows and columns are independent relative to the constraints, the logits of YES differ by the same amount along both rows.

Equations

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

def Magri2025.Separable {n : ℕ} (H : (Fin n → ℕ) → ℝ) : Prop

A harmony is separable (30) when it is a product of powers of positive unary functions, each fed the violations of a single constraint.

Equations

• Magri2025.Separable H = ∃ (h : Fin n → ℕ → ℝ) (w : Fin n → ℝ), (∀ (k : Fin n) (c : ℕ), 0 < h k c) ∧ ∀ (v : Fin n → ℕ), H v = ∏ k : Fin n, h k (v k) ^ w k

theorem Magri2025.separable_iff_exists_prod {n : ℕ} {H : (Fin n → ℕ) → ℝ} : Separable H ↔ ∃ (g : Fin n → ℕ → ℝ), (∀ (k : Fin n) (c : ℕ), 0 < g k c) ∧ ∀ (v : Fin n → ℕ), H v = ∏ k : Fin n, g k (v k)

The weights of (30) add no generality, since a separable harmony is a product of positive unary functions.

theorem Magri2025.Separable.pos {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hH : Separable H) (v : Fin n → ℕ) : 0 < H v

Separable harmonies predict the generalization (§5.4)

theorem Magri2025.Separable.interaction_logOdds_eq_zero {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hH : Separable H) {X : Type u_1} {Y : Type u_2} {sq : HarmonicGrammar.Square X} {con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)} (hind : sq.Independent con) (a b : Y) : sq.interaction (logOdds H con a b) = 0

Under a separable harmony the log-odds of any two candidates have zero interaction on every independent square, whatever the candidates, since the log-odds is a sum of per-constraint terms.

theorem Magri2025.Separable.predictsHZ {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hH : Separable H) : PredictsHZ H

Separable harmonies predict HZ's generalization (§5.4).

Only separable harmonies predict the generalization (§5.5)

theorem Magri2025.PredictsHZ.mul_update {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hH : PredictsHZ H) (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (h0 : H 0 = 1) (u : Fin n → ℕ) (k : Fin n) (c : ℕ) : H (Function.update u k c) = H (Pi.single k c) * H (Function.update u k 0)

A harmony predicting HZ's generalization splits off the violations of any one constraint.

theorem Magri2025.PredictsHZ.eq_prod_single {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hH : PredictsHZ H) (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (h0 : H 0 = 1) (v : Fin n → ℕ) : H v = ∏ k : Fin n, H (Pi.single k (v k))

A harmony predicting HZ's generalization satisfies (32).

theorem Magri2025.predictsHZ_iff_separable {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (h0 : H 0 = 1) : PredictsHZ H ↔ Separable H

The characterization of §5.5. A positive normalized harmony predicts HZ's generalization iff it is separable.

theorem Magri2025.separable_iff_eq_prod_single {n : ℕ} {H : (Fin n → ℕ) → ℝ} (hpos : ∀ (v : Fin n → ℕ), 0 < H v) (h0 : H 0 = 1) : Separable H ↔ ∀ (v : Fin n → ℕ), H v = ∏ k : Fin n, H (Pi.single k (v k))

Separability (30) as (32), the harmony of a profile being the product of the harmonies of its single-constraint profiles.

Maximum entropy harmony (§3, §5.1)

noncomputable def Magri2025.meHarmony {n : ℕ} (w r : Fin n → ℝ) : ℝ

Maximum entropy harmony (14b) of a real-valued violation profile.

Equations

• Magri2025.meHarmony w r = Real.exp (-∑ k : Fin n, w k * r k)

theorem Magri2025.grammar_meHarmony {n : ℕ} {X : Type u_1} {Y : Type u_2} [Fintype Y] [MeasurableSpace Y] (w : Fin n → ℝ) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (x : X) : grammar (fun (v : Fin n → ℕ) => meHarmony w fun (k : Fin n) => ↑(v k)) con x = HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x_1 : Y) => (x, x_1)) con).violations w

The maximum entropy grammar (14) is the MaxEnt distribution of the form's candidates.

theorem Magri2025.separable_meHarmony {n : ℕ} (w : Fin n → ℝ) : Separable fun (v : Fin n → ℕ) => meHarmony w fun (k : Fin n) => ↑(v k)

Maximum entropy harmony is separable (29), with hₖ(x) = exp(−x) for every constraint.

theorem Magri2025.predictsHZ_meHarmony {n : ℕ} (w : Fin n → ℝ) : PredictsHZ fun (v : Fin n → ℕ) => meHarmony w fun (k : Fin n) => ↑(v k)

Maximum entropy harmony predicts HZ's generalization (§3.6).

Constraint rescaling (§5.3)

noncomputable def Magri2025.rescale {n : ℕ} (h : Fin n → ℕ → ℝ) (k : Fin n) (c : ℕ) : ℝ

The rescaled constraint (33), Ĉₖ = −log hₖ(Cₖ).

Equations

• Magri2025.rescale h k c = -Real.log (h k c)

theorem Magri2025.prod_rpow_eq_meHarmony_rescale {n : ℕ} {h : Fin n → ℕ → ℝ} (hpos : ∀ (k : Fin n) (c : ℕ), 0 < h k c) (w : Fin n → ℝ) (v : Fin n → ℕ) : ∏ k : Fin n, h k (v k) ^ w k = meHarmony w fun (k : Fin n) => rescale h k (v k)

Every separable harmony is maximum entropy harmony of the rescaled violations (34).

theorem Magri2025.grammar_prod_rpow {n : ℕ} {X : Type u_1} {Y : Type u_2} [Fintype Y] [MeasurableSpace Y] {h : Fin n → ℕ → ℝ} (hpos : ∀ (k : Fin n) (c : ℕ), 0 < h k c) (w : Fin n → ℝ) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) (x : X) : grammar (fun (v : Fin n → ℕ) => ∏ k : Fin n, h k (v k) ^ w k) con x = HarmonicGrammar.maxEnt (fun (y : Y) (k : Fin n) => rescale h k (con k (x, y))) w

Any separable grammar is the maximum entropy grammar of the rescaled constraints (35), whose violations need not be integers.

theorem Magri2025.strictMono_rescale {n : ℕ} {h : Fin n → ℕ → ℝ} {k : Fin n} (hpos : ∀ (c : ℕ), 0 < h k c) (hanti : StrictAnti (h k)) : StrictMono (rescale h k)

Rescaling preserves the order of violation counts (footnote 14).

theorem Magri2025.rescale_eq_zero_iff {n : ℕ} {h : Fin n → ℕ → ℝ} {k : Fin n} (hpos : ∀ (c : ℕ), 0 < h k c) (hanti : StrictAnti (h k)) (h0 : h k 0 = 1) {c : ℕ} : rescale h k c = 0 ↔ c = 0

A rescaled constraint is satisfied iff the original is (footnote 15).

theorem Magri2025.rescale_nonneg {n : ℕ} {h : Fin n → ℕ → ℝ} {k : Fin n} (hpos : ∀ (c : ℕ), 0 < h k c) (hanti : StrictAnti (h k)) (h0 : h k 0 = 1) (c : ℕ) : 0 ≤ rescale h k c

Rescaled violations are nonnegative (footnote 16).

The Tagalog square (§2.1, §2.3)

def Magri2025.tagalogSquare : HarmonicGrammar.Square (ZurawHayes2017.Prefix × Zuraw2010.StemC)

The Tagalog square (11), maŋ- OTHER and maŋ- RED- crossed with /b/ and /k/.

Equations

• Magri2025.tagalogSquare = ZurawHayes2017.square ZurawHayes2017.Prefix.mangOther ZurawHayes2017.Prefix.mangRed Zuraw2010.StemC.b Zuraw2010.StemC.k

def Magri2025.tagalogConstraints : OptimalityTheory.ConstraintSet ZurawHayes2017.Candidate (Fin 6)

The six constraints of §2.3, *NC, *NC̥, *[stem ŋ, *[stem ŋ/n, and the Uniformity constraints of the two prefixes.

Equations

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

theorem Magri2025.tagalog_independent : tagalogSquare.Independent tagalogConstraints

Prefixes and stems are independent dimensions (§2.3, Figure 3), the markedness constraints being insensitive to the prefix and the Uniformity constraints to the stem.

The inverse harmony (§4.4)

noncomputable def Magri2025.inverseHarmony {n : ℕ} (w : Fin n → ℝ) (v : Fin n → ℕ) : ℝ

The inverse harmony (27) feeds the weighted violations to h(x) = 1/(1+x) in place of maximum entropy's exp(−x).

Equations

• Magri2025.inverseHarmony w v = (1 + w ⬝ᵥ Nat.cast ∘ v)⁻¹

theorem Magri2025.inverseHarmony_pos {n : ℕ} {w : Fin n → ℝ} (hw : ∀ (k : Fin n), 0 ≤ w k) (v : Fin n → ℕ) : 0 < inverseHarmony w v

theorem Magri2025.inverseHarmony_hz_tagalog_iff {w : Fin 6 → ℝ} (hw : ∀ (k : Fin 6), 0 ≤ w k) : tagalogSquare.interaction (logOdds (inverseHarmony w) tagalogConstraints Zuraw2010.SubSt.yes Zuraw2010.SubSt.no) = 0 ↔ w 4 = w 5 ∨ w 2 = 0 ∧ w 3 = 0

On the Tagalog square, the inverse harmony satisfies HZ's identity (28) only when the two prefix constraints have equal weights, or the two stem-nasal constraints have none (§4.4 and footnote 11).

theorem Magri2025.not_separable_inverseHarmony {w : Fin 6 → ℝ} (hw : ∀ (k : Fin 6), 0 ≤ w k) (h45 : w 4 ≠ w 5) (h2 : w 2 ≠ 0) : ¬Separable (inverseHarmony w)

The inverse harmony is not separable once the prefix constraints differ in weight and a stem-nasal constraint is active.