Constraints

A constraint is a violation-counting function C → ℕ ([PS93]). There is no stored "name" and no stored faithfulness/markedness tag: a constraint is its evaluation function.

The faithfulness/markedness distinction is a structural property, derived — not stipulated — over a correspondence carrier (OptimalityTheory.Correspondence): markedness factors through the output; faithfulness vanishes on the identity candidate. A bare C → ℕ over an opaque candidate type has no family, by design.

Main definitions

• Constraint C — a violation-counting function C → ℕ.
• Constraint.binary — the indicator constraint of a decidable predicate.
• Constraint.comap — pull a constraint back along a candidate map.
• CON C n — a grammar's constraint set: an indexed family of n constraints.
• weightedViolations / harmonyScore — the Harmonic-Grammar weighted sum Σⱼ wⱼ · Cⱼ(c) and its negation H(c) = -Σⱼ wⱼ · Cⱼ(c) ([SL06]).

@[reducible, inline]

abbrev Constraints.Constraint (C : Type u_1) : Type u_1

An OT / Harmonic-Grammar constraint: a violation-counting function on candidates ([PS93]). The faithfulness/markedness family is a structural property (see OptimalityTheory.Correspondence), not a stored tag; a constraint over an opaque candidate type has no family.

Equations

• Constraints.Constraint C = (C → ℕ)

def Constraints.Constraint.binary {C : Type u_1} (P : C → Prop) [DecidablePred P] : Constraint C

The binary constraint of a decidable predicate: 1 when P c, else 0. The shared shape of every binary markedness/faithfulness constraint — the faith/mark reading is recovered structurally, not from the constructor.

Equations

• Constraints.Constraint.binary P c = if P c then 1 else 0

@[simp]

theorem Constraints.Constraint.binary_apply {C : Type u_1} (P : C → Prop) [DecidablePred P] (c : C) : binary P c = if P c then 1 else 0

theorem Constraints.Constraint.binary_le_one {C : Type u_1} (P : C → Prop) [DecidablePred P] (c : C) : binary P c ≤ 1

A binary constraint never assigns more than one violation.

def Constraints.Constraint.comap {C : Type u_1} {D : Type u_2} (f : C → D) (con : Constraint D) : Constraint C

Pull a constraint back along f : C → D: evaluate the D-constraint on the image. Lets a specific carrier reuse a constraint defined on a more general one.

Equations

• Constraints.Constraint.comap f con = con ∘ f

@[simp]

theorem Constraints.Constraint.comap_apply {C : Type u_1} {D : Type u_2} (f : C → D) (con : Constraint D) (c : C) : comap f con c = con (f c)

@[reducible, inline]

abbrev Constraints.CON (C : Type u_3) (n : ℕ) : Type u_3

A grammar's constraint set CON: an indexed family of n constraints over candidates C ([PS93]'s CON). A CON sends each candidate to a ViolationProfile n (buildViolationProfile, in Constraints.Profile); an OT grammar then ranks the coordinates (a Ranking n), a Harmonic Grammar weights them (a Fin n → ℝ vector). Both feed the framework-neutral Core.Optimization.ConstraintSystem through different decoders (lexicographic argmin vs. softmax).

Equations

• Constraints.CON C n = (Fin n → Constraints.Constraint C)

Harmony (Harmonic Grammar)

A Harmonic Grammar weights each constraint in CON by a real number; the harmony of a candidate is the negated weighted sum of its violations, H(c) = -Σⱼ wⱼ · Cⱼ(c) ([SL06]) — a real linear functional of the candidate's raw violation vector. The weight vector w : Fin n → ℝ is the grammar's parameter (the HG twin of an OT Ranking n); both act on one CON.

def Constraints.weightedViolations {n : ℕ} (w : Fin n → ℝ) (v : Fin n → ℕ) : ℝ

The weighted violation sum Σⱼ wⱼ · Cⱼ(c) of a raw violation vector under weight vector w: a real linear functional of the counts. The positive part of harmony (harmonyScore = -weightedViolations …); weight-monotonicity and the HG→OT exponential-separation results are stated on this.

Equations

• Constraints.weightedViolations w v = ∑ j : Fin n, w j * ↑(v j)

def Constraints.harmonyScore {C : Type u_1} {n : ℕ} (con : CON C n) (w : Fin n → ℝ) (c : C) : ℝ

Harmony H(c) = -Σⱼ wⱼ · Cⱼ(c) ([SL06]): the negated weighted sum of a candidate's violations under the grammar's weight vector w; higher is more grammatical. The HG reading of a constraint set con weighted by w — the twin of ranking con in OT.

Equations

• Constraints.harmonyScore con w c = -Constraints.weightedViolations w fun (j : Fin n) => con j c

theorem Constraints.harmonyScore_eq_neg_sum {C : Type u_1} {n : ℕ} (con : CON C n) (w : Fin n → ℝ) (c : C) : harmonyScore con w c = -∑ j : Fin n, w j * ↑(con j c)

harmonyScore as a negated Finset.sum (unfolding lemma for rewriting).

def Constraints.harmonyDominates {C : Type u_1} {n : ℕ} (con : CON C n) (w : Fin n → ℝ) : C → C → Prop

a outranks b in harmony: H(a) > H(b), the pullback of > along harmonyScore con w (Order.Preimage); inherits IsStrictOrder from ℝ's >.

Equations

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

@[simp]

theorem Constraints.harmonyDominates_iff {C : Type u_1} {n : ℕ} (con : CON C n) (w : Fin n → ℝ) (a b : C) : harmonyDominates con w a b ↔ harmonyScore con w b < harmonyScore con w a