Constraint rankings

A ranking of a constraint set indexed by ι ([Pri02]'s total domination order ≫) is an enumeration r : Fin n ≃ ι of the constraints in rank order: r p is the constraint at rank position p, position 0 most dominant, and r.symm i is the rank position of i. For ι = Fin n a ranking is a permutation, Equiv.Perm (Fin n). Ranking.Dominates is the induced strict dominance relation, a strict total order on the constraints, and Ranking.toRel its reflexive closure, from which the ranking is recoverable (toRel_le_toRel_iff); Ranking.take r k is the set of its top k constraints. Reading two violation vectors in rank order and comparing them lexicographically is Pi.Lex under dominance (toLex_comp_lt_iff). The Tableau machinery evaluates under a ranking, and the elementary-ranking-condition layer (ElementaryRankingCondition.lean) infers rankings from winner–loser pairs. Rankings carry the discrete σ-algebra, so that a distribution over rankings, a partially ordered grammar's or stochastic OT's, is a Measure.

Implementation notes

A ranking is stored as the enumeration rather than as the order relation, so that rankings can be enumerated and compared decidably; the relation is derived (Dominates). The length n is a parameter rather than Fintype.card ι, so that a ranking of Fin n is literally a permutation; card_eq recovers Fintype.card ι = n from any ranking, and a statement quantifying over all rankings is vacuous when n does not match.

References

• A. Prince, Entailed Ranking Arguments (2002)

@[reducible, inline]

abbrev OptimalityTheory.Ranking (ι : Type u_1) (n : ℕ) : Type u_1

A ranking of the constraints ι into n rank positions, Prince's total domination order ≫, is an enumeration of the constraints in rank order: r p is the constraint at rank position p, position 0 being the most dominant, and r.symm i is the rank position of i.

Equations

• OptimalityTheory.Ranking ι n = (Fin n ≃ ι)

@[instance_reducible]

instance OptimalityTheory.instMeasurableSpaceRanking {ι : Type u_1} {n : ℕ} : MeasurableSpace (Ranking ι n)

There are finitely many rankings of n constraints, and every set of them is measurable.

Equations

• OptimalityTheory.instMeasurableSpaceRanking = ⊤

instance OptimalityTheory.instDiscreteMeasurableSpaceRanking {ι : Type u_1} {n : ℕ} : DiscreteMeasurableSpace (Ranking ι n)

theorem OptimalityTheory.total_eq_of_le {α : Type u_2} {r s : α → α → Prop} [ht : Std.Total r] [ha : Std.Antisymm s] (h : r ≤ s) : r = s

A total relation is maximal among antisymmetric relations, so an antisymmetric relation above it in the pointwise lattice equals it.

theorem OptimalityTheory.Ranking.card_eq {ι : Type u_1} {n : ℕ} [Fintype ι] (r : Ranking ι n) : Fintype.card ι = n

A ranking enumerates all the constraints, so their number is the number of rank positions.

def OptimalityTheory.Ranking.Dominates {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (i j : ι) : Prop

Constraint i dominates constraint j under r when it sits at a lower, more dominant, rank position.

Equations

• r.Dominates i j = ((Equiv.symm r) i < (Equiv.symm r) j)

@[instance_reducible]

instance OptimalityTheory.Ranking.instDecidableDominates {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (i j : ι) : Decidable (r.Dominates i j)

Equations

• r.instDecidableDominates i j = { decide := (↑((Equiv.symm r) i)).succ.ble ↑((Equiv.symm r) j), reflects_decide := ⋯ }

instance OptimalityTheory.Ranking.instIsStrictTotalOrderDominates {ι : Type u_1} {n : ℕ} (r : Ranking ι n) : IsStrictTotalOrder ι r.Dominates

@[simp]

theorem OptimalityTheory.Ranking.dominates_apply_iff {ι : Type u_1} {n : ℕ} (r : Ranking ι n) {p q : Fin n} : r.Dominates (r p) (r q) ↔ p < q

Dominance between ranked positions is position order.

theorem OptimalityTheory.Ranking.toLex_comp_lt_iff {ι : Type u_1} {n : ℕ} (r : Ranking ι n) {β : Type u_2} [LT β] (v w : ι → β) : toLex (v ∘ ⇑r) < toLex (w ∘ ⇑r) ↔ Pi.Lex r.Dominates (fun {i : ι} (x1 x2 : β) => x1 < x2) v w

Reading two vectors in rank order and comparing them lexicographically is Pi.Lex under dominance.

@[simp]

theorem OptimalityTheory.Ranking.one_dominates_iff {n : ℕ} {i j : Fin n} : Dominates 1 i j ↔ i < j

Under the identity ranking 1, dominance is index order.

@[instance_reducible]

instance OptimalityTheory.Ranking.instSMulFinLexForall {n : ℕ} {α : Type u_2} : SMul (Ranking (Fin n) n) (Lex (Fin n → α))

A ranking reads a lex-ordered vector in rank order, so that coordinate p of r • v is the value of v at the constraint ranked p-th. Reordering is the one operation that breaks and reconstitutes the lex order — the Sₙ action whose orbit structure is constraint ranking. (With this convention the action is a right action: (r * s) • v = s • r • v.)

Equations

• OptimalityTheory.Ranking.instSMulFinLexForall = { smul := fun (r : OptimalityTheory.Ranking (Fin n) n) (v : Lex (Fin n → α)) => toLex fun (p : Fin n) => ofLex v (r p) }

@[simp]

theorem OptimalityTheory.Ranking.smul_apply {n : ℕ} {α : Type u_2} (r : Ranking (Fin n) n) (v : Lex (Fin n → α)) (p : Fin n) : ofLex (r • v) p = ofLex v (r p)

@[simp]

theorem OptimalityTheory.Ranking.one_smul {n : ℕ} {α : Type u_2} (v : Lex (Fin n → α)) : 1 • v = v

theorem OptimalityTheory.Ranking.exists_dominates {n : ℕ} {i j : Fin n} (hij : i ≠ j) : ∃ (r : Ranking (Fin n) n), r.Dominates i j

Any two distinct constraints can be ranked either way, so some ranking makes i dominate j.

theorem OptimalityTheory.Ranking.exists_forall_dominates {ι : Type u_1} {n : ℕ} [Fintype ι] (i : ι) (h : Fintype.card ι = n := by simp) : ∃ (r : Ranking ι n), ∀ (j : ι), j ≠ i → r.Dominates i j

Any constraint can be ranked above all the others.

The top constraints of a ranking

def OptimalityTheory.Ranking.take {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (k : Fin (n + 1)) : Finset ι

The top k constraints of a ranking.

Equations

• r.take k = Finset.map (Equiv.toEmbedding r) {p : Fin n | ↑p < ↑k}

@[simp]

theorem OptimalityTheory.Ranking.mem_take {ι : Type u_1} {n : ℕ} (r : Ranking ι n) {k : Fin (n + 1)} {i : ι} : i ∈ r.take k ↔ ↑((Equiv.symm r) i) < ↑k

@[simp]

theorem OptimalityTheory.Ranking.card_take {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (k : Fin (n + 1)) : (r.take k).card = ↑k

@[simp]

theorem OptimalityTheory.Ranking.take_zero {ι : Type u_1} {n : ℕ} (r : Ranking ι n) : r.take 0 = ∅

@[simp]

theorem OptimalityTheory.Ranking.take_last {ι : Type u_1} {n : ℕ} (r : Ranking ι n) [Fintype ι] : r.take (Fin.last n) = Finset.univ

theorem OptimalityTheory.Ranking.take_succ {ι : Type u_1} {n : ℕ} (r : Ranking ι n) [DecidableEq ι] (k : Fin n) : r.take k.succ = insert (r k) (r.take k.castSucc)

Passing from the top k constraints to the top k + 1 adds the constraint ranked k.

theorem OptimalityTheory.Ranking.apply_notMem_take {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (k : Fin n) : r k ∉ r.take k.castSucc

theorem OptimalityTheory.Ranking.mem_take_of_dominates {ι : Type u_1} {n : ℕ} (r : Ranking ι n) {k : Fin (n + 1)} {i j : ι} (h : r.Dominates i j) (hj : j ∈ r.take k) : i ∈ r.take k

A constraint that dominates a member of a prefix is in the prefix.

theorem OptimalityTheory.Ranking.exists_take_eq {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (D : Finset ι) (hD : ∀ i ∈ D, ∀ j ∉ D, r.Dominates i j) : ∃ (k : Fin (n + 1)), r.take k = D

A set of constraints that dominate every constraint outside it is a prefix.

The ranking as a total order

def OptimalityTheory.Ranking.toRel {ι : Type u_1} {n : ℕ} (r : Ranking ι n) : ι → ι → Prop

The dominance-or-equal relation of a ranking holds of i and j when i is ranked at least as high as j; it is the reflexive closure of Dominates (toRel_iff) and a total order on the constraints.

Equations

• r.toRel i j = ((Equiv.symm r) i ≤ (Equiv.symm r) j)

@[instance_reducible]

instance OptimalityTheory.Ranking.instDecidableToRel {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (i j : ι) : Decidable (r.toRel i j)

Equations

• r.instDecidableToRel i j = { decide := (↑((Equiv.symm r) i)).ble ↑((Equiv.symm r) j), reflects_decide := ⋯ }

instance OptimalityTheory.Ranking.instIsPartialOrderToRel {ι : Type u_1} {n : ℕ} (r : Ranking ι n) : IsPartialOrder ι r.toRel

instance OptimalityTheory.Ranking.instTotalToRel {ι : Type u_1} {n : ℕ} (r : Ranking ι n) : Std.Total r.toRel

theorem OptimalityTheory.Ranking.toRel_iff {ι : Type u_1} {n : ℕ} (r : Ranking ι n) {i j : ι} : r.toRel i j ↔ i = j ∨ r.Dominates i j

toRel is the reflexive closure of Dominates.

theorem OptimalityTheory.Ranking.toRel_iff_dominates {ι : Type u_1} {n : ℕ} (r : Ranking ι n) {i j : ι} (hij : i ≠ j) : r.toRel i j ↔ r.Dominates i j

On distinct constraints, toRel is Dominates.

@[simp]

theorem OptimalityTheory.Ranking.toRel_mul {n : ℕ} (g σ : Ranking (Fin n) n) (i j : Fin n) : (g * σ).toRel i j ↔ σ.toRel (g⁻¹ i) (g⁻¹ j)

Relabeling constraints by g pulls the induced order back along g⁻¹.

theorem OptimalityTheory.Ranking.toRel_injective {ι : Type u_1} {n : ℕ} : Function.Injective toRel

A ranking is recoverable from its induced total order.

theorem OptimalityTheory.Ranking.toRel_le_toRel_iff {ι : Type u_1} {n : ℕ} {σ τ : Ranking ι n} : σ.toRel ≤ τ.toRel ↔ σ = τ

Total orders comparable in the relation lattice coincide, so toRel is rigid: nothing sits strictly between two ranking-induced orders.

theorem OptimalityTheory.Ranking.exists_toRel_eq {ι : Type u_1} {n : ℕ} [Fintype ι] (s : ι → ι → Prop) [IsLinearOrder ι s] (h : Fintype.card ι = n := by simp) : ∃ (σ : Ranking ι n), σ.toRel = s

Every linear order on the constraints is the induced order of a ranking, the surjectivity companion to toRel_injective: enumerate the constraints in s-order (Finset.sort) and read off the ranking.

theorem OptimalityTheory.Ranking.exists_dominates_iff {ι : Type u_1} {n : ℕ} [Fintype ι] {β : Type u_2} [LinearOrder β] (f : ι → β) (hf : Function.Injective f) (h : Fintype.card ι = n := by simp) : ∃ (σ : Ranking ι n), ∀ (i j : ι), σ.Dominates i j ↔ f i < f j

Constraints keyed injectively into a linear order are ranked by their keys.