Violation Profiles

OT-tradition names for the neutral violation primitives in Core.Optimization.Evaluation, shared by Optimality Theory (lexicographic comparison) and Harmonic Grammar (weighted aggregation, [riggle-2009]).

Main definitions

• ViolationProfile n — Lex (Fin n → Nat), a fixed-length violation vector.
• buildViolationProfile — assemble a profile from a constraint vector.

Main results

• ViolationProfile.zero_le — the zero profile is the bottom element.
• ViolationProfile.le_apply_zero — first-component extraction from ≤.

@[reducible, inline]

abbrev Constraints.ViolationProfile (n : ℕ) : Type

OT-named alias for Lex (Fin n → Nat) — fixed-length violation profile.

Equations

• Constraints.ViolationProfile n = Lex (Fin n → ℕ)

@[reducible, inline]

abbrev Constraints.buildViolationProfile {C : Type u_1} {n : ℕ} (con : CON C n) (c : C) : ViolationProfile n

OT-named alias for lexFinNatOf — assemble a profile from a constraint set CON C n.

Equations

• Constraints.buildViolationProfile con c = Core.Optimization.Evaluation.lexFinNatOf con c

@[simp]

theorem Constraints.buildViolationProfile_apply {C : Type u_1} {n : ℕ} (con : CON C n) (c : C) (i : Fin n) : buildViolationProfile con c i = con i c

theorem Constraints.ViolationProfile.zero_le {n : ℕ} (p : ViolationProfile n) : 0 ≤ p

The zero profile is the bottom element: 0 ≤ p for every profile p, so a candidate with no violations wins under any ranking.

theorem Constraints.ViolationProfile.le_apply_zero {n : ℕ} {a b : ViolationProfile (n + 1)} (h : a ≤ b) : a 0 ≤ b 0

OT-named alias for lexFinNat_le_apply_zero — first-component extraction from a lexicographic ≤.