Constraint Evaluation

@cite{erlewine-2016} @cite{kratzer-1991}

Unified framework for constraint-based candidate evaluation, supporting two comparison modes:

1. Lexicographic (Optimality Theory): constraints are strictly ranked; the first constraint where candidates differ determines the winner. Used in phonology (@cite{prince-smolensky-1993}/2004) and syntactic competition.

2. Subset inclusion (Satisfaction ordering): a candidate is at least as good as another iff it satisfies every criterion the other satisfies. Used in @cite{kratzer-1991}'s modal semantics (see SatisfactionOrdering.lean).

Both select optimal candidates from a set. They differ in comparison: lexLE yields a total order (OT always picks a winner); satLE yields a partial order (incomparable candidates possible, as in Kratzer's semantics).

Connection to SatisfactionOrdering

Core.SatisfactionOrdering.SatisfactionOrdering is the special case where violations are binary (0 = satisfied, ≥1 = violated) and comparison uses subset inclusion (satLE). A SatisfactionOrdering with criteria [c₁,..., cₙ] induces the profile fun a => [if satisfies a c₁ then 0 else 1,..., if satisfies a cₙ then 0 else 1], and atLeastAsGood coincides with satLE on this profile.

def Core.ConstraintEvaluation.lexLE : List Nat → List Nat → Bool

Lexicographic ≤ on violation profiles (lists of violation counts).

Each position is a constraint, ranked highest (head) to lowest (tail). At the first position where profiles differ, fewer violations wins. Missing entries are implicitly 0 (no violation).

lexLE a b = true means "a is at least as harmonic as b."

Equations

• Core.ConstraintEvaluation.lexLE [] [] = true
• Core.ConstraintEvaluation.lexLE [] (head :: tail) = true
• Core.ConstraintEvaluation.lexLE (a :: as) [] = (a == 0 && Core.ConstraintEvaluation.lexLE as [])
• Core.ConstraintEvaluation.lexLE (a :: as) (b :: bs) = if a < b then true else if b < a then false else Core.ConstraintEvaluation.lexLE as bs

def Core.ConstraintEvaluation.lexLT (a b : List Nat) : Bool

Strict lexicographic <: a is strictly more harmonic than b.

Equations

• Core.ConstraintEvaluation.lexLT a b = (Core.ConstraintEvaluation.lexLE a b && !Core.ConstraintEvaluation.lexLE b a)

def Core.ConstraintEvaluation.satLE : List Nat → List Nat → Bool

Subset-inclusion ≤ on violation profiles.

satLE a b = true iff every constraint that b satisfies (0 violations), a also satisfies. Superset-inclusion on sets of satisfied constraints.

Unlike lexLE, this is a partial order — two candidates may be incomparable if each satisfies constraints the other violates. This is @cite{kratzer-1991}'s ordering on worlds relative to a premise set.

Equations

• Core.ConstraintEvaluation.satLE [] [] = true
• Core.ConstraintEvaluation.satLE [] (head :: tail) = true
• Core.ConstraintEvaluation.satLE (a :: as) [] = (a == 0 && Core.ConstraintEvaluation.satLE as [])
• Core.ConstraintEvaluation.satLE (a :: as) (b :: bs) = ((b != 0 || a == 0) && Core.ConstraintEvaluation.satLE as bs)

structure Core.ConstraintEvaluation.OTTableau (Candidate : Type) : Type

An OT tableau: candidates evaluated against ranked constraints.

profile c gives the violation list for candidate c, with position 0 = highest-ranked constraint.

• candidates : List Candidate
• profile : Candidate → List Nat
• nonempty : self.candidates ≠ []

def Core.ConstraintEvaluation.OTTableau.optimal {Candidate : Type} (t : OTTableau Candidate) : List Candidate

Optimal candidates: those not lexicographically dominated.

In a well-formed OT tableau this is typically a singleton — strict ranking ensures a unique winner when profiles differ.

Equations

• t.optimal = List.filter (fun (c : Candidate) => t.candidates.all fun (c' : Candidate) => Core.ConstraintEvaluation.lexLE (t.profile c) (t.profile c')) t.candidates

def Core.ConstraintEvaluation.OTTableau.satOptimal {Candidate : Type} (t : OTTableau Candidate) : List Candidate

Satisfaction-optimal: those not dominated under subset inclusion. May contain multiple candidates (partial order).

Equations

• t.satOptimal = List.filter (fun (c : Candidate) => t.candidates.all fun (c' : Candidate) => Core.ConstraintEvaluation.satLE (t.profile c) (t.profile c')) t.candidates

theorem Core.ConstraintEvaluation.lexLE_refl (a : List Nat) : lexLE a a = true

Lexicographic ≤ is reflexive.

theorem Core.ConstraintEvaluation.satLE_refl (a : List Nat) : satLE a a = true

Satisfaction ≤ is reflexive.

theorem Core.ConstraintEvaluation.lexLE_total (a b : List Nat) (h : a.length = b.length) : lexLE a b = true ∨ lexLE b a = true

Lexicographic ≤ is total for equal-length profiles: OT always determines a winner (modulo ties). Key difference from satLE.

theorem Core.ConstraintEvaluation.satLE_not_total : ¬∀ (a b : List Nat), satLE a b = true ∨ satLE b a = true

satLE is NOT total: candidates can be incomparable when each satisfies a constraint the other violates.

theorem Core.ConstraintEvaluation.optimal_subset {Candidate : Type} (t : OTTableau Candidate) (c : Candidate) : c ∈ t.optimal → c ∈ t.candidates

Optimal candidates are drawn from the candidate set.

def Core.ConstraintEvaluation.blocked {F M : Type} [BEq F] [BEq M] (profile : F × M → List Nat) (s : List (F × M)) (p : F × M) : Bool

A pair ⟨f, m⟩ is blocked by another pair ⟨f', m'⟩ in set s iff:

1. They share exactly one dimension (same form or same meaning, not both),
2. The blocker is strictly more harmonic (lexicographic <).

This is the blocking relation for @cite{blutner-2000}'s superoptimality, used by @cite{de-hoop-malchukov-2008} for bidirectional case optimization.

Equations

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

def Core.ConstraintEvaluation.iterativeSuperoptimal {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) : List (F × M)

Iterative-removal superoptimality: start with all pairs, remove those blocked by any remaining pair, repeat until stable.

Important: this algorithm is equivalent to strong BiOT (eq. 9 of @cite{blutner-2000}) for typical cases — once a pair is removed, it can never return, even if its blockers are themselves eliminated. For @cite{blutner-2000}'s weak BiOT (eq. 14), use superoptimal, which correctly re-evaluates against all original pairs each round.

Equations

• Core.ConstraintEvaluation.iterativeSuperoptimal pairs profile = Core.ConstraintEvaluation.iterativeSuperoptLoop✝ profile pairs pairs.length

def Core.ConstraintEvaluation.superoptimal {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) : List (F × M)

@cite{blutner-2000}'s superoptimality (eq. 14): the greatest fixed point S = {p ∈ Gen | no q ∈ S blocks p}.

A pair ⟨A, τ⟩ is super-optimal iff:

• (Q) No other super-optimal ⟨A', τ⟩ (same meaning) is strictly better
• (I) No other super-optimal ⟨A, τ'⟩ (same form) is strictly better

The Q- and I-principles mutually constrain each other: competition under Q is restricted to I-surviving pairs, and vice versa. This derives @cite{horn-1984}'s division of pragmatic labour: unmarked forms pair with unmarked (stereotypical) meanings, marked forms with marked meanings.

Differs from iterativeSuperoptimal (iterative removal) when indirect blocking creates cycles — superoptimal correctly re-admits pairs whose blockers were themselves eliminated.

Equations

• Core.ConstraintEvaluation.superoptimal pairs profile = Core.ConstraintEvaluation.superoptLoop✝ profile pairs pairs (2 * pairs.length)

def Core.ConstraintEvaluation.strongOptimal {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) : List (F × M)

@cite{blutner-2000}'s strong bidirectional OT (eq. 9): Q and I are evaluated independently against the full candidate set.

⟨A, τ⟩ is optimal iff:

• (Q) No pair ⟨A', τ⟩ in Gen (same meaning) is strictly better
• (I) No pair ⟨A, τ'⟩ in Gen (same form) is strictly better

Unlike superoptimality (eq. 14), the two directions do not constrain each other. Strong-optimal ⊆ super-optimal: every strong-optimal pair is also super-optimal, but superoptimality can admit additional pairs (marked forms for marked meanings).

Equations

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

theorem Core.ConstraintEvaluation.superoptimal_of_unblocked {F M : Type} [BEq F] [BEq M] (pairs : List (F × M)) (profile : F × M → List Nat) (p : F × M) (hp : p ∈ pairs) (hnb : blocked profile pairs p = false) : p ∈ superoptimal pairs profile

A pair that belongs to pairs and is not blocked by any element of pairs is in superoptimal pairs profile.