Shared Phonological Constraint Library

@cite{prince-smolensky-1993} @cite{mccarthy-prince-1995}

Reusable constraint constructors for Optimality Theory and Harmonic Grammar. Every phonological study in linglib defines constraints as NamedConstraint C or WeightedConstraint C instances. Many constraint families recur across studies with different candidate types:

• MAX: penalizes deletion (segment/feature not in output)
• DEP: penalizes epenthesis (segment/feature in output but not input)
• IDENT: penalizes featural unfaithfulness
• *STRUC: penalizes structural complexity (markedness)

This module provides generic constructors so that study files can write:

def myMax := mkMax "MAX-V" (fun c => c.deleted)

rather than manually assembling the NamedConstraint record each time. The constructors enforce the correct ConstraintFamily classification.

Contextual faithfulness

Following @cite{coetzee-pater-2011}, contextual faithfulness constraints (e.g. MAX-PRE-V, MAX-FINAL) are standard MAX/DEP constraints with an additional context predicate. mkMaxCtx and mkDepCtx take a context guard: the constraint is violated only when the context guard is true.

Violation counting

All constructors support both binary (0/1) and gradient (Nat) violations. Binary constraints use a Bool predicate; gradient constraints use a Nat-valued evaluation function directly.

def Theories.Phonology.Constraints.mkMax {C : Type} (name : String) (violated : C → Bool) : Core.OT.NamedConstraint C

Build a MAX constraint (penalizes deletion). violated c returns true when candidate c exhibits deletion.

Equations

• Theories.Phonology.Constraints.mkMax name violated = { name := name, family := Core.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if violated c = true then 1 else 0 }

def Theories.Phonology.Constraints.mkMaxCtx {C : Type} (name : String) (deleted context : C → Bool) : Core.OT.NamedConstraint C

Build a contextual MAX constraint. Violated only when both deletion occurs AND the context holds. Models positional faithfulness (@cite{coetzee-pater-2011} §3.2).

Equations

• One or more equations did not get rendered due to their size.

def Theories.Phonology.Constraints.mkDep {C : Type} (name : String) (violated : C → Bool) : Core.OT.NamedConstraint C

Build a DEP constraint (penalizes epenthesis). violated c returns true when candidate c exhibits insertion.

Equations

• Theories.Phonology.Constraints.mkDep name violated = { name := name, family := Core.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if violated c = true then 1 else 0 }

def Theories.Phonology.Constraints.mkIdent {C : Type} (name : String) (violated : C → Bool) : Core.OT.NamedConstraint C

Build an IDENT constraint (penalizes featural change). violated c returns true when the feature value has changed.

Equations

• Theories.Phonology.Constraints.mkIdent name violated = { name := name, family := Core.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if violated c = true then 1 else 0 }

def Theories.Phonology.Constraints.mkMark {C : Type} (name : String) (violated : C → Bool) : Core.OT.NamedConstraint C

Build a binary markedness constraint. violated c returns true when the marked structure is present.

Equations

• Theories.Phonology.Constraints.mkMark name violated = { name := name, family := Core.OT.ConstraintFamily.markedness, eval := fun (c : C) => if violated c = true then 1 else 0 }

def Theories.Phonology.Constraints.mkMarkGrad {C : Type} (name : String) (violations : C → ℕ) : Core.OT.NamedConstraint C

Build a gradient markedness constraint with a Nat-valued violation count. violations c returns the number of violations for candidate c.

Equations

• Theories.Phonology.Constraints.mkMarkGrad name violations = { name := name, family := Core.OT.ConstraintFamily.markedness, eval := violations }

theorem Theories.Phonology.Constraints.mkMax_is_faithfulness {C : Type} (name : String) (p : C → Bool) : (mkMax name p).family = Core.OT.ConstraintFamily.faithfulness

MAX constraints are faithfulness constraints.

theorem Theories.Phonology.Constraints.mkDep_is_faithfulness {C : Type} (name : String) (p : C → Bool) : (mkDep name p).family = Core.OT.ConstraintFamily.faithfulness

DEP constraints are faithfulness constraints.

theorem Theories.Phonology.Constraints.mkMark_is_markedness {C : Type} (name : String) (p : C → Bool) : (mkMark name p).family = Core.OT.ConstraintFamily.markedness

Markedness constraints are markedness constraints.

theorem Theories.Phonology.Constraints.mkMaxCtx_is_faithfulness {C : Type} (name : String) (d ctx : C → Bool) : (mkMaxCtx name d ctx).family = Core.OT.ConstraintFamily.faithfulness

Contextual MAX constraints are faithfulness constraints.

theorem Theories.Phonology.Constraints.mkMax_bounded {C : Type} (name : String) (p : C → Bool) (c : C) : (mkMax name p).eval c ≤ 1

Binary constraints have violations bounded by 1.

theorem Theories.Phonology.Constraints.mkMark_bounded {C : Type} (name : String) (p : C → Bool) (c : C) : (mkMark name p).eval c ≤ 1

Binary markedness constraints have violations bounded by 1.

theorem Theories.Phonology.Constraints.mkMaxCtx_bounded {C : Type} (name : String) (d ctx : C → Bool) (c : C) : (mkMaxCtx name d ctx).eval c ≤ 1

Contextual MAX constraints have violations bounded by 1.

def Theories.Phonology.Constraints.mkMaxW {C : Type} (name : String) (violated : C → Bool) (w : ℚ) : HarmonicGrammar.WeightedConstraint C

Build a weighted MAX constraint with a given weight.

Equations

• Theories.Phonology.Constraints.mkMaxW name violated w = { toNamedConstraint := Theories.Phonology.Constraints.mkMax name violated, weight := w }

def Theories.Phonology.Constraints.mkMaxCtxW {C : Type} (name : String) (deleted context : C → Bool) (w : ℚ) : HarmonicGrammar.WeightedConstraint C

Build a weighted contextual MAX constraint.

Equations

• Theories.Phonology.Constraints.mkMaxCtxW name deleted context w = { toNamedConstraint := Theories.Phonology.Constraints.mkMaxCtx name deleted context, weight := w }

def Theories.Phonology.Constraints.mkDepW {C : Type} (name : String) (violated : C → Bool) (w : ℚ) : HarmonicGrammar.WeightedConstraint C

Build a weighted DEP constraint.

Equations

• Theories.Phonology.Constraints.mkDepW name violated w = { toNamedConstraint := Theories.Phonology.Constraints.mkDep name violated, weight := w }

def Theories.Phonology.Constraints.mkIdentW {C : Type} (name : String) (violated : C → Bool) (w : ℚ) : HarmonicGrammar.WeightedConstraint C

Build a weighted IDENT constraint.

Equations

• Theories.Phonology.Constraints.mkIdentW name violated w = { toNamedConstraint := Theories.Phonology.Constraints.mkIdent name violated, weight := w }

def Theories.Phonology.Constraints.mkMarkW {C : Type} (name : String) (violated : C → Bool) (w : ℚ) : HarmonicGrammar.WeightedConstraint C

Build a weighted binary markedness constraint.

Equations

• Theories.Phonology.Constraints.mkMarkW name violated w = { toNamedConstraint := Theories.Phonology.Constraints.mkMark name violated, weight := w }

def Theories.Phonology.Constraints.mkMarkGradW {C : Type} (name : String) (violations : C → ℕ) (w : ℚ) : HarmonicGrammar.WeightedConstraint C

Build a weighted gradient markedness constraint.

Equations

• Theories.Phonology.Constraints.mkMarkGradW name violations w = { toNamedConstraint := Theories.Phonology.Constraints.mkMarkGrad name violations, weight := w }