Harmony

A Harmonic Grammar, in Smolensky and Legendre's formulation, weights each constraint of a constraint set by a number, real in the usual statement, and the harmony of a candidate is the negated weighted sum of its violations, H(c) = -(w ⬝ᵥ C(c)), a linear functional of the candidate's violation vector. The weight vector w : ι → R is the grammar's parameter, the Harmonic-Grammar twin of an OT ranking, and both act on one ConstraintSet C ι. The weight ring is a parameter so that a grammar with rational or integer weights keeps its scores exactly computable. Violations need not be counts: harmony T w is the harmony of violation vectors T c with entries in the weight ring, such as violations scaled by the activation of a lexical item.

Harmony is additive over concatenated and jointly evaluated constraint sets, so constraint summation is innocuous for it, and with non-negative weights a candidate that incurs no more violations than another on every constraint has at least its harmony, which is harmonic bounding.

Main definitions

• harmonyScore: the harmony H(c) = -(w ⬝ᵥ C(c)) of a candidate.
• OptimalityTheory.ConstraintSet.violations, harmony: the violation vector C(c) of a candidate, and the harmony of a real-valued violation vector, of which harmonyScore is the case of counted violations.
• OptimalityTheory.ConstraintSet.violationDiff: the violation difference C(a) - C(b).
• harmonyDominates: harmonic dominance, H(a) > H(b).

Main results

• harmonyScore_cons: @[simp] cons-recursion evaluating harmony on literal grammars ![C₀, …], ![w₀, …].
• harmonyScore_sub: the harmony difference is -(w ⬝ᵥ (C(a) - C(b))).
• harmonyScore_congr: harmony depends only on the violation vector.
• harmonyScore_append, harmonyScore_joint: harmony is additive over a concatenated constraint set and, for a jointly evaluated one, over the mappings.
• harmonyScore_le_of_forall_le, harmonyDominates_of_lt: a Pareto-dominant candidate has at least, and given a strict advantage on a positively weighted constraint strictly greater, harmony.

References

• P. Smolensky and G. Legendre, The Harmonic Mind: From Neural Computation to Optimality-Theoretic Grammar (2006)
• A. Prince and P. Smolensky, Optimality Theory: Constraint Interaction in Generative Grammar (1993)
• G. Magri and B. Storme, Constraint Summation in Phonological Theory (2021)

def OptimalityTheory.ConstraintSet.violations {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Ring R] (con : ConstraintSet C ι) (c : C) : ι → R

The violation vector C(c) of a candidate, its violations of each constraint, a row of a tableau.

Equations

• con.violations c j = ↑(con j c)

@[simp]

theorem OptimalityTheory.ConstraintSet.violations_apply {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Ring R] (con : ConstraintSet C ι) (c : C) (j : ι) : con.violations c j = ↑(con j c)

Harmony

def HarmonicGrammar.harmonyScore {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → R) (c : C) : R

The harmony H(c) = -(w ⬝ᵥ C(c)) of a candidate ([SL06]) is the negated weighted sum of its violations under the weight vector w, and higher harmony is more grammatical.

Equations

• HarmonicGrammar.harmonyScore con w c = -(w ⬝ᵥ fun (j : ι) => ↑(con j c))

theorem HarmonicGrammar.harmonyScore_eq_neg_sum {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → R) (c : C) : harmonyScore con w c = -∑ j : ι, w j * ↑(con j c)

harmonyScore is a negated Finset.sum.

def HarmonicGrammar.harmony {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] (T : C → ι → R) (w : ι → R) (c : C) : R

The harmony -(w ⬝ᵥ T c) of a candidate whose violations T c may be any elements of the weight ring, as when a lexicon scales the violations of faithfulness constraints.

Equations

• HarmonicGrammar.harmony T w c = -(w ⬝ᵥ T c)

@[simp]

theorem HarmonicGrammar.harmony_violations {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → R) : harmony con.violations w = harmonyScore con w

theorem HarmonicGrammar.harmony_add {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] (T : C → ι → R) (w w' : ι → R) : harmony T (w + w') = harmony T w + harmony T w'

Harmony is linear in the weights.

theorem HarmonicGrammar.harmony_smul {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [CommRing R] (T : C → ι → R) (r : R) (w : ι → R) : harmony T (r • w) = r • harmony T w

theorem HarmonicGrammar.harmony_sum {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] {κ : Type u_4} {D : Type u_5} [Fintype κ] (T : κ → D → ι → R) (w : ι → R) (f : κ → D) : harmony (fun (f : κ → D) => ∑ k : κ, T k (f k)) w f = ∑ k : κ, harmony (T k) w (f k)

The harmony of a sum of violation vectors is the sum of their harmonies.

def OptimalityTheory.ConstraintSet.violationDiff {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Ring R] (con : ConstraintSet C ι) (a b : C) : ι → R

The violation difference C(a) - C(b) of two candidates, a row of a comparative tableau.

Equations

• con.violationDiff a b j = ↑(con j a) - ↑(con j b)

theorem HarmonicGrammar.harmonyScore_sub {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → R) (a b : C) : harmonyScore con w a - harmonyScore con w b = -(w ⬝ᵥ con.violationDiff a b)

The harmony difference of two candidates is the weight vector against their violation difference.

def HarmonicGrammar.harmonyDominates {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] [LT R] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → R) : C → C → Prop

The candidate a harmonically dominates b when H(a) > H(b). The relation is the pullback of > along harmonyScore con w (Order.Preimage), so it inherits IsStrictOrder from the weight ring.

Equations

• HarmonicGrammar.harmonyDominates con w = HarmonicGrammar.harmonyScore con w ⁻¹'o fun (x1 x2 : R) => x1 > x2

@[simp]

theorem HarmonicGrammar.harmonyDominates_iff {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] [LT R] (con : OptimalityTheory.ConstraintSet C ι) (w : ι → R) (a b : C) : harmonyDominates con w a b ↔ harmonyScore con w b < harmonyScore con w a

@[simp]

theorem HarmonicGrammar.harmonyScore_comap {C : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype ι] [Ring R] {D : Type u_4} (f : C → D) (con : OptimalityTheory.ConstraintSet D ι) (w : ι → R) (c : C) : harmonyScore (OptimalityTheory.ConstraintSet.comap f con) w c = harmonyScore con w (f c)

Evaluation by cons-recursion

@[simp]

theorem HarmonicGrammar.harmonyScore_nil {C : Type u_1} (con : OptimalityTheory.ConstraintSet C (Fin 0)) (w : Fin 0 → ℝ) (x : C) : harmonyScore con w x = 0

@[simp]

theorem HarmonicGrammar.harmonyScore_cons {C : Type u_1} {n : ℕ} (c₀ : OptimalityTheory.Constraint C) (con : OptimalityTheory.ConstraintSet C (Fin n)) (w₀ : ℝ) (w : Fin n → ℝ) (x : C) : harmonyScore (Matrix.vecCons c₀ con) (Matrix.vecCons w₀ w) x = -(w₀ * ↑(c₀ x)) + harmonyScore con w x

@[simp]

theorem HarmonicGrammar.harmonyScore_zero_weight {C : Type u_1} {ι : Type u_2} [Fintype ι] (con : OptimalityTheory.ConstraintSet C ι) (x : C) : harmonyScore con 0 x = 0

theorem HarmonicGrammar.harmonyScore_congr {C : Type u_1} {ι : Type u_2} [Fintype ι] {con : OptimalityTheory.ConstraintSet C ι} {w : ι → ℝ} {a b : C} (h : ∀ (j : ι), con j a = con j b) : harmonyScore con w a = harmonyScore con w b

Harmony depends only on the violation vector.

Concatenated and jointly evaluated constraint sets

theorem HarmonicGrammar.harmonyScore_append {C : Type u_1} {n m : ℕ} (c₁ : OptimalityTheory.ConstraintSet C (Fin n)) (c₂ : OptimalityTheory.ConstraintSet C (Fin m)) (w₁ : Fin n → ℝ) (w₂ : Fin m → ℝ) (x : C) : harmonyScore (Fin.append c₁ c₂) (Fin.append w₁ w₂) x = harmonyScore c₁ w₁ x + harmonyScore c₂ w₂ x

Harmony is additive over a concatenated constraint set and weight vector.

theorem HarmonicGrammar.harmonyScore_joint {ι : Type u_2} [Fintype ι] {κ : Type u_4} {I : Type u_5} {O : Type u_6} [Fintype κ] (inputs : κ → I) (con : OptimalityTheory.ConstraintSet (I × O) ι) (w : ι → ℝ) (f : κ → O) : harmonyScore (OptimalityTheory.ConstraintSet.joint inputs con) w f = ∑ i : κ, harmonyScore con w (inputs i, f i)

The harmony of a jointly evaluated constraint set is the sum of the mappings' harmonies — constraint summation is innocuous for harmony ([MS21]).

Harmonic bounding (Pareto dominance)

theorem HarmonicGrammar.harmonyScore_le_of_forall_le {C : Type u_1} {ι : Type u_2} [Fintype ι] {con : OptimalityTheory.ConstraintSet C ι} {w : ι → ℝ} {a b : C} (hw : 0 ≤ w) (h : ∀ (i : ι), con i a ≤ con i b) : harmonyScore con w b ≤ harmonyScore con w a

With non-negative weights, a candidate incurring no more violations than b on every constraint has at least b's harmony, which is harmonic bounding ([PS93]).

theorem HarmonicGrammar.harmonyDominates_of_lt {C : Type u_1} {ι : Type u_2} [Fintype ι] {con : OptimalityTheory.ConstraintSet C ι} {w : ι → ℝ} {a b : C} (hw : 0 ≤ w) (hle : ∀ (i : ι), con i a ≤ con i b) (hlt : ∃ (i : ι), 0 < w i ∧ con i a < con i b) : harmonyDominates con w a b

Strictly fewer violations on some positively weighted constraint give strictly greater harmony.