Forbidden-pair constraints

This file defines the forbidden-pair constraints on strings, which carry genuine adjacency logic: Constraint.forbidPairs R, with one violation for each adjacent pair (a, b) satisfying R a b, and its identity and non-identity instances, the OCP ([Gol76], [McC86]) and AGREE. A constraint on candidates of another type, or on a tier, is not a separate constructor but the Constraint.comap of a string constraint along the candidate's string or along erasure of the off-tier symbols. Pulled back along the output form of a correspondence candidate, a string constraint is a markedness constraint (Correspondence.isMarkedness_iff_exists_comap).

On a tier, the zero set of Constraint.forbidPairs R is the tier-based strictly 2-local language of TierStrictlyLocalGrammar.ofForbiddenPairs R p ([HRT11]). The OCP and AGREE instances of this bridge are in Subregular/OCP.lean and Subregular/Agree.lean.

Main definitions

• Constraint.forbidPairs, Constraint.ocp, Constraint.agree: the forbidden-pair constraints on strings.
• Constraint.zeroSet: the zero-violation language of a constraint on strings.

Main results

• Constraint.zeroSet_comap: pulling a constraint back pulls its zero set back.
• Constraint.zeroSet_comap_filter_forbidPairs: on a tier, the zero set of the forbidden-pair constraint is the TSL₂ language of ofForbiddenPairs.

Implementation notes

Constraint.ocp and Constraint.agree compare whole symbols. Over segments, ocp is the identity OCP rather than OCP-Place, and agree is AGREE[F] only after the string is projected to the values of the feature F.

References

• J. A. Goldsmith, Autosegmental Phonology (1976)
• J. J. McCarthy, OCP Effects: Gemination and Antigemination (1986)
• J. Heinz, C. Rawal and H. G. Tanner, Tier-based Strictly Local Constraints for Phonology (2011)
• I. Berent, Three arguments for abstraction in phonology (2026)

def OptimalityTheory.Constraint.forbidPairs {α : Type u_1} (R : α → α → Prop) [DecidableRel R] : Constraint (List α)

The forbidden-pair constraint on strings, with one violation for each adjacent pair (a, b) satisfying R a b.

Equations

• OptimalityTheory.Constraint.forbidPairs R = Subregular.countAdjacent R

def OptimalityTheory.Constraint.ocp {α : Type u_1} [DecidableEq α] : Constraint (List α)

The OCP ([Gol76], [McC86]), the forbidden-pair constraint against adjacent identical elements, polymorphic over the feature type ([Ber26]).

Equations

• OptimalityTheory.Constraint.ocp = OptimalityTheory.Constraint.forbidPairs fun (x1 x2 : α) => x1 = x2

def OptimalityTheory.Constraint.agree {α : Type u_1} [DecidableEq α] : Constraint (List α)

AGREE, the forbidden-pair constraint against adjacent distinct elements and the dual of Constraint.ocp.

Equations

• OptimalityTheory.Constraint.agree = OptimalityTheory.Constraint.forbidPairs fun (x1 x2 : α) => x1 ≠ x2

def OptimalityTheory.Constraint.zeroSet {α : Type u_1} (c : Constraint (List α)) : Language α

The language of strings that satisfy c, with zero violations. It lets the eval = 0 predicate compose with Language.IsRegular and the subregular classes (IsTierStrictlyLocal, IsBTC).

Equations

• c.zeroSet = {w : List α | c w = 0}

theorem OptimalityTheory.Constraint.ocp_cons_self {α : Type u_1} [DecidableEq α] (a : α) (w : List α) : ocp (a :: a :: w) = 1 + ocp (a :: w)

theorem OptimalityTheory.Constraint.ocp_cons_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (h : a ≠ b) (w : List α) : ocp (a :: b :: w) = ocp (b :: w)

theorem OptimalityTheory.Constraint.ocp_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (w : List α) : ocp (List.map f w) = ocp w

The OCP is invariant under an injective relabelling of the elements.

theorem OptimalityTheory.Constraint.mem_zeroSet {α : Type u_1} (c : Constraint (List α)) (w : List α) : w ∈ c.zeroSet ↔ c w = 0

@[simp]

theorem OptimalityTheory.Constraint.zeroSet_comap {α : Type u_1} {β : Type u_2} (f : List α → List β) (c : Constraint (List β)) : (comap f c).zeroSet = f ⁻¹' c.zeroSet

Pulling a constraint back along a string map pulls its zero set back.

theorem OptimalityTheory.Constraint.forbidPairs_eq_zero_iff {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (w : List α) : forbidPairs R w = 0 ↔ List.IsChain (fun (a b : α) => ¬R a b) w

A string satisfies the forbidden-pair constraint iff no two adjacent elements are R-related.

theorem OptimalityTheory.Constraint.zeroSet_comap_filter_forbidPairs {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] : (comap (fun (w : List α) => List.filter (fun (x : α) => decide (p x)) w) (forbidPairs R)).zeroSet = (Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs R p).language

On the tier p, the zero set of the forbidden-pair constraint is the language of the TSL₂ grammar TierStrictlyLocalGrammar.ofForbiddenPairs R p.