Tier-based markedness constraint library

[PS93] [McCP95] [Gol76] [McC86]

Constructors for the framework-neutral Constraint C = C → ℕ (shared by OT and Harmonic Grammar) whose content goes beyond a single predicate.

Binary constraints are just Constraint.binary P (Defs): MAX, DEP, IDENT, ALIGN, *STRUC differ only in the predicate you pass and the def name you give — post-family-deletion they are the same function, so there is no mkMax/mkDep/… The faithfulness/markedness family is recovered structurally (OptimalityTheory.Correspondence), not from a constructor. Contextual faithfulness ([CP11b]) is Constraint.binary (fun c => deleted c ∧ ctx c).

This file provides the gradient, tier-projected markedness constructors — OCP, AGREE, forbidden pairs/singletons — which carry genuine adjacency logic.

def Constraints.mkForbidPairsOnTier {C : Type u_1} {α : Type u_2} {β : Type u_3} (R : β → β → Prop) [DecidableRel R] (T : TierProjection α β) (extract : C → List α) : Constraint C

A markedness constraint penalizing tier-adjacent forbidden pairs: project the candidate's symbols onto tier T, then count tier-adjacent pairs (a, b) with R a b ([Gol76]; the TSL₂ bridge is mkForbidPairsOnTier_zero_iff_in_lang).

Equations

• Constraints.mkForbidPairsOnTier R T extract c = Subregular.countAdjacent R (T.apply (extract c))

def Constraints.mkForbidSingletonOnTier {C : Type u_1} {α : Type u_2} {β : Type u_3} (P : β → Prop) [DecidablePred P] (T : TierProjection α β) (extract : C → List α) : Constraint C

A markedness constraint penalizing tier elements satisfying P (the SL₁ sibling of mkForbidPairsOnTier; e.g. *Coda).

Equations

• Constraints.mkForbidSingletonOnTier P T extract c = List.countP (fun (x : β) => decide (P x)) (T.apply (extract c))

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

Count adjacent identical pairs — countAdjacent (· = ·), under the OCP name.

Equations

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

def Constraints.mkOCP {C : Type u_1} {α : Type u_2} [DecidableEq α] (project : C → List α) : Constraint C

An OCP constraint ([McC86]): penalizes adjacent identical elements on the tier extracted by project. Polymorphic over the feature type ([Ber26]).

Equations

• Constraints.mkOCP project c = Constraints.adjacentIdentical (project c)

def Constraints.mkOCPOnTier {C : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq β] (T : TierProjection α β) (extract : C → List α) : Constraint C

An OCP constraint from a TierProjection — the R := (· = ·) instance of mkForbidPairsOnTier ([Gol76] [McC86] [Ber26]).

Equations

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

def Constraints.mkAgreeOnTier {C : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq β] (T : TierProjection α β) (extract : C → List α) : Constraint C

An AGREE constraint — the R := (· ≠ ·) instance of mkForbidPairsOnTier, the non-identity dual of mkOCPOnTier.

Equations

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