Tableaux

The OT evaluation vocabulary and machinery. A Tableau is the lexicographic minimisation problem [PS93] solves — a finite candidate set ranked by a ViolationProfile-valued objective. These are OT-tradition names for the LexMinProblem engine in Core.Optimization.Evaluation; downstream OT code uses Tableau/Tableau.optimal rather than the generic spellings. On top of the vocabulary: smart constructors, the structural optimality theorems, and factorial-typology computation.

Main definitions

• Tableau C n — a finite OT tableau over candidates C with n constraints.
• Tableau.optimal — the winner set; optimality is plain membership.
• Ranking n — a constraint ranking ([Pri02]'s domination order).
• Tableau.ofPerm — a tableau from a fixed constraint set CON C n under a ranking r : Ranking n (priority position p reads constraint r p).
• Tableau.ofRanking — the list form: ranked constraint list, list order = priority (position 0 most dominant); Tableau.ofPerm under the identity ranking.
• factorialOptima / factorialTypologySize — the distinct optimal sets predicted across all rankings, and their count.

Main results

• Tableau.mem_optimal_iff / Tableau.optimal_nonempty / Tableau.optimal_subset — the winner characterization; winners exist.
• Tableau.optimal_eq_singleton_iff — sole winner ⟺ strict domination.
• Tableau.ofPerm_zero_mem_optimal / Tableau.ofRanking_zero_mem_optimal / Tableau.ofRanking_zero_mem_optimal_allRankings — a candidate with no violations wins under any (every) ranking.
• Tableau.ofRanking_optimal_zero_first — a satisfiable top constraint forces all winners to satisfy it.

The tableau vocabulary

@[reducible, inline]

abbrev OptimalityTheory.Tableau (C : Type u_1) [DecidableEq C] (n : ℕ) : Type u_1

OT-named alias for LexMinProblem — a finite candidate set ranked by a fixed-length violation profile.

Equations

• OptimalityTheory.Tableau C n = Core.Optimization.Evaluation.LexMinProblem C n

@[reducible, inline]

abbrev OptimalityTheory.Tableau.optimal {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) : Finset C

OT-named alias for LexMinProblem.lexMins — the winning candidates. Optimality is plain membership c ∈ t.optimal, unfolded by mem_optimal_iff; there is no separate winner predicate.

Equations

• t.optimal = Core.Optimization.Evaluation.LexMinProblem.lexMins t

theorem OptimalityTheory.Tableau.mem_optimal_iff {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c : C} : c ∈ t.optimal ↔ c ∈ t.candidates ∧ ∀ d ∈ t.candidates, t.profile c ≤ t.profile d

Membership in the winner set, unfolded: a winner is a candidate whose profile lexicographically bounds the whole tableau.

theorem OptimalityTheory.Tableau.optimal_nonempty {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} : t.optimal.Nonempty

OT-named alias for LexMinProblem.lexMins_nonempty.

theorem OptimalityTheory.Tableau.optimal_subset {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c : C} : c ∈ t.optimal → c ∈ t.candidates

OT-named alias for LexMinProblem.lexMins_subset.

theorem OptimalityTheory.Tableau.le_of_mem_optimal {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c d : C} (hc : c ∈ t.optimal) (hd : d ∈ t.candidates) : t.profile c ≤ t.profile d

A winner's profile bounds every candidate's.

theorem OptimalityTheory.Tableau.mem_optimal_of_profile_eq {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c d : C} (hd : d ∈ t.optimal) (hc : c ∈ t.candidates) (he : t.profile c = t.profile d) : c ∈ t.optimal

Optimality factors through the profile, so it transports along profile equality: scoring like a winner is winning.

theorem OptimalityTheory.Tableau.mem_optimal_of_profile_eq_zero {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c : C} (hc : c ∈ t.candidates) (h0 : t.profile c = 0) : c ∈ t.optimal

A candidate whose profile vanishes wins: 0 is the global lex-minimum.

theorem OptimalityTheory.Tableau.optimal_eq_singleton_iff {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {m : C} (hm : m ∈ t.candidates) : t.optimal = {m} ↔ ∀ c ∈ t.candidates, c ≠ m → t.profile m < t.profile c

A tableau has sole winner m iff m strictly lex-dominates every other candidate.

Tableau constructors

def OptimalityTheory.Tableau.ofPerm {C : Type u_1} [DecidableEq C] {n : ℕ} (con : Constraints.CON C n) (r : Ranking n) (candidates : List C) (h : candidates ≠ [] := by decide) : Tableau C n

Build a Tableau C n from a fixed constraint set con : CON C n under a ranking r : Ranking n: priority position p reads constraint r p, so coordinate 0 of the lexicographic profile is the most dominant constraint. Candidates are deduplicated via List.toFinset.

Equations

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

def OptimalityTheory.Tableau.ofRanking {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (Constraints.Constraint C)) (h : candidates ≠ [] := by decide) : Tableau C ranking.length

Build a Tableau C ranking.length from a candidate list and a ranked constraint list, list order being priority (position 0 most dominant): Tableau.ofPerm under the identity ranking. Study files use this as (Tableau.ofRanking candidates ranking h).optimal = {.winner}.

Equations

• OptimalityTheory.Tableau.ofRanking candidates ranking h = OptimalityTheory.Tableau.ofPerm ranking.get (Equiv.refl (Fin ranking.length)) candidates h

@[simp]

theorem OptimalityTheory.Tableau.ofPerm_candidates {C : Type u_1} [DecidableEq C] {n : ℕ} (con : Constraints.CON C n) (r : Ranking n) (candidates : List C) (h : candidates ≠ []) : (ofPerm con r candidates h).candidates = candidates.toFinset

@[simp]

theorem OptimalityTheory.Tableau.ofPerm_profile {C : Type u_1} [DecidableEq C] {n : ℕ} (con : Constraints.CON C n) (r : Ranking n) (candidates : List C) (h : candidates ≠ []) (c : C) : (ofPerm con r candidates h).profile c = Constraints.buildViolationProfile (fun (p : Fin n) => con (r p)) c

@[simp]

theorem OptimalityTheory.Tableau.ofRanking_candidates {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (Constraints.Constraint C)) (h : candidates ≠ []) : (ofRanking candidates ranking h).candidates = candidates.toFinset

@[simp]

theorem OptimalityTheory.Tableau.ofRanking_profile {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (Constraints.Constraint C)) (h : candidates ≠ []) (c : C) : (ofRanking candidates ranking h).profile c = Constraints.buildViolationProfile ranking.get c

theorem OptimalityTheory.Tableau.ofRanking_optimal_mem {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {ranking : List (Constraints.Constraint C)} {h : candidates ≠ []} (hc : c ∈ (ofRanking candidates ranking h).optimal) : c ∈ candidates

Candidates in (Tableau.ofRanking ...).optimal belong to the original list.

theorem OptimalityTheory.Tableau.ofPerm_optimal_mem {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {con : Constraints.CON C n} {r : Ranking n} {candidates : List C} {h : candidates ≠ []} (hc : c ∈ (ofPerm con r candidates h).optimal) : c ∈ candidates

Candidates in (Tableau.ofPerm ...).optimal belong to the original list.

Top-constraint optimality

theorem OptimalityTheory.Tableau.ofRanking_optimal_zero_first {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {h : candidates ≠ []} (top : Constraints.Constraint C) (rest : List (Constraints.Constraint C)) (hExists : ∃ c₀ ∈ candidates, top c₀ = 0) (hc : c ∈ (ofRanking candidates (top :: rest) h).optimal) : top c = 0

If any candidate has 0 violations on the top-ranked constraint, every optimal candidate has 0 violations on it — constraint dominance: a satisfiable constraint promoted to the top of the ranking forces all winners to satisfy it perfectly.

theorem OptimalityTheory.Tableau.ofPerm_zero_mem_optimal {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {con : Constraints.CON C n} {r : Ranking n} {candidates : List C} {h : candidates ≠ []} (hc : c ∈ candidates) (hzero : ∀ (i : Fin n), con i c = 0) : c ∈ (ofPerm con r candidates h).optimal

A candidate with 0 violations on every constraint of con is optimal in Tableau.ofPerm con r under every ranking r: permuting the coordinates of the all-zero profile leaves it zero.

theorem OptimalityTheory.Tableau.ofRanking_zero_mem_optimal {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {ranking : List (Constraints.Constraint C)} {h : candidates ≠ []} (hc : c ∈ candidates) (hzero : ∀ con ∈ ranking, con c = 0) : c ∈ (ofRanking candidates ranking h).optimal

The list form of ofPerm_zero_mem_optimal.

theorem OptimalityTheory.Tableau.ofRanking_zero_mem_optimal_allRankings {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {h : candidates ≠ []} {constraints : List (Constraints.Constraint C)} (hc : c ∈ candidates) (hzero : ∀ con ∈ constraints, con c = 0) {rk : List (Constraints.Constraint C)} (hrk : rk ∈ constraints.permutations') : c ∈ (ofRanking candidates rk h).optimal

A candidate with 0 violations on every constraint is optimal under every permutation of those constraints — the structural backbone of adj_always_initial in [MR26]: the uniform-initial adjective paradigm has [0, …, 0] on all OP constraints, so it wins regardless of ranking.

Factorial typology

def OptimalityTheory.factorialOptima {C : Type u_1} [DecidableEq C] (candidates : List C) (constraints : List (Constraints.Constraint C)) (h : candidates ≠ [] := by decide) : List (Finset C)

For each ranking of constraints — a permutation, via List.permutations', which unlike List.permutations reduces under decide — the set of optimal candidates; deduplicated. The number of distinct sets is the number of language types the constraint set predicts.

Equations

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

def OptimalityTheory.factorialTypologySize {C : Type u_1} [DecidableEq C] (candidates : List C) (constraints : List (Constraints.Constraint C)) (h : candidates ≠ [] := by decide) : ℕ

The number of distinct language types predicted by the factorial typology.

Equations

• OptimalityTheory.factorialTypologySize candidates constraints h = (OptimalityTheory.factorialOptima candidates constraints h).length