Documentation

Studies.MerchantPrince2022

Merchant and Prince (2022): The Mother of All Tableaux #

This file formalizes the bridge from tableaux to grammars in [MP22], which studies the large-scale structure of an optimality-theoretic typology: the partition of the rankings into grammars, the invariant that every violation tableau yielding the typology instantiates, and its geometry. A row of a tableau asserted optimal generates the elementary ranking conditions of its winner–loser comparisons (rowERCs), and the grammar of that row is the grammar of those conditions in the hub of [MR16b] (rowGrammar); its rankings are exactly those under which the row wins by lexicographic optimality after [PS93] (mem_rowGrammar_legs_iff_lex). The typology as the partition of row grammars, the border-point pair, and the invariant itself are not represented.

References #

source
def MerchantPrince2022.rowERCs {C : Type u_1} [DecidableEq C] {n : ℕ} (t : OptimalityTheory.Tableau C n) (w : C) :
Finset (OptimalityTheory.ERC (Fin n))

The ERC set of a tableau row w: w's winner-loser ERCs against every other candidate. These are the ranking conditions a leg must satisfy for w to be the optimum ([Pri02]).

Equations
Instances For
    source
    def MerchantPrince2022.rowGrammar {C : Type u_1} [DecidableEq C] {n : ℕ} (t : OptimalityTheory.Tableau C n) (w : C) (h : (OptimalityTheory.ERC.linearExtensions (rowERCs t w)).Nonempty) :
    OptimalityTheory.Grammar n

    The grammar of a tableau row — the bridge from the Concrete-OT tableau engine to the abstract Grammar hub ([MP22]; [MR16b]). h is the consistency of the row's conditions, i.e. that w is a genuine, non-harmonically-bounded optimum.

    Equations
    Instances For
      source
      @[simp]
      theorem MerchantPrince2022.mem_rowGrammar_legs {C : Type u_1} [DecidableEq C] {n : ℕ} {t : OptimalityTheory.Tableau C n} {w : C} {h : (OptimalityTheory.ERC.linearExtensions (rowERCs t w)).Nonempty} {r : OptimalityTheory.Ranking (Fin n) n} :
      r ∈ (rowGrammar t w h).legs ↔ ∀ α ∈ rowERCs t w, OptimalityTheory.ERC.SatisfiedBy r α
      source
      theorem MerchantPrince2022.mem_rowGrammar_legs_iff_lex {C : Type u_1} [DecidableEq C] {n : ℕ} {t : OptimalityTheory.Tableau C n} {w : C} {h : (OptimalityTheory.ERC.linearExtensions (rowERCs t w)).Nonempty} {r : OptimalityTheory.Ranking (Fin n) n} :
      r ∈ (rowGrammar t w h).legs ↔ ∀ l ∈ t.candidates.erase w, (toLex fun (p : Fin n) => t.profile w (r p)) ≤ toLex fun (p : Fin n) => t.profile l (r p)

      The semantic anchor. A row's grammar collects exactly the rankings under which w's violation profile, read in the ranking's priority order, lexicographically dominates every competitor's — i.e. the rankings that select w as optimum ([PS93]). This connects the abstract Grammar hub back to the tableau's lexicographic evaluation.