Tableaux

The OT evaluation vocabulary and machinery. A candidate's violation profile under a constraint set is its violation vector ordered lexicographically, Lex (Fin n → ℕ) ([Rig09b]); the lexicographic order is Optimality Theory's strict domination, while Harmonic Grammar weights the same vector without ordering it (HarmonicGrammar.harmonyScore). A Tableau is the lexicographic minimisation problem [PS93] solves — a finite candidate set ranked by a ViolationProfile-valued objective, whose winners are the candidates with a profile at most every candidate's under mathlib's Pi.Lex order. On top of the vocabulary: smart constructors and the structural optimality theorems.

Main definitions

• ViolationProfile n — Lex (Fin n → ℕ), a fixed-length violation vector. The profile of a candidate c under a constraint set con read in rank order r is toLex fun p ↦ con (r p) c.
• 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 constraint set con : ConstraintSet C ι 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.
• Tableau.ofFintype — the same over every candidate of a finite type.
• Tableau.ofOrder — a tableau from a constraint order (labels, most dominant first) and the candidates' violation marks by label: the paper-tableau form.

Main results

• Tableau.mem_optimal_iff / Tableau.optimal_nonempty / Tableau.optimal_subset — the winner characterization; winners exist.
• Tableau.optimal_eq_singleton_iff / Tableau.optimal_eq_singleton_iff_pair — sole winner ⟺ strict domination.
• Tableau.ofPerm_profile_lt_iff / Tableau.ofPerm_profile_lt_iff_exists_dominates — a candidate beats another under a ranking iff the most dominant constraint distinguishing them prefers it, iff some constraint preferring it dominates every constraint preferring the other.
• Tableau.notMem_optimal_of_lt / Tableau.ofPerm_notMem_optimal_of_lt — harmonic bounding: a candidate beaten pointwise never wins.
• Tableau.forall_ofPerm_profile_lt_iff / Tableau.exists_mem_ofPerm_optimal_iff_pair — a candidate beats a competitor under every ranking iff it bounds it, so a candidate wins against its only competitor under some ranking iff it is not bounded.
• Tableau.ofPerm_zero_mem_optimal / Tableau.ofRanking_zero_mem_optimal — a candidate with no violations wins under every ranking, and Tableau.ofPerm_eq_zero_of_mem_optimal — then every winner has no violations.
• Tableau.ofRanking_optimal_zero_first — a satisfiable top constraint forces all winners to satisfy it, via ViolationProfile.le_apply_zero.

References

• A. Prince and P. Smolensky, Optimality Theory: Constraint Interaction in Generative Grammar (1993)
• A. Prince, Entailed Ranking Arguments (2002)
• J. Riggle, Violation Semirings in Optimality Theory (2009)

Violation profiles

@[reducible, inline]

abbrev OptimalityTheory.ViolationProfile (n : ℕ) : Type

A fixed-length violation profile, the violation vector Fin n → ℕ under its lexicographic order.

Equations

• OptimalityTheory.ViolationProfile n = Lex (Fin n → ℕ)

theorem OptimalityTheory.ViolationProfile.le_apply_zero {n : ℕ} {a b : ViolationProfile (n + 1)} (h : a ≤ b) : a 0 ≤ b 0

A profile at most another is at most it on the first constraint.

The tableau vocabulary

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

An OT tableau is a finite candidate set scored by a fixed-length violation profile, with a witness that there is a candidate.

• candidates : Finset C

  The candidates.

• profile : C → ViolationProfile n

  Each candidate's violation profile.

• nonempty : self.candidates.Nonempty

  A tableau has a candidate.

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

The winning candidates, those whose profile is lexicographically at most every candidate's; the comparison is decided by Pi.Lex.decidableLE. Optimality is plain membership c ∈ t.optimal, unfolded by mem_optimal_iff; there is no separate winner predicate.

Equations

• t.optimal = {c ∈ t.candidates | ∀ d ∈ t.candidates, t.profile c ≤ t.profile d}

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

A winner is a candidate whose profile is lexicographically below that of every candidate.

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

Every tableau has a winner, since the linearly ordered image of a nonempty finset has a minimum.

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

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, since 0 is the least profile.

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.

@[simp]

theorem OptimalityTheory.Tableau.optimal_singleton {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c : C} (hc : t.candidates = {c}) : t.optimal = {c}

A tableau with a single candidate has it as sole winner.

theorem OptimalityTheory.Tableau.optimal_eq_singleton_iff_pair {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c d : C} (hcand : t.candidates = {c, d}) (hne : c ≠ d) : t.optimal = {c} ↔ t.profile c < t.profile d

A two-candidate tableau has sole winner c iff c strictly lex-dominates d.

theorem OptimalityTheory.Tableau.mem_optimal_iff_pair {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c d : C} (hcand : t.candidates = {c, d}) : c ∈ t.optimal ↔ ¬t.profile d < t.profile c

In a two-candidate tableau, c wins iff d does not strictly lex-dominate it.

theorem OptimalityTheory.Tableau.notMem_optimal_of_lt {C : Type u_1} [DecidableEq C] {n : ℕ} {t : Tableau C n} {c d : C} (hc : c ∈ t.candidates) (h : t.profile c < t.profile d) : d ∉ t.optimal

A candidate strictly lex-dominated by a competitor is no winner.

Tableau constructors

def OptimalityTheory.Tableau.ofPerm {C : Type u_1} [DecidableEq C] {n : ℕ} {ι : Type u_2} (con : ConstraintSet C ι) (r : Ranking ι n) (candidates : List C) (h : candidates ≠ [] := by first | decide | simp) : Tableau C n

ofPerm con r candidates is the tableau of a constraint set con : ConstraintSet C ι 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

• OptimalityTheory.Tableau.ofPerm con r candidates h = { candidates := candidates.toFinset, profile := fun (c : C) => toLex fun (p : Fin n) => con (r p) c, nonempty := ⋯ }

def OptimalityTheory.Tableau.ofRanking {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (Constraint C)) (h : candidates ≠ [] := by first | decide | simp) : 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

def OptimalityTheory.Tableau.ofFintype {C : Type u_1} [DecidableEq C] (ranking : List (Constraint C)) [Fintype C] [Nonempty C] : Tableau C ranking.length

Build a Tableau C ranking.length whose candidates are every inhabitant of the finite type C — the form for a candidate type that enumerates exactly the candidate set.

Equations

• OptimalityTheory.Tableau.ofFintype ranking = { candidates := Finset.univ, profile := fun (c : C) => toLex fun (x : Fin ranking.length) => ranking.get x c, nonempty := ⋯ }

def OptimalityTheory.Tableau.ofOrder {C : Type u_1} [DecidableEq C] {L : Type u_3} (order : List L) (marks : C → L → ℕ) [Fintype C] [Nonempty C] : Tableau C order.length

Build a tableau from a constraint order — labels L, most dominant first — and each candidate's violation marks by label, as a paper's tableau is printed: order is its column order and marks c l the cell. Candidates are every inhabitant of C.

Equations

• OptimalityTheory.Tableau.ofOrder order marks = { candidates := Finset.univ, profile := fun (c : C) => toLex fun (p : Fin order.length) => marks c (order.get p), nonempty := ⋯ }

@[simp]

theorem OptimalityTheory.Tableau.ofPerm_candidates {C : Type u_1} [DecidableEq C] {n : ℕ} {ι : Type u_2} (con : ConstraintSet C ι) (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 : ℕ} {ι : Type u_2} (con : ConstraintSet C ι) (r : Ranking ι n) (candidates : List C) (h : candidates ≠ []) (c : C) : (ofPerm con r candidates h).profile c = toLex 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 (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 (Constraint C)) (h : candidates ≠ []) (c : C) : (ofRanking candidates ranking h).profile c = toLex fun (x : Fin ranking.length) => ranking.get x c

@[simp]

theorem OptimalityTheory.Tableau.ofFintype_candidates {C : Type u_1} [DecidableEq C] (ranking : List (Constraint C)) [Fintype C] [Nonempty C] : (ofFintype ranking).candidates = Finset.univ

@[simp]

theorem OptimalityTheory.Tableau.ofFintype_profile {C : Type u_1} [DecidableEq C] (ranking : List (Constraint C)) [Fintype C] [Nonempty C] (c : C) : (ofFintype ranking).profile c = toLex fun (x : Fin ranking.length) => ranking.get x c

@[simp]

theorem OptimalityTheory.Tableau.ofOrder_candidates {C : Type u_1} [DecidableEq C] {L : Type u_3} (order : List L) (marks : C → L → ℕ) [Fintype C] [Nonempty C] : (ofOrder order marks).candidates = Finset.univ

@[simp]

theorem OptimalityTheory.Tableau.ofOrder_profile {C : Type u_1} [DecidableEq C] {L : Type u_3} (order : List L) (marks : C → L → ℕ) [Fintype C] [Nonempty C] (c : C) (p : Fin order.length) : (ofOrder order marks).profile c p = marks c (order.get p)

theorem OptimalityTheory.Tableau.ofRanking_optimal_mem {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {ranking : List (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} {ι : Type u_2} {con : ConstraintSet C ι} {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.

theorem OptimalityTheory.Tableau.ofPerm_profile_lt_iff {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} {d : C} : (ofPerm con r candidates h).profile c < (ofPerm con r candidates h).profile d ↔ Pi.Lex r.Dominates (fun {i : ι} (x1 x2 : ℕ) => x1 < x2) (fun (x : ι) => con x c) fun (x : ι) => con x d

Under a ranking, one candidate beats another iff their violation vectors are lexicographically ordered under dominance: the most dominant constraint that distinguishes them prefers it.

theorem OptimalityTheory.Tableau.ofPerm_profile_lt_iff_exists_dominates {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} {d : C} : (ofPerm con r candidates h).profile c < (ofPerm con r candidates h).profile d ↔ ∃ (i : ι), con i c < con i d ∧ ∀ (j : ι), con j d < con j c → r.Dominates i j

One candidate beats another iff some constraint preferring it dominates every constraint preferring the other, which is the elementary ranking condition.

theorem OptimalityTheory.Tableau.ofPerm_optimal_eq_singleton_iff {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} (hc : c ∈ candidates) : (ofPerm con r candidates h).optimal = {c} ↔ ∀ d ∈ candidates, d ≠ c → ∃ (i : ι), con i c < con i d ∧ ∀ (j : ι), con j d < con j c → r.Dominates i j

A candidate is the sole winner under a ranking iff, against each competitor, some constraint preferring it dominates every constraint preferring the competitor.

theorem OptimalityTheory.Tableau.ofPerm_profile_lt_of_lt {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} {d : C} (hlt : (fun (x : ι) => con x c) < fun (x : ι) => con x d) : (ofPerm con r candidates h).profile c < (ofPerm con r candidates h).profile d

A candidate that beats another pointwise on the constraint set beats it under every ranking of the set.

theorem OptimalityTheory.Tableau.ofPerm_notMem_optimal_of_lt {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} {d : C} (hc : c ∈ candidates) (hlt : (fun (x : ι) => con x c) < fun (x : ι) => con x d) : d ∉ (ofPerm con r candidates h).optimal

A candidate beaten pointwise on the constraint set by a competitor is harmonically bounded, that is, optimal under no ranking of the set.

theorem OptimalityTheory.Tableau.ofPerm_optimal_eq_singleton_of_forall_lt {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} (hc : c ∈ candidates) (hlt : ∀ d ∈ candidates, d ≠ c → (fun (x : ι) => con x c) < fun (x : ι) => con x d) : (ofPerm con r candidates h).optimal = {c}

A candidate that harmonically bounds every competitor is the sole winner under every ranking of the constraint set.

theorem OptimalityTheory.Tableau.ofPerm_profile_lt_of_forall_dominates {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} {d : C} {i : ι} (hi : con i c < con i d) (hr : ∀ (j : ι), j ≠ i → r.Dominates i j) : (ofPerm con r candidates h).profile c < (ofPerm con r candidates h).profile d

A candidate beats a competitor under a ranking that puts a constraint preferring it on top.

theorem OptimalityTheory.Tableau.exists_ofPerm_profile_lt_iff {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {candidates : List C} {h : candidates ≠ []} [Fintype ι] (hn : Fintype.card ι = n) {d : C} : (∃ (r : Ranking ι n), (ofPerm con r candidates h).profile c < (ofPerm con r candidates h).profile d) ↔ ∃ (i : ι), con i c < con i d

A candidate beats a competitor under some ranking iff some constraint prefers it.

theorem OptimalityTheory.Tableau.forall_ofPerm_profile_lt_iff {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {candidates : List C} {h : candidates ≠ []} [Fintype ι] (hn : Fintype.card ι = n) {d : C} : (∀ (r : Ranking ι n), (ofPerm con r candidates h).profile c < (ofPerm con r candidates h).profile d) ↔ (fun (x : ι) => con x c) < fun (x : ι) => con x d

A candidate beats a competitor under every ranking iff it harmonically bounds it, beating it pointwise on the constraint set.

theorem OptimalityTheory.Tableau.exists_mem_ofPerm_optimal_iff_pair {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {candidates : List C} {h : candidates ≠ []} [Fintype ι] (hn : Fintype.card ι = n) {d : C} (hcand : candidates.toFinset = {c, d}) : (∃ (r : Ranking ι n), c ∈ (ofPerm con r candidates h).optimal) ↔ ¬(fun (x : ι) => con x d) < fun (x : ι) => con x c

A candidate wins against its only competitor under some ranking iff the competitor does not harmonically bound it.

theorem OptimalityTheory.Tableau.exists_ofPerm_optimal_eq_singleton_iff_pair {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {candidates : List C} {h : candidates ≠ []} [Fintype ι] (hn : Fintype.card ι = n) {d : C} (hcand : candidates.toFinset = {c, d}) (hne : c ≠ d) : (∃ (r : Ranking ι n), (ofPerm con r candidates h).optimal = {c}) ↔ ∃ (i : ι), con i c < con i d

A candidate is the sole winner against its only competitor under some ranking iff some constraint prefers it.

Top-constraint optimality

theorem OptimalityTheory.Tableau.ofRanking_optimal_zero_first {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {h : candidates ≠ []} (top : Constraint C) (rest : List (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} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} (hc : c ∈ candidates) (hzero : ∀ (i : ι), 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, since permuting the coordinates of the all-zero profile leaves it zero.

theorem OptimalityTheory.Tableau.ofPerm_eq_zero_of_mem_optimal {C : Type u_1} [DecidableEq C] {n : ℕ} {c : C} {ι : Type u_2} {con : ConstraintSet C ι} {r : Ranking ι n} {candidates : List C} {h : candidates ≠ []} {c₀ : C} (hc₀ : c₀ ∈ candidates) (h₀ : ∀ (i : ι), con i c₀ = 0) (hc : c ∈ (ofPerm con r candidates h).optimal) (i : ι) : con i c = 0

If some candidate satisfies every constraint of con, then under every ranking so does every optimal candidate.

theorem OptimalityTheory.Tableau.ofRanking_zero_mem_optimal {C : Type u_1} [DecidableEq C] {c : C} {candidates : List C} {ranking : List (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.