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 ([MR16b]): 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 have the same linear extensions (Grammar.ofERCs_eq_iff). The transitive-reduction ambiguity that forces [MR16b] Theorem 2 to be stated up to logical equivalence becomes literal Grammar equality here.

The antimatroid face (Grammar.toAntimatroid) has a converse — every full-support antimatroid is some grammar's — by [Die87]'s rooted-circuit characterization (ERC.toAntimatroid_ofAntimatroid, ERC.satisfiedBy_ofAntimatroid_toAntimatroid_iff in OptimalityTheory.Antimatroid). The feasible family is read directly off the legs and is independent of the presenting ERC set, since ERC.IsFeasible depends only on the satisfying rankings.

Main definitions

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

Main results

• Grammar.ofERCs_eq_iff — two consistent ERC sets present the same grammar iff they have the same linear extensions (the entailment quotient dissolves).
• Grammar.feasible_ofERCs — the antimatroid family of ofERCs E is ERC.IsFeasible 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 (Fin n) n), ⊆) and (Set (ERC (Fin 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 order — on the ERC face, definitionally containment of linear-extension sets, i.e. entailment) 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

• [MR16b]
• [Pri02]
• [PS93]

The grammar–condition Galois connection

The leg-set / ERC-set duality is the antitone Galois connection — the formal-concept "polarity" ([MR16b]; 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 (Fin n))) : Set (Ranking (Fin n) n)

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

theorem OptimalityTheory.subset_models_iff {n : ℕ} {A : Set (ERC (Fin n))} {R : Set (Ranking (Fin n) 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 (Fin n) n)) : Set (Ranking (Fin n) 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 (Fin n) n)) : R ⊆ grammarClosure R

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

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

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

def OptimalityTheory.IsGrammarClosed {n : ℕ} (R : Set (Ranking (Fin n) 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 (Fin n))) : IsGrammarClosed (models A)

theorem OptimalityTheory.isGrammarClosed_iff_exists_models {n : ℕ} {R : Set (Ranking (Fin n) n)} : IsGrammarClosed R ↔ ∃ (A : Set (ERC (Fin 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 (Fin n))) : models (A ∪ B) = models A ∩ models B

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

The closure of any set of rankings is closed, so grammarClosure R is a grammar, the super-grammar generated by R.

theorem OptimalityTheory.isGrammarClosed_inter {n : ℕ} {R R' : Set (Ranking (Fin n) 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 : Finset (ERC (Fin n))) : ↑(ERC.linearExtensions E) = models ↑E

The Finset and Set granularities of satisfaction agree: the coerced linear-extension set is the models of the coerced ERC set.

structure OptimalityTheory.Grammar (n : ℕ) : Type

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

• legs : Finset (Ranking (Fin n) n)

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

• realizable : ∃ (E : Finset (ERC (Fin n))), (ERC.linearExtensions E).Nonempty ∧ self.legs = ERC.linearExtensions E

  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, since the realizability witness is a Prop.

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

def OptimalityTheory.Grammar.ofERCs {n : ℕ} (E : Finset (ERC (Fin n))) (hcons : (ERC.linearExtensions E).Nonempty) : Grammar n

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

Equations

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

@[simp]

theorem OptimalityTheory.Grammar.legs_ofERCs {n : ℕ} (E : Finset (ERC (Fin n))) (hcons : (ERC.linearExtensions E).Nonempty) : (ofERCs E hcons).legs = ERC.linearExtensions E

@[instance_reducible]

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

A ranking belongs to a grammar when it is one of its legs.

Equations

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

@[simp]

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

@[simp]

theorem OptimalityTheory.Grammar.mem_ofERCs {n : ℕ} {E : Finset (ERC (Fin n))} {hcons : (ERC.linearExtensions E).Nonempty} {r : Ranking (Fin n) n} : r ∈ ofERCs E hcons ↔ ∀ α ∈ E, ERC.SatisfiedBy r α

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

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

The ERC face: grammar equality is mutual entailment

theorem OptimalityTheory.Grammar.ofERCs_eq_iff {n : ℕ} {E E' : Finset (ERC (Fin n))} (h : (ERC.linearExtensions E).Nonempty) (h' : (ERC.linearExtensions E').Nonempty) : ofERCs E h = ofERCs E' h' ↔ ERC.linearExtensions E = ERC.linearExtensions E'

The entailment quotient dissolves at the grammar level. Two consistent ERC sets present the same grammar iff they have the same linear extensions — iff each entails the other. 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 ([MR16b] 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 consists of the top segments of its legs, read directly off the legs and independent of any ERC presentation.

Equations

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

theorem OptimalityTheory.Grammar.feasible_ofERCs {n : ℕ} (E : Finset (ERC (Fin n))) (hcons : (ERC.linearExtensions E).Nonempty) (S : Set (Fin n)) : (ofERCs E hcons).feasible S ↔ ERC.IsFeasible (↑E) S

The feasible family of ofERCs E is that of E, so the antimatroid face agrees with ERC.toAntimatroid.

theorem OptimalityTheory.Grammar.feasible_eq_isFeasible {n : ℕ} (G : Grammar n) {E : Finset (ERC (Fin n))} (hlegs : G.legs = ERC.linearExtensions E) : G.feasible = ERC.IsFeasible ↑E

The feasible family depends only on the legs, so any consistent ERC set realizing G computes it.

theorem OptimalityTheory.Grammar.exists_antimatroid_feasible_eq {n : ℕ} (G : Grammar n) : ∃ (A : Antimatroid (Fin n)), A.E = Set.univ ∧ A.IsFeasible = G.feasible

The feasible family of a grammar is that of the antimatroid of any ERC set realizing it.

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

The antimatroid face of a grammar ([MR16b]) has the constraints as ground set and the top segments of the legs as feasible sets. Every grammar is an antimatroid, and the converse rests on [Die87] (ERC.toAntimatroid_ofAntimatroid). The axioms transfer from the antimatroid of any ERC set realizing the grammar (exists_antimatroid_feasible_eq).

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_ofERCs_isFeasible {n : ℕ} (E : Finset (ERC (Fin n))) (hcons : (ERC.linearExtensions E).Nonempty) (S : Set (Fin n)) : (ofERCs E hcons).toAntimatroid.IsFeasible S ↔ (ERC.toAntimatroid ↑E ⋯).IsFeasible S

The antimatroid face of ofERCs E has the same feasible sets as the antimatroid of 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 (Fin n) 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 ofERCs E h ≤ ofERCs E' h' is definitionally ERC.linearExtensions E ⊆ ERC.linearExtensions E' — the entailment order, 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.

@[instance_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

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

The trivial grammar has all rankings as legs and no ranking conditions (ofERCs ∅); it is the terminal object of the specificity order.

Equations

• OptimalityTheory.Grammar.trivial = OptimalityTheory.Grammar.ofERCs ∅ ⋯

@[simp]

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

@[instance_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 [MR16b]'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

The super-grammar of G and G' is the least grammar above both, their coproduct in the thin category of grammars.