Riggle (2009): Violation semirings in Optimality Theory

This file formalizes the paper's algebraic characterization of constraint violation. A violation profile is a multiset over the constraint set, merge is multiset union, and harmonic inequality under a ranking is the lexicographic order of the ranking's reading of the profiles, HarmonicLT. The minimum under harmonic inequality and merge make the violation semiring V, a tropical semiring over profiles with an infinitely bad profile as the additive identity, whose commutative semiring structure is inherited from mathlib's MinTropical. The semiring is idempotent and monotone, le_mul: merging can only make a profile worse, which is the principle behind shortest-path optimization that every piece of an optimal mapping is itself optimal, Optimal.left_of_add. Merge commutes with every ranking's reading, smul_add, so the merged violations of a constraint set are one object for all rankings and a ranking enters only through the minimum. A Harmonic Grammar weighting is a homomorphism of the merge monoids into the tropical semiring of costs, tropWeight.

Implementation notes

Profiles are ViolationProfile n, whose lexicographic order is harmonic inequality under the identity ranking; a ranking reads a profile through the action of OptimalityTheory.Ranking, as the tableau substrate does. The weighted same-length transducers of the paper's sections 3 and 4, their intersection, and the complexity bound of the H-Opt algorithm are not formalized.

References

• J. Riggle, Violation Semirings in Optimality Theory (2009)
• E. W. Dijkstra, A note on two problems in connexion with graphs (1959)
• A. Prince, P. Smolensky, Optimality Theory: constraint interaction in generative grammar (1993)
• P. Smolensky, G. Legendre, The harmonic mind: from neural computation to Optimality-Theoretic grammar (2006)

Harmonic inequality and merge

def Riggle2009b.HarmonicLT {n : ℕ} (r : OptimalityTheory.Ranking (Fin n) n) (A B : OptimalityTheory.ViolationProfile n) : Prop

Harmonic inequality (Definition 1) under a ranking: the ranking's reading of A is lexicographically below that of B, so A has fewer violations of the highest-ranked constraint on which the two differ.

Equations

• Riggle2009b.HarmonicLT r A B = (r • A < r • B)

theorem Riggle2009b.smul_add {n : ℕ} (r : OptimalityTheory.Ranking (Fin n) n) (A B : OptimalityTheory.ViolationProfile n) : r • (A + B) = r • A + r • B

Merge is ranking-independent (section 3): a ranking reads a merged profile as the merge of its readings, so one merged constraint set serves every ranking.

theorem Riggle2009b.HarmonicLT.add_right {n : ℕ} {r : OptimalityTheory.Ranking (Fin n) n} {A B : OptimalityTheory.ViolationProfile n} (h : HarmonicLT r A B) (C : OptimalityTheory.ViolationProfile n) : HarmonicLT r (A + C) (B + C)

Merging the same profile on both sides preserves harmonic inequality.

def Riggle2009b.Optimal {n : ℕ} (r : OptimalityTheory.Ranking (Fin n) n) (S : Set (OptimalityTheory.ViolationProfile n)) (A : OptimalityTheory.ViolationProfile n) : Prop

A profile is optimal in a set under a ranking when it belongs to the set and no member is more harmonic.

Equations

• Riggle2009b.Optimal r S A = (A ∈ S ∧ ∀ B ∈ S, ¬Riggle2009b.HarmonicLT r B A)

theorem Riggle2009b.Optimal.left_of_add {n : ℕ} {r : OptimalityTheory.Ranking (Fin n) n} {S T : Set (OptimalityTheory.ViolationProfile n)} {A B : OptimalityTheory.ViolationProfile n} (h : Optimal r (S + T) (A + B)) (hA : A ∈ S) (hB : B ∈ T) : Optimal r S A

Dijkstra's principle for harmonic optimization (section 2): a merge that is optimal among the merges of two sets has an optimal first part, so every piece of an optimal mapping is itself an optimal mapping.

theorem Riggle2009b.Optimal.right_of_add {n : ℕ} {r : OptimalityTheory.Ranking (Fin n) n} {S T : Set (OptimalityTheory.ViolationProfile n)} {A B : OptimalityTheory.ViolationProfile n} (h : Optimal r (S + T) (A + B)) (hA : A ∈ S) (hB : B ∈ T) : Optimal r T B

The violation semiring

@[reducible, inline]

abbrev Riggle2009b.V (n : ℕ) : Type

The violation semiring (Example 2): profiles under the identity ranking together with the infinitely bad profile ⊤; tropical addition is the minimum under harmonic inequality, tropical multiplication is merge, and the commutative semiring structure is mathlib's.

Equations

• Riggle2009b.V n = MinTropical (WithTop (OptimalityTheory.ViolationProfile n))

theorem Riggle2009b.le_mul {n : ℕ} (a b : V n) : a ≤ a * b

Monotonicity (section 2): merging can only make a profile worse, so the semiring is monotone in the sense that makes shortest-path optimization sound.

theorem Riggle2009b.add_mul_self {n : ℕ} (a b : V n) : a + a * b = a

In semiring terms, the minimum of a profile and any merge extending it is the profile.

Harmonic Grammar

def Riggle2009b.weightMap {n : ℕ} (w : Fin n → ℝ) : OptimalityTheory.ViolationProfile n →+ ℝ

A weighting read as a homomorphism from the merge monoid of profiles to the additive reals: the weighted violation sum.

Equations

• Riggle2009b.weightMap w = { toFun := fun (v : OptimalityTheory.ViolationProfile n) => w ⬝ᵥ Nat.cast ∘ ofLex v, map_zero' := ⋯, map_add' := ⋯ }

def Riggle2009b.tropWeight {n : ℕ} (w : Fin n → ℝ) : V n →* MinTropical (WithTop ℝ)

The weighting maps the violation semiring to the tropical semiring of costs (section 2), preserving tropical multiplication and the identities; whether it also preserves the minimum is the question of Harmonic Grammar's agreement with Optimality Theory, which the paper does not raise.

Equations

• Riggle2009b.tropWeight w = { toFun := fun (a : Riggle2009b.V n) => MinTropical.trop (WithTop.map (⇑(Riggle2009b.weightMap w)) (MinTropical.untrop a)), map_one' := ⋯, map_mul' := ⋯ }

theorem Riggle2009b.tropWeight_zero {n : ℕ} (w : Fin n → ℝ) : (tropWeight w) 0 = 0