Antimatroids

Antimatroids are combinatorial structures that generalize the notion of a partial order. They were first described by [Dil40] in the context of lattice theory and have been rediscovered many times under different names ([Mon85]; see [KLS91] for a comprehensive survey). An antimatroid is uniquely determined by its rooted circuits ([Die87]).

This file develops the framework-agnostic theory; the Optimality-Theory specialization (the ERC–antimatroid isomorphism of [MR16]) lives in Linglib.Phonology.OptimalityTheory.Antimatroid.

[UPSTREAM]: mathlib has Matroid but no Antimatroid/Greedoid. The design mirrors mathlib's Matroid: a bundled structure (not a typeclass) with a Set α ground set and Prop axioms.

Main definitions

• SetSystem — a ground set E with a collection of feasible subsets.
• AccessibleSetSystem — a set system with augmentation and removal.
• Antimatroid — an accessible set system closed under union.
• Antimatroid.Finite — finiteness of the ground set, as an inferable class.
• Antimatroid.free — the free antimatroid on E (every subset feasible).
• Antimatroid.trace — the trace A : S, restricting feasibility to · ∩ S.
• Antimatroid.RootedCircuit — a minimal non-free trace, with a root.

References

[Dil40] — Lattices with unique irreducible decompositions [Mon85] — A use for frequently rediscovering a concept (antimatroids) [Die87] — A circuit set characterization of antimatroids [KLS91] — Greedoids [MR16] — OT grammars, beyond partial orders: ERC sets and antimatroids

Set systems

structure SetSystem (α : Type u_1) : Type u_1

A set system (G, F) is a finite ground set G with a collection F of subsets of G, called feasible sets.

Any subset of a power set is a set system. The feasible sets are the subsets of G that the system "recognizes."

• E : Set α

  The ground set.

• IsFeasible : Set α → Prop

  The feasible set predicate: IsFeasible S means S is a recognized subset of the ground set.

• empty_feasible : self.IsFeasible ∅

  The empty set is always feasible.

• feasible_sub (S : Set α) : self.IsFeasible S → S ⊆ self.E

  Feasible sets are subsets of the ground set.

Accessible set systems

structure AccessibleSetSystem (α : Type u_1) extends SetSystem α : Type u_1

An accessible set system is a set system with augmentation and removal properties. Informally:

• Augmentation: any feasible set that isn't the full ground set can be extended by adding one element to produce another feasible set.
• Removal: any non-empty feasible set can be shrunk by removing one element to produce another feasible set.

The term "accessible" refers to the fact that both the empty set and the ground set are reachable from any feasible set via single-element additions or removals.

[MR16] Definition 3.

• E : Set α
• IsFeasible : Set α → Prop
• empty_feasible : self.IsFeasible ∅
• feasible_sub (S : Set α) : self.IsFeasible S → S ⊆ self.E
• ground_feasible : self.IsFeasible self.E

  The ground set is feasible.

• augmentation (S : Set α) : self.IsFeasible S → S ≠ self.E → ∃ x ∈ self.E, x ∉ S ∧ self.IsFeasible (insert x S)

  Augmentation: every feasible set that is not the ground set can be extended by adding one element from E to produce another feasible set.

• removal (S : Set α) : self.IsFeasible S → S.Nonempty → ∃ x ∈ S, self.IsFeasible (S \ {x})

  Removal: every non-empty feasible set can be shrunk by removing one element to produce another feasible set.

Antimatroids

structure Antimatroid (α : Type u_1) extends AccessibleSetSystem α : Type u_1

An antimatroid is an accessible set system that is closed under union: the union of any two feasible sets is also feasible.

The three defining properties — accessibility (augmentation + removal) and union closure — are what [MR16] prove isomorphic to consistent ERC sets.

The design follows mathlib's Matroid: bundled structure (not a typeclass), Set α ground set, Prop axioms.

[MR16] Definition 5.

• E : Set α
• IsFeasible : Set α → Prop
• empty_feasible : self.IsFeasible ∅
• feasible_sub (S : Set α) : self.IsFeasible S → S ⊆ self.E
• ground_feasible : self.IsFeasible self.E
• augmentation (S : Set α) : self.IsFeasible S → S ≠ self.E → ∃ x ∈ self.E, x ∉ S ∧ self.IsFeasible (insert x S)
• removal (S : Set α) : self.IsFeasible S → S.Nonempty → ∃ x ∈ S, self.IsFeasible (S \ {x})
• union_closed (S T : Set α) : self.IsFeasible S → self.IsFeasible T → self.IsFeasible (S ∪ T)

  Union closure: the union of any two feasible sets is feasible.

  This property distinguishes antimatroids from arbitrary accessible set systems. It corresponds to the fact that consistent ERC sets have "disjunctive" ranking requirements — if two partial rankings are consistent, their union (combining their requirements) is also consistent.

Finiteness

class Antimatroid.Finite {α : Type u_1} (A : Antimatroid α) : Prop

An antimatroid with a finite ground set. Following mathlib's Matroid.Finite, this is a typeclass so it can be inferred.

• ground_finite : A.E.Finite

theorem Antimatroid.ground_finite {α : Type u_1} (A : Antimatroid α) [A.Finite] : A.E.Finite

Basic properties

theorem Antimatroid.ground_isFeasible {α : Type u_1} (A : Antimatroid α) : A.IsFeasible A.E

The ground set of an antimatroid is feasible.

theorem Antimatroid.empty_isFeasible {α : Type u_1} (A : Antimatroid α) : A.IsFeasible ∅

The empty set is feasible in any antimatroid.

theorem Antimatroid.exists_singleton_feasible {α : Type u_1} (A : Antimatroid α) (hne : A.E.Nonempty) : ∃ x ∈ A.E, A.IsFeasible {x}

Singletons in the ground set are feasible in any antimatroid.

Proof: the empty set is feasible and not equal to E (since E contains x), so by augmentation there exists some y ∈ E with {y} feasible. By induction (via removal from larger sets), every singleton is feasible.

For now, we prove only the weaker statement that some singleton exists.

The free antimatroid

def Antimatroid.free {α : Type u_1} (E : Set α) : Antimatroid α

The free antimatroid on a set E: every subset is feasible.

This corresponds to the OT system with no ranking requirements (the empty ERC set) — all n! rankings are consistent. [MR16] Definition 8.

Equations

• Antimatroid.free E = { E := E, IsFeasible := fun (S : Set α) => S ⊆ E, empty_feasible := ⋯, feasible_sub := ⋯, ground_feasible := ⋯, augmentation := ⋯, removal := ⋯, union_closed := ⋯ }

theorem Antimatroid.free_isFeasible {α : Type u_1} (E S : Set α) : (free E).IsFeasible S ↔ S ⊆ E

The free antimatroid on E has IsFeasible S ↔ S ⊆ E.

Traces

def Antimatroid.trace {α : Type u_1} (A : Antimatroid α) (S : Set α) (_hS : S ⊆ A.E) : SetSystem α

The trace of antimatroid A on subset S ⊆ E is the antimatroid (S, {f ∩ S | f ∈ F}) — restricting the feasible sets to their intersections with S.

Traces capture the ordering relations that the original antimatroid places on the constraints in S.

[MR16] Definition 7.

Equations

• A.trace S _hS = { E := S, IsFeasible := fun (T : Set α) => ∃ (F : Set α), A.IsFeasible F ∧ T = F ∩ S, empty_feasible := ⋯, feasible_sub := ⋯ }

Rooted circuits

structure Antimatroid.RootedCircuit {α : Type u_1} (A : Antimatroid α) : Type u_1

A rooted circuit of antimatroid A on S ⊆ E is a trace A : S such that every proper subset of S gives a free trace (no ordering constraints), but A : S itself is not free.

Rooted circuits are the minimal subsets of E that encode actual ranking requirements. Each rooted circuit corresponds to exactly one ERC under the RCErc map.

The root of the circuit is the unique element r ∈ S such that {r} is not feasible in A : S.

[MR16] Definition 9.

• carrier : Set α

  The set defining the circuit.

• carrier_sub : self.carrier ⊆ A.E

  The carrier is a subset of the ground set.

• root : α

  The root element.

• root_mem : self.root ∈ self.carrier

  The root is in the carrier.

• not_free : ¬(A.trace self.carrier ⋯).IsFeasible {self.root}

  The trace on the carrier is not free: {root} is not feasible in the trace.

• proper_free (T : Set α) (hT : T ⊂ self.carrier) (x : α) : x ∈ T → (A.trace T ⋯).IsFeasible {x}

  Every proper subset of the carrier gives a free trace: for every T ⊂ carrier and x ∈ T, the singleton {x} is feasible in the trace A : T.