ERC sets and antimatroids

Merchant and Riggle show that consistent sets of elementary ranking conditions (ERCs) over n constraints and antimatroids on Fin n are the same objects. A set of ERCs determines the family of the top segments of the rankings that satisfy it, which is an antimatroid; an antimatroid determines one ERC for each of its rooted circuits. The two maps are inverse to each other, the second up to logical equivalence, and both preserve entailment.

Main definitions

• ERC.IsFeasible E S: S is the set of the top k constraints of a ranking satisfying E.
• ERC.toAntimatroid E: the antimatroid of a consistent set of ERCs.
• ERC.ofAntimatroid A: the ERCs of the rooted circuits of an antimatroid.

Main statements

• ERC.toAntimatroid_ofAntimatroid: an antimatroid is the antimatroid of its ERCs.
• ERC.satisfiedBy_ofAntimatroid_toAntimatroid_iff: the ERCs of the antimatroid of E are satisfied by exactly the rankings that satisfy E.
• ERC.isFeasible_iff_forall_singleton_of_simple: for ERCs that each rank one constraint over one other, the feasible sets are those feasible for each ERC alone, while ERC.exists_forall_isFeasible_singleton_not_isFeasible shows this fails in general.

Implementation notes

• Rankings satisfying a set of ERCs are built by sorting the constraints by a key into a lexicographic product (Ranking.exists_dominates_iff), and their top segments are read off with Ranking.exists_take_eq.
• The paper's remark after its definition of the feasible family, and its proof of union closure, assume that a set feasible for each ERC alone is feasible for all of them; ERC.exists_forall_isFeasible_singleton_not_isFeasible refutes this, so union closure is proved by merging rankings instead.
• The paper states that the ERCs of the antimatroid of E equal E, but proves that they are satisfied by the same rankings. Equality fails, since a chain's rooted circuits include its transitive edges, so the theorem states the equivalence.
• Antimatroids carry a ground set, as mathlib's Matroid does; the inverse laws assume it is all of Fin n, which is the paper's setting.

References

• N. Merchant, J. Riggle, OT grammars, beyond partial orders: ERC sets and antimatroids (2016)
• B. L. Dietrich, A circuit set characterization of antimatroids (1987)

The feasible sets of a set of ERCs

def OptimalityTheory.ERC.IsFeasible {n : ℕ} (E : Set (ERC (Fin n))) (S : Set (Fin n)) : Prop

A set of constraints is feasible for a set of ERCs when it is the set of the top k constraints of a ranking that satisfies all of them.

Equations

• OptimalityTheory.ERC.IsFeasible E S = ∃ (r : OptimalityTheory.Ranking (Fin n) n), (∀ α ∈ E, OptimalityTheory.ERC.SatisfiedBy r α) ∧ ∃ (k : Fin (n + 1)), ↑(r.take k) = S

theorem OptimalityTheory.ERC.isFeasible_take {n : ℕ} {E : Set (ERC (Fin n))} {r : Ranking (Fin n) n} (hr : ∀ α ∈ E, SatisfiedBy r α) (k : Fin (n + 1)) : IsFeasible E ↑(r.take k)

The top segments of a ranking that satisfies a set of ERCs are feasible for it.

theorem OptimalityTheory.ERC.isFeasible_coe_iff {n : ℕ} (E : Finset (ERC (Fin n))) (S : Finset (Fin n)) : IsFeasible ↑E ↑S ↔ ∃ r ∈ linearExtensions E, ∃ (k : Fin (n + 1)), r.take k = S

For finite sets the feasibility of a set is decided by the linear extensions.

theorem OptimalityTheory.ERC.linearExtensions_nonempty_iff {n : ℕ} (E : Finset (ERC (Fin n))) : (linearExtensions E).Nonempty ↔ ∃ (r : Ranking (Fin n) n), ∀ α ∈ ↑E, SatisfiedBy r α

A finite set of ERCs has a linear extension exactly when some ranking satisfies all of its ERCs.

theorem OptimalityTheory.ERC.IsFeasible.mono {n : ℕ} {E F : Set (ERC (Fin n))} {S : Set (Fin n)} (h : ∀ (r : Ranking (Fin n) n), (∀ α ∈ E, SatisfiedBy r α) → ∀ α ∈ F, SatisfiedBy r α) (hS : IsFeasible E S) : IsFeasible F S

Entailment between sets of ERCs carries over to their feasible sets.

theorem OptimalityTheory.ERC.satisfiedBy_iff_forall_isFeasible_take {n : ℕ} {E : Set (ERC (Fin n))} (r : Ranking (Fin n) n) : (∀ α ∈ E, SatisfiedBy r α) ↔ ∀ (k : Fin (n + 1)), IsFeasible E ↑(r.take k)

A ranking satisfies a set of ERCs exactly when each of its top segments is feasible, since the ranking witnessing the segment through a loser puts a winner of the ERC in it.

theorem OptimalityTheory.ERC.isFeasible_singleton_iff {n : ℕ} {α : ERC (Fin n)} (hα : ∃ (r : Ranking (Fin n) n), SatisfiedBy r α) (S : Finset (Fin n)) : IsFeasible {α} ↑S ↔ (∃ l ∈ S, α l = ERCVal.L) → ∃ w ∈ S, α w = ERCVal.W

A set is feasible for a single satisfiable ERC exactly when it holds a winner of the ERC whenever it holds a loser.

Union closure

theorem OptimalityTheory.ERC.IsFeasible.union {n : ℕ} {E : Set (ERC (Fin n))} {S T : Set (Fin n)} (hS : IsFeasible E S) (hT : IsFeasible E T) : IsFeasible E (S ∪ T)

The feasible sets of a set of ERCs are closed under union. The union of the top segment S of r₁ and the top segment T of r₂ is a top segment of the ranking that lists S in the order of r₁, then the rest of T in the order of r₂, then the remaining constraints in the order of r₁.

The antimatroid of a set of ERCs

def OptimalityTheory.ERC.toAntimatroid {n : ℕ} (E : Set (ERC (Fin n))) (hcons : ∃ (r : Ranking (Fin n) n), ∀ α ∈ E, SatisfiedBy r α) : Antimatroid (Fin n)

The antimatroid of a consistent set of ERCs, whose feasible sets are the top segments of the rankings that satisfy it.

Equations

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

@[simp]

theorem OptimalityTheory.ERC.toAntimatroid_E {n : ℕ} {E : Set (ERC (Fin n))} (hcons : ∃ (r : Ranking (Fin n) n), ∀ α ∈ E, SatisfiedBy r α) : (toAntimatroid E hcons).E = Set.univ

@[simp]

theorem OptimalityTheory.ERC.toAntimatroid_isFeasible {n : ℕ} {E : Set (ERC (Fin n))} {S : Set (Fin n)} (hcons : ∃ (r : Ranking (Fin n) n), ∀ α ∈ E, SatisfiedBy r α) : (toAntimatroid E hcons).IsFeasible S ↔ IsFeasible E S

The simple fragment

When every ERC ranks a single winner over a single loser, or imposes nothing, the ERCs encode a partial order, and the feasible sets are its order ideals: the sets feasible for each ERC alone. In general that intersection is strictly larger.

theorem OptimalityTheory.ERC.isFeasible_iff_forall_singleton_of_simple {n : ℕ} {E : Set (ERC (Fin n))} (hcons : ∃ (r : Ranking (Fin n) n), ∀ α ∈ E, SatisfiedBy r α) (hsimple : ∀ α ∈ E, α.IsSimple ∨ α.IsTrivial) (S : Finset (Fin n)) : IsFeasible E ↑S ↔ ∀ α ∈ E, IsFeasible {α} ↑S

For ERCs that each rank one constraint over one other, a set is feasible exactly when it is feasible for each of them. A set feasible for each is a top segment of the ranking that lists it first and the rest after, each in the order of a ranking satisfying all the ERCs, since each ERC's loser in the set has its unique winner in the set.

theorem OptimalityTheory.ERC.exists_forall_isFeasible_singleton_not_isFeasible : ∃ (E : Finset (ERC (Fin 4))) (S : Finset (Fin 4)), (linearExtensions E).Nonempty ∧ (∀ α ∈ E, IsFeasible {α} ↑S) ∧ ¬IsFeasible ↑E ↑S

In general a set feasible for each of a consistent set of ERCs need not be feasible for all of them: two ERCs over four constraints, each with two winners, admit a set that holds a winner of each ERC whose loser it holds without being a top segment of a ranking satisfying both.

The ERCs of an antimatroid

noncomputable def OptimalityTheory.ERC.ofRootedCircuit {n : ℕ} {A : Antimatroid (Fin n)} (rc : A.RootedCircuit) : ERC (Fin n)

The ERC of a rooted circuit has the other members of its carrier as winners, its root as loser, and the constraints outside the carrier as neutral.

Equations

• OptimalityTheory.ERC.ofRootedCircuit rc k = if k ∈ rc.carrier ∧ k ≠ rc.root then OptimalityTheory.ERCVal.W else if k = rc.root then OptimalityTheory.ERCVal.L else OptimalityTheory.ERCVal.e

noncomputable def OptimalityTheory.ERC.ofAntimatroid {n : ℕ} (A : Antimatroid (Fin n)) : Set (ERC (Fin n))

The ERCs of an antimatroid, one for each of its rooted circuits.

Equations

• OptimalityTheory.ERC.ofAntimatroid A = Set.range OptimalityTheory.ERC.ofRootedCircuit

@[simp]

theorem OptimalityTheory.ERC.ofRootedCircuit_eq_L_iff {n : ℕ} {A : Antimatroid (Fin n)} (rc : A.RootedCircuit) (k : Fin n) : ofRootedCircuit rc k = ERCVal.L ↔ k = rc.root

@[simp]

theorem OptimalityTheory.ERC.ofRootedCircuit_eq_W_iff {n : ℕ} {A : Antimatroid (Fin n)} (rc : A.RootedCircuit) (k : Fin n) : ofRootedCircuit rc k = ERCVal.W ↔ k ∈ rc.carrier ∧ k ≠ rc.root

theorem OptimalityTheory.ERC.ofRootedCircuit_eq_simpleERC {n : ℕ} {A : Antimatroid (Fin n)} (rc : A.RootedCircuit) {w l : Fin n} (hcarrier : rc.carrier = {w, l}) (hroot : rc.root = l) (hwl : w ≠ l) : ofRootedCircuit rc = simpleERC w l

A rooted circuit with two members gives a simple ERC, ranking the other member over the root; larger carriers give ERCs with several winners.

Dietrich's characterization

theorem OptimalityTheory.ERC.satisfiedBy_ofAntimatroid_iff {n : ℕ} {A : Antimatroid (Fin n)} (hE : A.E = Set.univ) (r : Ranking (Fin n) n) : (∀ α ∈ ofAntimatroid A, SatisfiedBy r α) ↔ ∀ (k : Fin (n + 1)), A.IsFeasible ↑(r.take k)

A ranking satisfies the ERCs of an antimatroid exactly when each of its top segments is feasible ([Die87]). Satisfaction gives each next segment by union closure, since a failure would yield a rooted circuit whose root no winner outranks; feasibility of the segment through a root puts one of its winners above it.

The inverse laws

theorem OptimalityTheory.ERC.isFeasible_ofAntimatroid_iff {n : ℕ} {A : Antimatroid (Fin n)} (hE : A.E = Set.univ) (S : Set (Fin n)) : IsFeasible (ofAntimatroid A) S ↔ A.IsFeasible S

The feasible sets of an antimatroid are those of its ERCs. A feasible set extends to a chain of feasible sets, by removal below it and augmentation above it, which is the sequence of top segments of a ranking; that ranking satisfies the ERCs by Dietrich's characterization.

theorem OptimalityTheory.ERC.exists_satisfiedBy_ofAntimatroid {n : ℕ} {A : Antimatroid (Fin n)} (hE : A.E = Set.univ) : ∃ (r : Ranking (Fin n) n), ∀ α ∈ ofAntimatroid A, SatisfiedBy r α

The ERCs of an antimatroid are consistent.

theorem OptimalityTheory.ERC.toAntimatroid_ofAntimatroid {n : ℕ} {A : Antimatroid (Fin n)} (hE : A.E = Set.univ) : toAntimatroid (ofAntimatroid A) ⋯ = A

An antimatroid is the antimatroid of its ERCs.

theorem OptimalityTheory.ERC.satisfiedBy_ofAntimatroid_toAntimatroid_iff {n : ℕ} {E : Set (ERC (Fin n))} (hcons : ∃ (r : Ranking (Fin n) n), ∀ α ∈ E, SatisfiedBy r α) (r : Ranking (Fin n) n) : (∀ α ∈ ofAntimatroid (toAntimatroid E hcons), SatisfiedBy r α) ↔ ∀ α ∈ E, SatisfiedBy r α

The ERCs of the antimatroid of E are satisfied by exactly the rankings that satisfy E.

theorem OptimalityTheory.ERC.satisfiedBy_ofAntimatroid_mono {n : ℕ} {A B : Antimatroid (Fin n)} (hA : A.E = Set.univ) (hB : B.E = Set.univ) (h : ∀ (S : Set (Fin n)), A.IsFeasible S → B.IsFeasible S) (r : Ranking (Fin n) n) (hr : ∀ α ∈ ofAntimatroid A, SatisfiedBy r α) (α : ERC (Fin n)) : α ∈ ofAntimatroid B → SatisfiedBy r α

Containment of antimatroids carries over to entailment of their ERCs.