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)
• ALIGN: penalizes edge mismatches between morphological and prosodic constituents (@cite{mccarthy-prince-1993} Generalized Alignment, used by @cite{faust-2026} as *Misalignment)

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 Phonology.Constraints.mkMax {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build a MAX constraint (penalizes deletion).

P c holds (as a proposition) when candidate c exhibits deletion. Decidable for the constraint to be evaluable.

Equations

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

def Phonology.Constraints.mkMaxCtx {C : Type} (name : String) (Deleted : C → Prop) [DecidablePred Deleted] (Context : C → Prop) [DecidablePred Context] : Core.Constraint.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

• Phonology.Constraints.mkMaxCtx name Deleted Context = { name := name, family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if Deleted c ∧ Context c then 1 else 0 }

def Phonology.Constraints.mkDep {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build a DEP constraint (penalizes epenthesis). P c holds when candidate c exhibits insertion.

Equations

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

def Phonology.Constraints.mkIdent {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build an IDENT constraint (penalizes featural change). P c holds when the feature value has changed.

Equations

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

def Phonology.Constraints.mkAnchorLeft {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build a LEFT-ANCHOR constraint: the morpheme's tonal specification must be in correspondence with the left edge of the host. P c holds when the left anchor is not satisfied.

Following @cite{finley-2009}: morpheme-specific versions of @cite{mccarthy-prince-1995}'s ANCHOR constraints.

Equations

• Phonology.Constraints.mkAnchorLeft name P = { name := name, family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if P c then 1 else 0 }

def Phonology.Constraints.mkAnchorRight {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build a RIGHT-ANCHOR constraint: the morpheme's tonal specification must be in correspondence with the right edge of the host.

Equations

• Phonology.Constraints.mkAnchorRight name P = { name := name, family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if P c then 1 else 0 }

def Phonology.Constraints.mkIntegrity {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build an INTEGRITY constraint: the morpheme's tone must not have multiple correspondents in the output. Penalizes splitting of a single input tone across multiple output TBUs when the one-to-one mapping is violated.

Equations

• Phonology.Constraints.mkIntegrity name P = { name := name, family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if P c then 1 else 0 }

theorem Phonology.Constraints.mkAnchorLeft_is_faithfulness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkAnchorLeft name P).family = Core.Constraint.OT.ConstraintFamily.faithfulness

Anchor-left constraints are faithfulness constraints.

theorem Phonology.Constraints.mkAnchorRight_is_faithfulness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkAnchorRight name P).family = Core.Constraint.OT.ConstraintFamily.faithfulness

Anchor-right constraints are faithfulness constraints.

theorem Phonology.Constraints.mkIntegrity_is_faithfulness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkIntegrity name P).family = Core.Constraint.OT.ConstraintFamily.faithfulness

Integrity constraints are faithfulness constraints.

def Phonology.Constraints.mkForbidPairsOnTier {C α β : Type} (name : String) (R : β → β → Prop) [DecidableRel R] (T : Core.Tier α β) (extract : C → List α) : Core.Constraint.OT.NamedConstraint C

Build a markedness constraint penalizing tier-adjacent forbidden pairs. The candidate's raw symbol list is extracted by extract, the tier T projects it onto the relevant tier alphabet (an erasing string homomorphism — see Core.StringHom), and each tier-adjacent pair (a, b) with R a b contributes one violation.

Generic markedness constructor for adjacency-based phonological constraints over a single tier. OCP is the case R := (· = ·) (mkOCPOnTier below). The TSL_2 bridge Phonology.Subregular.mkForbidPairsOnTier_zero_iff_in_lang characterizes zero-violation candidates as members of the corresponding tier-based strictly 2-local language for any choice of R.

Equations

• Phonology.Constraints.mkForbidPairsOnTier name R T extract = Core.Constraint.OT.mkMarkGrad name fun (c : C) => Core.Computability.Subregular.countAdjacent R (T.apply (extract c))

def Phonology.Constraints.mkForbidSingletonOnTier {C α β : Type} (name : String) (P : β → Prop) [DecidablePred P] (T : Core.Tier α β) (extract : C → List α) : Core.Constraint.OT.NamedConstraint C

Build a markedness constraint penalizing tier elements satisfying P. The SL_1 sibling of mkForbidPairsOnTier: each tier symbol a with P a contributes one violation. *Coda — viewed as "no segment in coda position survives the syllable-coda tier" — is the canonical SL_1 instance and should use this constructor rather than be shoehorned into the forbidden-pair schema. The TSL_1 / SL_1 language-side bridge is not yet wired; the constructor exists to keep SL_1 phenomena from silently masquerading as TSL_2.

Equations

• Phonology.Constraints.mkForbidSingletonOnTier name P T extract = Core.Constraint.OT.mkMarkGrad name fun (c : C) => List.countP (fun (x : β) => decide (P x)) (T.apply (extract c))

def Phonology.Constraints.adjacentIdentical {α : Type} [DecidableEq α] : List α → ℕ

Count adjacent identical pairs in a list. Definitional alias for countAdjacent (· = ·) — kept under this name because OCP-style constraints read more naturally with the linguistic-domain term.

Equations

• Phonology.Constraints.adjacentIdentical = Core.Computability.Subregular.countAdjacent fun (x1 x2 : α) => x1 = x2

def Phonology.Constraints.mkOCP {C α : Type} [DecidableEq α] (name : String) (project : C → List α) : Core.Constraint.OT.NamedConstraint C

Build an OCP constraint: penalizes adjacent identical elements on a tier. project extracts the relevant tier from a candidate.

The OCP is parametrically polymorphic over the feature type α — it operates on identity vs. non-identity of adjacent elements, regardless of what kind of features they are. Following @cite{berent-2026}, this polymorphism captures the algebraic nature of phonological constraints: they generalize to novel feature values by construction.

Equations

• Phonology.Constraints.mkOCP name project = Core.Constraint.OT.mkMarkGrad name fun (c : C) => Phonology.Constraints.adjacentIdentical (project c)

def Phonology.Constraints.mkOCPOnTier {C α β : Type} [DecidableEq β] (name : String) (T : Core.Tier α β) (extract : C → List α) : Core.Constraint.OT.NamedConstraint C

Build an OCP constraint from a Core.Tier projection. The candidate's raw symbol list is extracted by extract, and the tier T projects that string onto the relevant tier alphabet (an erasing string homomorphism — see Core.StringHom).

This is the constraint-algebra adapter for the unified Tier interface: autosegmental tonal-tier OCP, sibilant-harmony OCP, and learned-tier OCP (à la @cite{belth-2026}) all factor through this constructor.

Defined as the R := (· = ·) specialization of mkForbidPairsOnTier, mirroring mkAgreeOnTier's R := (· ≠ ·) specialization. The two sit in the same constraint algebra and the equivalence is rfl.

@cite{goldsmith-1976} @cite{berent-2026}

Equations

• Phonology.Constraints.mkOCPOnTier name T extract = Phonology.Constraints.mkForbidPairsOnTier name (fun (x1 x2 : β) => x1 = x2) T extract

def Phonology.Constraints.mkAgreeOnTier {C α β : Type} [DecidableEq β] (name : String) (T : Core.Tier α β) (extract : C → List α) : Core.Constraint.OT.NamedConstraint C

Build an AGREE constraint from a Core.Tier projection: penalizes each tier-adjacent pair (a, b) with a ≠ b. The non-identity dual of mkOCPOnTier. AGREE-style markedness in OT phonology is the symmetric specialization of mkForbidPairsOnTier with R := (· ≠ ·), just as the OCP is the R := (· = ·) specialization. The two specializations sit in the same constraint algebra; their consumers (consonant harmony, vowel harmony, dissimilation, anti-OCP) use the same machinery up to the choice of R.

Equations

• Phonology.Constraints.mkAgreeOnTier name T extract = Phonology.Constraints.mkForbidPairsOnTier name (fun (x1 x2 : β) => x1 ≠ x2) T extract

def Phonology.Constraints.mkAlign {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : Core.Constraint.OT.NamedConstraint C

Build a binary ALIGN constraint (markedness): violated when the candidate's edge configuration is wrong. The Generalized Alignment schema Align(Cat₁, Edge₁, Cat₂, Edge₂) (@cite{mccarthy-prince-1993}) is given here in its predicate-based form: the user supplies the predicate P c that holds when the edge configuration is misaligned.

Specific alignment instances include left/right edge alignment of morphological constituents to prosodic constituents and the *Misalignment principle of @cite{faust-2026} (root nonfinal element must not be template-final).

Equations

• Phonology.Constraints.mkAlign name P = { name := name, family := Core.Constraint.OT.ConstraintFamily.markedness, eval := fun (c : C) => if P c then 1 else 0 }

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

Gradient ALIGN: counts edge-mismatch violations (@cite{mccarthy-prince-1993}).

Equations

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

theorem Phonology.Constraints.mkMax_is_faithfulness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkMax name P).family = Core.Constraint.OT.ConstraintFamily.faithfulness

MAX constraints are faithfulness constraints.

theorem Phonology.Constraints.mkDep_is_faithfulness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkDep name P).family = Core.Constraint.OT.ConstraintFamily.faithfulness

DEP constraints are faithfulness constraints.

theorem Phonology.Constraints.mkMark_is_markedness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkMark name P).family = Core.Constraint.OT.ConstraintFamily.markedness

Markedness constraints are markedness constraints.

theorem Phonology.Constraints.mkMaxCtx_is_faithfulness {C : Type} (name : String) (D : C → Prop) [DecidablePred D] (Ctx : C → Prop) [DecidablePred Ctx] : (mkMaxCtx name D Ctx).family = Core.Constraint.OT.ConstraintFamily.faithfulness

Contextual MAX constraints are faithfulness constraints.

theorem Phonology.Constraints.mkForbidPairsOnTier_is_markedness {C α β : Type} (name : String) (R : β → β → Prop) [DecidableRel R] (T : Core.Tier α β) (extract : C → List α) : (mkForbidPairsOnTier name R T extract).family = Core.Constraint.OT.ConstraintFamily.markedness

Forbidden-pair constraints are markedness constraints.

theorem Phonology.Constraints.mkAgreeOnTier_is_markedness {C α β : Type} [DecidableEq β] (name : String) (T : Core.Tier α β) (extract : C → List α) : (mkAgreeOnTier name T extract).family = Core.Constraint.OT.ConstraintFamily.markedness

AGREE constraints are markedness constraints.

theorem Phonology.Constraints.mkForbidSingletonOnTier_is_markedness {C α β : Type} (name : String) (P : β → Prop) [DecidablePred P] (T : Core.Tier α β) (extract : C → List α) : (mkForbidSingletonOnTier name P T extract).family = Core.Constraint.OT.ConstraintFamily.markedness

Forbidden-singleton constraints are markedness constraints.

theorem Phonology.Constraints.mkOCP_is_markedness {C α : Type} [DecidableEq α] (name : String) (project : C → List α) : (mkOCP name project).family = Core.Constraint.OT.ConstraintFamily.markedness

OCP constraints are markedness constraints.

theorem Phonology.Constraints.mkOCPOnTier_is_markedness {C α β : Type} [DecidableEq β] (name : String) (T : Core.Tier α β) (extract : C → List α) : (mkOCPOnTier name T extract).family = Core.Constraint.OT.ConstraintFamily.markedness

Tier-driven OCP constraints are markedness constraints.

theorem Phonology.Constraints.mkAlign_is_markedness {C : Type} (name : String) (P : C → Prop) [DecidablePred P] : (mkAlign name P).family = Core.Constraint.OT.ConstraintFamily.markedness

ALIGN constraints are markedness constraints (@cite{mccarthy-prince-1993}).

theorem Phonology.Constraints.mkMax_bounded {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (c : C) : (mkMax name P).eval c ≤ 1

Binary constraints have violations bounded by 1.

theorem Phonology.Constraints.mkMark_bounded {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (c : C) : (mkMark name P).eval c ≤ 1

Binary markedness constraints have violations bounded by 1.

theorem Phonology.Constraints.mkMaxCtx_bounded {C : Type} (name : String) (D : C → Prop) [DecidablePred D] (Ctx : C → Prop) [DecidablePred Ctx] (c : C) : (mkMaxCtx name D Ctx).eval c ≤ 1

Contextual MAX constraints have violations bounded by 1.

def Phonology.Constraints.mkMaxW {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (w : ℚ) : Core.Constraint.WeightedConstraint C

Build a weighted MAX constraint with a given weight.

Equations

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

def Phonology.Constraints.mkMaxCtxW {C : Type} (name : String) (D : C → Prop) [DecidablePred D] (Ctx : C → Prop) [DecidablePred Ctx] (w : ℚ) : Core.Constraint.WeightedConstraint C

Build a weighted contextual MAX constraint.

Equations

• Phonology.Constraints.mkMaxCtxW name D Ctx w = { toNamedConstraint := Phonology.Constraints.mkMaxCtx name D Ctx, weight := w }

def Phonology.Constraints.mkDepW {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (w : ℚ) : Core.Constraint.WeightedConstraint C

Build a weighted DEP constraint.

Equations

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

def Phonology.Constraints.mkIdentW {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (w : ℚ) : Core.Constraint.WeightedConstraint C

Build a weighted IDENT constraint.

Equations

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

def Phonology.Constraints.mkMarkW {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (w : ℚ) : Core.Constraint.WeightedConstraint C

Build a weighted binary markedness constraint.

Equations

• Phonology.Constraints.mkMarkW name P w = { toNamedConstraint := Core.Constraint.OT.mkMark name P, weight := w }

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

Build a weighted gradient markedness constraint.

Equations

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