OT grammars: the leg-set / ERC-set / antimatroid hub

In Optimality Theory the linguistically fundamental object is not a single ranking but a grammar: the set of all rankings ("legs") that yield the same optima ([Pri02]; [PS93]). A grammar has three equivalent faces ([MR16]): a leg set (the satisfying rankings), an ERC set (its ranking conditions), and an antimatroid. This file makes the grammar a first-class type, taking the leg set as its canonical identity and exhibiting the other two faces as views.

Taking the leg set as identity makes grammar equality decidable and dissolves the "up to entailment" hedge that the ERC-set presentation carries: two consistent ERC sets present the same grammar exactly when they are mutually entailing (Grammar.ofERCSet_eq_iff_entails), because they then have the same legs. The transitive-reduction ambiguity that forces [MR16] Theorem 2 to be stated up to logical equivalence becomes literal Grammar equality here.

The antimatroid face (Grammar.toAntimatroid) is a one-directional view: every grammar is an antimatroid, but the converse — that every antimatroid is some grammar's — rests on [Die87]'s rooted-circuit characterization and is carried as honest sorrys in OptimalityTheory.Antimatroid (Antimat_RCErc_inv, RCErc_Antimat_inv). The feasible family is read directly off the legs and is independent of the presenting ERC set, since MChain depends only on the satisfying rankings.

Main definitions

• Grammar n — a realizable leg set: a Finset (Ranking n) equal to the linear extensions of some consistent ERC set.
• Grammar.ofERCSet — the canonical grammar of a consistent ERC set (the ERC face, as a constructor).
• Grammar.feasible / Grammar.toAntimatroid — the antimatroid face.

Main results

• Grammar.ofERCSet_eq_iff_entails — two consistent ERC sets present the same grammar iff they are mutually entailing (the entailment quotient dissolves).
• Grammar.feasible_ofERCSet — the antimatroid family of ofERCSet E is MChain E.
• Grammar.toAntimatroid_isFeasible — the antimatroid face's feasible sets are exactly the prefixes of the grammar's legs.

Categorical structure

All the structure here is the order-theoretic specialization of category theory — the categories are thin (posetal), not monoidal. (Set (Ranking n), ⊆) and (Set (ERC n), ⊆) are thin categories; subset_models_iff exhibits conditions and models as a (dual) adjunction between them. The induced monad grammarClosure = models ∘ conditions is the idempotent closure monad, and its algebras — the closed objects (IsGrammarClosed) — are exactly the grammars: a reflective subcategory of ranking-space with grammarClosure as the reflector. On Grammar n itself this lands as a PartialOrder (the specificity = entailment order, ofERCSet_le_iff_entails) with a terminal object (OrderTop, the trivial grammar) and binary coproducts (superGrammar, the super-grammar join, with universal property superGrammar_le). Binary products (meets) may be empty, so the full complete lattice lives on the closed sets, not on Grammar.

References

• [MR16]
• [Pri02]
• [PS93]

The grammar–condition Galois connection

The leg-set / ERC-set duality is the antitone Galois connection — the formal-concept "polarity" ([MR16]; the framing is Birkhoff / Ganter–Wille) — induced by the satisfaction relation on Ord(S.Con) × ERC. models A collects the rankings satisfying every condition in A; conditions R collects the conditions satisfied by every ranking in R. Grammars are exactly the closed sets models (conditions R), the extents of this context.

def OptimalityTheory.models {n : ℕ} (A : Set (ERC n)) : Set (Ranking n)

The rankings satisfying every condition in A (the extent polarity).

Equations

• OptimalityTheory.models A = {r : OptimalityTheory.Ranking n | ∀ α ∈ A, OptimalityTheory.ERC.SatisfiedBy r α}

def OptimalityTheory.conditions {n : ℕ} (R : Set (Ranking n)) : Set (ERC n)

The conditions satisfied by every ranking in R (the intent polarity).

Equations

• OptimalityTheory.conditions R = {α : OptimalityTheory.ERC n | ∀ r ∈ R, OptimalityTheory.ERC.SatisfiedBy r α}

@[simp]

theorem OptimalityTheory.mem_models {n : ℕ} {A : Set (ERC n)} {r : Ranking n} : r ∈ models A ↔ ∀ α ∈ A, ERC.SatisfiedBy r α

@[simp]

theorem OptimalityTheory.mem_conditions {n : ℕ} {R : Set (Ranking n)} {α : ERC n} : α ∈ conditions R ↔ ∀ r ∈ R, ERC.SatisfiedBy r α

theorem OptimalityTheory.subset_models_iff {n : ℕ} {A : Set (ERC n)} {R : Set (Ranking n)} : R ⊆ models A ↔ A ⊆ conditions R

The grammar–condition Galois connection. R ⊆ models A ↔ A ⊆ conditions R: both sides say every ranking in R satisfies every condition in A.

theorem OptimalityTheory.models_antitone {n : ℕ} : Antitone models

theorem OptimalityTheory.conditions_antitone {n : ℕ} : Antitone conditions

def OptimalityTheory.grammarClosure {n : ℕ} (R : Set (Ranking n)) : Set (Ranking n)

The closure operator on ranking-space — the reflector onto the grammars, i.e. the idempotent monad models ∘ conditions induced by the Galois adjunction. Its fixed points (the algebras / closed objects) are exactly the grammars.

Equations

• OptimalityTheory.grammarClosure R = OptimalityTheory.models (OptimalityTheory.conditions R)

theorem OptimalityTheory.subset_grammarClosure {n : ℕ} (R : Set (Ranking n)) : R ⊆ grammarClosure R

theorem OptimalityTheory.grammarClosure_mono {n : ℕ} : Monotone grammarClosure

theorem OptimalityTheory.conditions_grammarClosure {n : ℕ} (R : Set (Ranking n)) : conditions (grammarClosure R) = conditions R

theorem OptimalityTheory.grammarClosure_idem {n : ℕ} (R : Set (Ranking n)) : grammarClosure (grammarClosure R) = grammarClosure R

def OptimalityTheory.IsGrammarClosed {n : ℕ} (R : Set (Ranking n)) : Prop

A ranking-set is grammar-closed iff it equals its closure — iff it is the models of some condition set. These are the closure monad's algebras (the closed objects of the reflective subcategory), exactly the leg sets of grammars (Grammar.coe_legs_isGrammarClosed, Grammar.exists_grammar_of_isGrammarClosed).

Equations

• OptimalityTheory.IsGrammarClosed R = (OptimalityTheory.grammarClosure R = R)

theorem OptimalityTheory.isGrammarClosed_models {n : ℕ} (A : Set (ERC n)) : IsGrammarClosed (models A)

theorem OptimalityTheory.isGrammarClosed_iff_exists_models {n : ℕ} {R : Set (Ranking n)} : IsGrammarClosed R ↔ ∃ (A : Set (ERC n)), R = models A

The closure system: meet and the super-grammar join

The closed sets form a closure system, hence a complete lattice. The meet of two grammars is the intersection of their legs (isGrammarClosed_inter) — conjoin their conditions (models_union). The join is grammarClosure (R ∪ R'), the smallest grammar containing both: the closure of the union of legs. This is the super-grammar that coarsens a typology by unioning grammars; closing the union is exactly what guarantees the result is again a grammar.

theorem OptimalityTheory.models_union {n : ℕ} (A B : Set (ERC n)) : models (A ∪ B) = models A ∩ models B

theorem OptimalityTheory.isGrammarClosed_grammarClosure {n : ℕ} (R : Set (Ranking n)) : IsGrammarClosed (grammarClosure R)

The closure of any set is closed: grammarClosure R is a grammar (the super-grammar generated by R).

theorem OptimalityTheory.isGrammarClosed_inter {n : ℕ} {R R' : Set (Ranking n)} (hR : IsGrammarClosed R) (hR' : IsGrammarClosed R') : IsGrammarClosed (R ∩ R')

Meet. The intersection of two grammars' leg sets is again closed — the greatest grammar contained in both.

theorem OptimalityTheory.coe_linearExtensions_eq_models {n : ℕ} (E : ERCSet n) : ↑E.linearExtensions = models {α : ERC n | α ∈ E}

The coerced linear-extension set of an ERC list is the models of that list's conditions — the bridge from the ERCSet presentation to the Galois polarity.

@[simp]

theorem OptimalityTheory.ERCSet.linearExtensions_nil {n : ℕ} : linearExtensions [] = Finset.univ

The empty ERC set is satisfied by every ranking: its linear extensions are all of Ord(S.Con). This is the trivial grammar (no ranking conditions).

structure OptimalityTheory.Grammar (n : ℕ) : Type

An OT grammar: a set of rankings realizable as the linear extensions of some consistent ERC set ([MR16]). The leg set is the grammar's canonical identity; the ERC-set and antimatroid presentations are views.

• legs : Finset (Ranking n)

  The grammar's legs: the rankings that select its language's optima.

• realizable : ∃ (E : ERCSet n), E.Consistent ∧ self.legs = E.linearExtensions

  Every grammar is the linear-extension set of some consistent ERC set.

theorem OptimalityTheory.Grammar.ext {n : ℕ} {G G' : Grammar n} (h : G.legs = G'.legs) : G = G'

A grammar is determined by its legs: the realizability witness is a Prop, so leg-set equality is grammar equality.

theorem OptimalityTheory.Grammar.ext_iff {n : ℕ} {G G' : Grammar n} : G = G' ↔ G.legs = G'.legs

def OptimalityTheory.Grammar.ofERCSet {n : ℕ} (E : ERCSet n) (hcons : E.Consistent) : Grammar n

The grammar of a consistent ERC set — the ERC face, as a constructor.

Equations

• OptimalityTheory.Grammar.ofERCSet E hcons = { legs := E.linearExtensions, realizable := ⋯ }

@[simp]

theorem OptimalityTheory.Grammar.legs_ofERCSet {n : ℕ} (E : ERCSet n) (hcons : E.Consistent) : (ofERCSet E hcons).legs = E.linearExtensions

@[implicit_reducible]

instance OptimalityTheory.Grammar.instMembershipRanking {n : ℕ} : Membership (Ranking n) (Grammar n)

Membership: r ∈ G means r is one of G's legs.

Equations

• OptimalityTheory.Grammar.instMembershipRanking = { mem := fun (G : OptimalityTheory.Grammar n) (r : OptimalityTheory.Ranking n) => r ∈ G.legs }

@[simp]

theorem OptimalityTheory.Grammar.mem_iff {n : ℕ} {G : Grammar n} {r : Ranking n} : r ∈ G ↔ r ∈ G.legs

@[simp]

theorem OptimalityTheory.Grammar.mem_ofERCSet {n : ℕ} {E : ERCSet n} {hcons : E.Consistent} {r : Ranking n} : r ∈ ofERCSet E hcons ↔ ERCSet.SatisfiedBy r E

theorem OptimalityTheory.Grammar.legs_nonempty {n : ℕ} (G : Grammar n) : G.legs.Nonempty

A grammar has at least one leg: a harmonically-bounded row gives no grammar ([Pri02]).

The ERC face: grammar equality is mutual entailment

theorem OptimalityTheory.Grammar.ofERCSet_eq_iff_entails {n : ℕ} {E E' : ERCSet n} (h : E.Consistent) (h' : E'.Consistent) : ofERCSet E h = ofERCSet E' h' ↔ E.Entails E' ∧ E'.Entails E

The entailment quotient dissolves at the grammar level. Two consistent ERC sets present the same grammar iff they are mutually entailing — iff they have the same legs. This is why the leg set, not the ERC set, is the grammar's identity: the "logically equivalent, not literally equal" hedge of the ERC presentation ([MR16] Theorem 2) becomes literal Grammar equality.

The antimatroid face

def OptimalityTheory.Grammar.feasible {n : ℕ} (G : Grammar n) (S : Set (Fin n)) : Prop

The feasible family of a grammar: the prefixes of its legs. This reads the antimatroid MChain family directly off the legs, independent of any ERC presentation.

Equations

• G.feasible S = ∃ r ∈ G.legs, ∃ (k : Fin (n + 1)), OptimalityTheory.maximalChain r k = S

theorem OptimalityTheory.Grammar.feasible_ofERCSet {n : ℕ} (E : ERCSet n) (hcons : E.Consistent) (S : Set (Fin n)) : (ofERCSet E hcons).feasible S ↔ MChain E S

The feasible family of ofERCSet E is exactly MChain E: the antimatroid face agrees with [MR16]'s Antimat E construction.

theorem OptimalityTheory.Grammar.feasible_eq_mChain {n : ℕ} (G : Grammar n) {E : ERCSet n} (hlegs : G.legs = E.linearExtensions) : G.feasible = MChain E

The feasible family is presentation-independent: it depends only on the legs, so any consistent ERC set realizing G computes it.

def OptimalityTheory.Grammar.toAntimatroid {n : ℕ} (G : Grammar n) : Antimatroid (Fin n)

The antimatroid face of a grammar ([MR16]): ground set the constraints, feasible sets the prefixes of the legs. Every grammar is an antimatroid; the converse rests on [Die87] (Antimat_RCErc_inv). The structure's accessibility and union-closure transfer from any realizing Antimat E via feasible_eq_mChain.

Equations

• G.toAntimatroid = { E := Set.univ, IsFeasible := G.feasible, empty_feasible := ⋯, feasible_sub := ⋯, ground_feasible := ⋯, augmentation := ⋯, removal := ⋯, union_closed := ⋯ }

@[simp]

theorem OptimalityTheory.Grammar.toAntimatroid_isFeasible {n : ℕ} (G : Grammar n) (S : Set (Fin n)) : G.toAntimatroid.IsFeasible S ↔ G.feasible S

theorem OptimalityTheory.Grammar.toAntimatroid_ofERCSet_isFeasible {n : ℕ} (E : ERCSet n) (hcons : E.Consistent) (S : Set (Fin n)) : (ofERCSet E hcons).toAntimatroid.IsFeasible S ↔ (Antimat E hcons).IsFeasible S

The antimatroid face of ofERCSet E has the same feasible sets as Antimat E.

Grammars are exactly the nonempty closed sets

theorem OptimalityTheory.Grammar.coe_legs_isGrammarClosed {n : ℕ} (G : Grammar n) : IsGrammarClosed ↑G.legs

A grammar's legs form a closed set of ranking-space — the extent of its conditions.

theorem OptimalityTheory.Grammar.exists_grammar_of_isGrammarClosed {n : ℕ} {R : Set (Ranking n)} (hcl : IsGrammarClosed R) (hne : R.Nonempty) : ∃ (G : Grammar n), ↑G.legs = R

Conversely, every nonempty grammar-closed set of rankings is some grammar's leg set. With coe_legs_isGrammarClosed, grammars are the nonempty closed sets of the grammar–condition Galois connection.

The specificity order: grammars as a thin category

Grammar n is a poset — a thin category — under leg-set inclusion: G ≤ G' means G is more specific (fewer legs, more ranking conditions). On the ERC face this is exactly the entailment order (ofERCSet_le_iff_entails), the order side of the Galois adjunction. grammarClosure is the reflector onto this subcategory (grammars are its closed objects — the algebras of the idempotent closure monad). The terminal object is the trivial grammar (OrderTop); the coproduct of two grammars is their super-grammar — the closure of the union of legs. Binary products (meets) may be empty, so the full lattice lives on the closed sets, with Grammar n the nonempty part.

@[implicit_reducible]

instance OptimalityTheory.Grammar.instPartialOrder {n : ℕ} : PartialOrder (Grammar n)

Equations

• OptimalityTheory.Grammar.instPartialOrder = { le := fun (G G' : OptimalityTheory.Grammar n) => G.legs ⊆ G'.legs, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem OptimalityTheory.Grammar.le_iff_legs {n : ℕ} {G G' : Grammar n} : G ≤ G' ↔ G.legs ⊆ G'.legs

theorem OptimalityTheory.Grammar.ofERCSet_le_iff_entails {n : ℕ} {E E' : ERCSet n} (h : E.Consistent) (h' : E'.Consistent) : ofERCSet E h ≤ ofERCSet E' h' ↔ E.Entails E'

The specificity order on grammars is the entailment order on their ERC sets — the order side of the grammar–condition Galois adjunction.

def OptimalityTheory.Grammar.trivial {n : ℕ} : Grammar n

The trivial grammar — the terminal object of the specificity order: all rankings, no ranking conditions (ofERCSet []).

Equations

• OptimalityTheory.Grammar.trivial = OptimalityTheory.Grammar.ofERCSet [] ⋯

@[simp]

theorem OptimalityTheory.Grammar.legs_trivial {n : ℕ} : trivial.legs = Finset.univ

@[implicit_reducible]

instance OptimalityTheory.Grammar.instOrderTop {n : ℕ} : OrderTop (Grammar n)

Equations

• OptimalityTheory.Grammar.instOrderTop = { top := OptimalityTheory.Grammar.trivial, le_top := ⋯ }

theorem OptimalityTheory.Grammar.grammarClosure_union_nonempty {n : ℕ} (G G' : Grammar n) : (grammarClosure (↑G.legs ∪ ↑G'.legs)).Nonempty

noncomputable def OptimalityTheory.Grammar.superGrammar {n : ℕ} (G G' : Grammar n) : Grammar n

The super-grammar (the coproduct / join in the thin category of grammars): the least grammar containing both G and G', the closure of the union of their legs. This is [MR16]'s typology coarsening — union the legs, then close to land back inside Grammar.

Equations

• G.superGrammar G' = ⋯.choose

theorem OptimalityTheory.Grammar.coe_superGrammar_legs {n : ℕ} (G G' : Grammar n) : ↑(G.superGrammar G').legs = grammarClosure (↑G.legs ∪ ↑G'.legs)

theorem OptimalityTheory.Grammar.le_superGrammar_left {n : ℕ} (G G' : Grammar n) : G ≤ G.superGrammar G'

theorem OptimalityTheory.Grammar.le_superGrammar_right {n : ℕ} (G G' : Grammar n) : G' ≤ G.superGrammar G'

theorem OptimalityTheory.Grammar.superGrammar_le {n : ℕ} {G G' K : Grammar n} (hG : G ≤ K) (hG' : G' ≤ K) : G.superGrammar G' ≤ K

Universal property of the super-grammar: it is the least grammar above both — the coproduct of G and G' in the thin category of grammars.