Constraints

This file defines the violable constraints of Optimality Theory ([prince-smolensky-1993]), which Harmonic Grammar, MaxEnt and optimality-theoretic work in syntax and semantics adopt. A constraint is a function C → ℕ that counts the violations of each candidate. It stores no name and no faithfulness or markedness tag, since a constraint is its evaluation function. The faithfulness–markedness distinction is a structural property of correspondence candidates (OptimalityTheory.Correspondence), where markedness factors through the output and faithfulness vanishes on the identity candidate, and a constraint over an opaque candidate type has no family.

Main definitions

• OptimalityTheory.Constraint C: a violation-counting function C → ℕ.
• Constraint.binary: the indicator constraint of a decidable predicate.
• Constraint.comap, ConstraintSet.comap: the pullback of a constraint or constraint set along a candidate map.
• ConstraintSet C ι: a grammar's constraint set, CON, a family of constraints indexed by ι.
• Constraint.joint, ConstraintSet.joint: joint evaluation on output tuples by constraint summation.

The Harmonic Grammar scores of a constraint set are in HarmonicGrammar/Harmony.lean.

References

• [A. Prince and P. Smolensky, Optimality Theory: Constraint Interaction in Generative Grammar (1993)][prince-smolensky-1993]
• [J. D. Alderete, Dominance Effects as Trans-derivational Anti-faithfulness (2001)][alderete-2001]
• [A. Prince, One Tableau Suffices (2015)][prince-2015]
• [G. Magri and B. Storme, Constraint Summation in Phonological Theory (2021)][magri-storme-2021]

@[reducible, inline]

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

An OT or Harmonic-Grammar constraint is a function counting the violations of each candidate. Whether it is a faithfulness or a markedness constraint is a structural property (see OptimalityTheory.Correspondence), not a stored tag.

Equations

• OptimalityTheory.Constraint C = (C → ℕ)

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

The binary constraint of a decidable predicate P assigns one violation when P c holds and none otherwise. Every binary markedness or faithfulness constraint has this shape, and which of the two it is follows from its structure, not from the constructor.

Equations

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

@[simp]

theorem OptimalityTheory.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 OptimalityTheory.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.

theorem OptimalityTheory.Constraint.binary_eq_zero_iff {C : Type u_1} (P : C → Prop) [DecidablePred P] (c : C) : binary P c = 0 ↔ ¬P c

A binary constraint is satisfied exactly when its predicate fails.

theorem OptimalityTheory.Constraint.binary_eq_one_iff {C : Type u_1} (P : C → Prop) [DecidablePred P] (c : C) : binary P c = 1 ↔ P c

A binary constraint is violated exactly when its predicate holds.

def OptimalityTheory.Constraint.antifaithful {C : Type u_1} (F : Constraint C) : Constraint C

The anti-faithfulness constraint ¬F of a constraint F ([alderete-2001]) is satisfied exactly when F is violated at least once, so it demands one violation and no more.

Equations

• F.antifaithful = OptimalityTheory.Constraint.binary fun (x : C) => F x = 0

theorem OptimalityTheory.Constraint.antifaithful_eq_zero_iff {C : Type u_1} (F : Constraint C) (c : C) : F.antifaithful c = 0 ↔ 0 < F c

theorem OptimalityTheory.Constraint.antifaithful_eq_one_iff {C : Type u_1} (F : Constraint C) (c : C) : F.antifaithful c = 1 ↔ F c = 0

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

The pullback of a D-constraint along f : C → D evaluates it on the image of each candidate, so a specific candidate type can reuse a constraint defined on a more general one.

Equations

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

@[simp]

theorem OptimalityTheory.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)

Joint evaluation

A systemic constraint — *HOMOPHONY, a distinctiveness constraint — scores a whole system of outputs, so its candidate is an output tuple f : κ → O assigning each input inputs i its output. A per-mapping constraint on I × O is lifted to output tuples by constraint summation ([prince-2015], [magri-storme-2021]), which sums its violations on f over the mappings (inputs i, f i).

def OptimalityTheory.Constraint.joint {κ : Type u_3} {I : Type u_4} {O : Type u_5} [Fintype κ] (inputs : κ → I) (con : Constraint (I × O)) : Constraint (κ → O)

The joint evaluation of a per-mapping constraint on an output tuple sums its violations over the mappings (inputs i, f i).

Equations

• OptimalityTheory.Constraint.joint inputs con f = ∑ i : κ, con (inputs i, f i)

@[simp]

theorem OptimalityTheory.Constraint.joint_apply {κ : Type u_3} {I : Type u_4} {O : Type u_5} [Fintype κ] (inputs : κ → I) (con : Constraint (I × O)) (f : κ → O) : joint inputs con f = ∑ i : κ, con (inputs i, f i)

@[reducible, inline]

abbrev OptimalityTheory.ConstraintSet (C : Type u_6) (ι : Type u_7) : Type (max u_7 u_6)

A grammar's constraint set, CON in [prince-smolensky-1993], is a family of constraints over candidates C indexed by the constraint names ι. An OT grammar ranks it (a Ranking ι n), a Harmonic Grammar weights its violations by a vector ι → ℝ, and MaxEnt takes the softmax of the resulting harmonies. A constraint set written as a vector ![C₀, …] is indexed by Fin n.

Equations

• OptimalityTheory.ConstraintSet C ι = (ι → OptimalityTheory.Constraint C)

def OptimalityTheory.ConstraintSet.comap {C : Type u_1} {D : Type u_2} {ι : Type u_6} (f : C → D) (con : ConstraintSet D ι) : ConstraintSet C ι

The pullback of a constraint set along a candidate map pulls back each constraint.

Equations

• OptimalityTheory.ConstraintSet.comap f con i = OptimalityTheory.Constraint.comap f (con i)

@[simp]

theorem OptimalityTheory.ConstraintSet.comap_apply {C : Type u_1} {D : Type u_2} {ι : Type u_6} (f : C → D) (con : ConstraintSet D ι) (i : ι) (c : C) : comap f con i c = con i (f c)

def OptimalityTheory.ConstraintSet.joint {κ : Type u_3} {I : Type u_4} {O : Type u_5} [Fintype κ] {ι : Type u_6} (inputs : κ → I) (con : ConstraintSet (I × O) ι) : ConstraintSet (κ → O) ι

The joint evaluation of a constraint set evaluates each constraint jointly.

Equations

• OptimalityTheory.ConstraintSet.joint inputs con j = OptimalityTheory.Constraint.joint inputs (con j)

@[simp]

theorem OptimalityTheory.ConstraintSet.joint_apply {κ : Type u_3} {I : Type u_4} {O : Type u_5} [Fintype κ] {ι : Type u_6} (inputs : κ → I) (con : ConstraintSet (I × O) ι) (j : ι) : joint inputs con j = Constraint.joint inputs (con j)