Noisy harmonic grammar

Boersma and Pater make harmonic grammar stochastic by adding independent Gaussian noise to every constraint weight at each evaluation, so that a candidate wins with the probability that its noisy harmony is the highest. Flemming reads this as a random utility model whose utilities are the noisy harmonies. The candidates share the weights, so their noisy harmonies are correlated, and the model is the choice rule choiceProb at the pushforward of the weight noise rather than at a product of independent laws. The harmony difference of two candidates is Gaussian with variance v * (d ⬝ᵥ d) for their violation difference d, so how noisy a comparison is depends on the violation profile and not only on the harmonies, unlike in MaxEnt, where the utilities are independent.

Main definitions

• weightNoise: independent N(0, v) noise on every constraint weight.
• weightNoiseChoiceProb: the probability that a candidate has the highest harmony under noisy weights.

Main results

• weightNoiseChoiceProb_eq_choiceProb_map: noisy harmonic grammar is the random utility model whose joint law is that of the noisy harmonies.
• map_weightNoise_harmonyScore_sub: the harmony difference of two candidates is Gaussian with variance v * (d ⬝ᵥ d).
• variance_harmonyScore_sub, covariance_harmonyScore_sub: the variances and covariances of the harmony differences.
• weightNoise_setOf_harmonyScore_lt, weightNoiseChoiceProb_of_forall_ne_eq, weightNoiseChoiceProb_fin_two: the probability that one candidate beats another is the probit of their harmony difference over its standard deviation.

Implementation notes

The noise has variance v : ℝ≥0, as in mathlib's gaussianReal; Boersma and Pater take v = 1. Flemming's normal MaxEnt, with independent Gaussian noise on the candidates' harmonies, needs no definition: it is choiceProb (Measure.pi fun c ↦ gaussianReal (harmonyScore con w c) v), with binary case choiceProb_pi_gaussianReal. His censored variant, which clamps noisy weights at zero, has no closed form and is not formalized.

References

• [BP16]
• [Fle21]

noncomputable def HarmonicGrammar.weightNoise (ι : Type u_3) [Fintype ι] (v : NNReal) : MeasureTheory.Measure (ι → ℝ)

The weight noise of noisy harmonic grammar perturbs each constraint weight by independent N(0, v) noise.

Equations

• HarmonicGrammar.weightNoise ι v = MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 v

instance HarmonicGrammar.instIsProbabilityMeasureForallRealWeightNoise {ι : Type u_2} [Fintype ι] (v : NNReal) : MeasureTheory.IsProbabilityMeasure (weightNoise ι v)

noncomputable def HarmonicGrammar.weightNoiseChoiceProb {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) (a : C) : ENNReal

weightNoiseChoiceProb con w v a is the probability that a has the highest harmony when the weights w are perturbed by weight noise of variance v.

Equations

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

theorem HarmonicGrammar.measurable_harmonyScore_add {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (c : C) : Measurable fun (η : ι → ℝ) => harmonyScore con (w + η) c

theorem HarmonicGrammar.measurable_harmonyScore_add_sub {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (a b : C) : Measurable fun (η : ι → ℝ) => harmonyScore con (w + η) a - harmonyScore con (w + η) b

theorem HarmonicGrammar.dotProduct_violationDiff_self_nonneg {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (a b : C) : 0 ≤ con.violationDiff a b ⬝ᵥ con.violationDiff a b

theorem HarmonicGrammar.weightNoiseChoiceProb_eq_choiceProb_map {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) [Fintype C] (a : C) : weightNoiseChoiceProb con w v a = ProbabilityTheory.choiceProb (MeasureTheory.Measure.map (fun (η : ι → ℝ) (c : C) => harmonyScore con (w + η) c) (weightNoise ι v)) a

Noisy harmonic grammar is the random utility model whose utilities are the noisy harmonies.

theorem HarmonicGrammar.harmonyScore_add_sub {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w η : ι → ℝ) (a b : C) : harmonyScore con (w + η) a - harmonyScore con (w + η) b = harmonyScore con w a - harmonyScore con w b + ∑ i : ι, -con.violationDiff a b i * η i

Noise on the weights moves the harmony difference of two candidates by the noise against their violation difference.

theorem HarmonicGrammar.map_weightNoise_harmonyScore_sub {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) (a b : C) : MeasureTheory.Measure.map (fun (η : ι → ℝ) => harmonyScore con (w + η) a - harmonyScore con (w + η) b) (weightNoise ι v) = ProbabilityTheory.gaussianReal (harmonyScore con w a - harmonyScore con w b) (v * (con.violationDiff a b ⬝ᵥ con.violationDiff a b).toNNReal)

Under weight noise the harmony difference of two candidates is Gaussian, with mean their harmony difference and variance v times the squared length of their violation difference.

theorem HarmonicGrammar.variance_harmonyScore_sub {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) (a b : C) : ProbabilityTheory.variance (fun (η : ι → ℝ) => harmonyScore con (w + η) a - harmonyScore con (w + η) b) (weightNoise ι v) = ↑v * con.violationDiff a b ⬝ᵥ con.violationDiff a b

The variance of the harmony difference of two candidates is v times the squared length of their violation difference.

theorem HarmonicGrammar.covariance_harmonyScore_sub {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) (a b c : C) : ProbabilityTheory.covariance (fun (η : ι → ℝ) => harmonyScore con (w + η) b - harmonyScore con (w + η) a) (fun (η : ι → ℝ) => harmonyScore con (w + η) c - harmonyScore con (w + η) a) (weightNoise ι v) = ↑v * con.violationDiff b a ⬝ᵥ con.violationDiff c a

The covariance of the harmony differences of b and of c from a common candidate a is v times the dot product of their violation differences, so the joint law of the differences depends on the whole violation profile and not only on the harmonies.

theorem HarmonicGrammar.weightNoise_setOf_harmonyScore_lt {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) (hv : v ≠ 0) {a b : C} (hab : con.violationDiff a b ≠ 0) : (weightNoise ι v) {η : ι → ℝ | harmonyScore con (w + η) b < harmonyScore con (w + η) a} = ENNReal.ofReal (ProbabilityTheory.normalCDF ((harmonyScore con w a - harmonyScore con w b) / √(↑v * con.violationDiff a b ⬝ᵥ con.violationDiff a b)))

The probability that a has a higher noisy harmony than b is the probit of their harmony difference over its standard deviation.

theorem HarmonicGrammar.weightNoiseChoiceProb_of_forall_ne_eq {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → ℝ) (v : NNReal) (hv : v ≠ 0) {a b : C} (hb : ∀ (c : C), c ≠ a → c = b) (hab : a ≠ b) (hd : con.violationDiff a b ≠ 0) : weightNoiseChoiceProb con w v a = ENNReal.ofReal (ProbabilityTheory.normalCDF ((harmonyScore con w a - harmonyScore con w b) / √(↑v * con.violationDiff a b ⬝ᵥ con.violationDiff a b)))

When b is the only other candidate, the probability that a wins is the probit of their harmony difference over its standard deviation.

theorem HarmonicGrammar.weightNoiseChoiceProb_fin_two {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet (Fin 2) ι) (w : ι → ℝ) (v : NNReal) (hv : v ≠ 0) (hd : con.violationDiff 0 1 ≠ 0) : weightNoiseChoiceProb con w v 0 = ENNReal.ofReal (ProbabilityTheory.normalCDF ((harmonyScore con w 0 - harmonyScore con w 1) / √(↑v * con.violationDiff 0 1 ⬝ᵥ con.violationDiff 0 1)))

With two candidates, the probability that the first wins is the probit of their harmony difference over its standard deviation.