Docs / Phonology / OptimalityTheory / Typology

Languages and typologies

import Linglib.Phonology.OptimalityTheory.Typology · namespace OptimalityTheory.ConstraintSystem

Source

An OT system pairs each input's candidates with a constraint set on input–output mappings (ConstraintSystem). Under a ranking, the winners of every input's tableau form the ranking's language. Following Merchant and Prince, the rankings with the same language form a ranking grammar, and the grammars partition the rankings into the system's typology, the kernel of the language map.

A system with finitely many inputs has the same typology as its joint system. The joint system is a single tableau whose candidates choose a candidate for every input and whose violations are summed over the inputs, the Minkowski sum of the system's tableaux. Prince shows that its language is the product of the languages, so summation loses no ranking information. Magri traces this to the additivity of the lexicographic order, under which minimizing a sum over a product of candidate sets minimizes each summand (Finset.mem_argmin_piFinset_sum).

Main definitions

Main results

References

Declarations

The language of a ranking assigns each input the winners of its tableau (Merchant & Prince 2022).

def languageL63–65
{I : Type u_1} {O : Type u_2} {ι : Type u_3} {n : ℕ} (S : ConstraintSystem I O ι) (r : Ranking ι n) (i : I) :
Finset O

Built from

Used by typology, typology_iff, language_eq_singleton_iff, language_nonempty, language_nonempty_iff, con_eq_of_mem_language, mem_language_iff_of_mem, language_joint

Used in Phonology/HarmonicGrammar/Expressivity, Phonology/OptimalityTheory/PartiallyOrderedConstraints, ItoMester2019, MerchantPrince2022, Stojkovic2026

A ranking selects o alone at an input iff o is a candidate whose violations, read in rank order, are lexicographically below every other candidate's.

theorem language_eq_singleton_iffL76–80
{I : Type u_1} {O : Type u_2} {ι : Type u_3} {n : ℕ} {S : ConstraintSystem I O ι} {r : Ranking ι n} {i : I} {o : O} :
S.language r i = {o} ↔ o ∈ S.gen i ∧ ∀ o' ∈ S.gen i, o' ≠ o → (toLex fun (k : Fin n) => S.con (r k) (i, o)) < toLex fun (k : Fin n) => S.con (r k) (i, o')

Built from