Stratal Optimality Theory

@cite{kiparsky-2000}

Stratal OT is a theory of the phonology-morphology interface where phonological computation is cyclic: it applies at multiple levels (strata) of morphological structure, with the output of each stratum feeding the next as input.

Architecture

The derivation proceeds through ordered strata:

Stem → Word → Phrase

Each stratum has:

1. A constraint ranking (which may differ from other strata)
2. A GEN function (producing candidates from the previous output)
3. An EVAL function (selecting the optimal candidate)

The crucial property is constraint reranking: the same constraint can occupy different positions in different strata's rankings. This captures level-ordering effects — e.g., compensatory lengthening is optimal at the Word level but not at the Phrase level — without ad hoc rules or extrinsic ordering.

Connection to Linglib

Each individual stratum is evaluated using Core.OT.buildTableau and OTTableau.optimal. This module adds the stratal architecture: strata ordering, cross-stratal chaining, and reranking specification.

The Telugu weak alternation (@cite{aitha-2026}) is a key application: the interaction of IDENT-STRESS with FT-BIN across Stem, Word, and Phrase strata derives the -am/-āni alternation from a single underlying form.

inductive Theories.Phonology.StratalOT.Stratum : Type

The three phonological strata of Stratal OT (@cite{kiparsky-2000}).

Stratum	Domain	Morphological boundary
Stem	Root + derivational mfx	Innermost cycle
Word	Stem + inflectional sfx	Prosodic word (PrWd) edge
Phrase	Words + clitics + P	Phonological phrase edge

Each stratum corresponds to a morphological domain. The Stem–Word boundary typically aligns with the edge of the prosodic word.

• stem : Stratum
• word : Stratum
• phrase : Stratum

instance Theories.Phonology.StratalOT.instDecidableEqStratum : DecidableEq Stratum

Equations

• Theories.Phonology.StratalOT.instDecidableEqStratum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Phonology.StratalOT.instBEqStratum : BEq Stratum

Equations

• Theories.Phonology.StratalOT.instBEqStratum = { beq := Theories.Phonology.StratalOT.instBEqStratum.beq }

def Theories.Phonology.StratalOT.instBEqStratum.beq : Stratum → Stratum → Bool

Equations

• Theories.Phonology.StratalOT.instBEqStratum.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.StratalOT.instReprStratum : Repr Stratum

Equations

• Theories.Phonology.StratalOT.instReprStratum = { reprPrec := Theories.Phonology.StratalOT.instReprStratum.repr }

def Theories.Phonology.StratalOT.instReprStratum.repr : Stratum → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Theories.Phonology.StratalOT.Stratum.rank : Stratum → Nat

Strata are linearly ordered: stem < word < phrase. This ordering reflects the direction of morphological derivation (innermost to outermost) and determines the feeding relation.

Equations

• Theories.Phonology.StratalOT.Stratum.stem.rank = 0
• Theories.Phonology.StratalOT.Stratum.word.rank = 1
• Theories.Phonology.StratalOT.Stratum.phrase.rank = 2

instance Theories.Phonology.StratalOT.instLTStratum : LT Stratum

Equations

• Theories.Phonology.StratalOT.instLTStratum = { lt := fun (a b : Theories.Phonology.StratalOT.Stratum) => a.rank < b.rank }

instance Theories.Phonology.StratalOT.instLEStratum : LE Stratum

Equations

• Theories.Phonology.StratalOT.instLEStratum = { le := fun (a b : Theories.Phonology.StratalOT.Stratum) => a.rank ≤ b.rank }

instance Theories.Phonology.StratalOT.instDecidableLtStratum (a b : Stratum) : Decidable (a < b)

Equations

• Theories.Phonology.StratalOT.instDecidableLtStratum a b = inferInstanceAs (Decidable (a.rank < b.rank))

instance Theories.Phonology.StratalOT.instDecidableLeStratum (a b : Stratum) : Decidable (a ≤ b)

Equations

• Theories.Phonology.StratalOT.instDecidableLeStratum a b = inferInstanceAs (Decidable (a.rank ≤ b.rank))

theorem Theories.Phonology.StratalOT.stem_lt_word : Stratum.stem < Stratum.word

theorem Theories.Phonology.StratalOT.word_lt_phrase : Stratum.word < Stratum.phrase

theorem Theories.Phonology.StratalOT.stem_lt_phrase : Stratum.stem < Stratum.phrase

def Theories.Phonology.StratalOT.evalStratum {C : Type} [DecidableEq C] (_stratum : Stratum) (candidates : List C) (ranking : List (Core.OT.NamedConstraint C)) (h : candidates ≠ []) : List C

Evaluate a single stratum: select optimal candidates from a candidate set under a constraint ranking.

Thin wrapper around buildTableau + optimal that labels the evaluation with its stratum.

Equations

• Theories.Phonology.StratalOT.evalStratum _stratum candidates ranking h = (Core.OT.buildTableau candidates ranking h).optimal

def Theories.Phonology.StratalOT.chainEval {C₁ C₂ : Type} [DecidableEq C₂] (_stratum : Stratum) (s₁Output : C₁) (bridge : C₁ → List C₂) (ranking : List (Core.OT.NamedConstraint C₂)) (hBridge : bridge s₁Output ≠ []) : List C₂

Chain two strata: take the optimal output of stratum s₁, transform it into candidates for stratum s₂ via a bridge function, and evaluate under s₂'s ranking.

The bridge function is language-specific: it adds morphological material from the next layer (e.g., inflectional suffixes at the Word level, postpositions at the Phrase level) and generates candidate representations.

Equations

• Theories.Phonology.StratalOT.chainEval _stratum s₁Output bridge ranking hBridge = (Core.OT.buildTableau (bridge s₁Output) ranking hBridge).optimal

structure Theories.Phonology.StratalOT.StratalDerivation (S W P : Type) : Type

The full derivational history across all three strata. Records the input and output at each level.

Type parameters:

• S: candidate type at the Stem level
• W: candidate type at the Word level
• P: candidate type at the Phrase level

Candidate types differ across strata because GEN produces different representations at each level (e.g., metrical parses at Stem level, segmental modifications at Word level).

• underlyingForm : S

  Underlying representation (input to the Stem stratum).

• stemOutput : S

  Optimal output of the Stem stratum.

• wordOutput : W

  Optimal output of the Word stratum.

• phraseOutput : P

  Optimal output of the Phrase stratum (= surface form).

def Theories.Phonology.StratalOT.StratalDerivation.surface {S W P : Type} (d : StratalDerivation S W P) : P

The surface form is the output of the final (Phrase) stratum.

Equations

• d.surface = d.phraseOutput

structure Theories.Phonology.StratalOT.ConstraintId : Type

A constraint identity: name and family, independent of ranking position. The same ConstraintId can appear at different positions in different strata's rankings — this is the core mechanism of Stratal OT.

Contrast with NamedConstraint, which bundles the identity with an evaluation function (tied to a specific candidate type).

• name : String
• family : Core.OT.ConstraintFamily

instance Theories.Phonology.StratalOT.instDecidableEqConstraintId : DecidableEq ConstraintId

Equations

• Theories.Phonology.StratalOT.instDecidableEqConstraintId = Theories.Phonology.StratalOT.instDecidableEqConstraintId.decEq

def Theories.Phonology.StratalOT.instDecidableEqConstraintId.decEq (x✝ x✝¹ : ConstraintId) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Theories.Phonology.StratalOT.instBEqConstraintId.beq : ConstraintId → ConstraintId → Bool

Equations

• Theories.Phonology.StratalOT.instBEqConstraintId.beq { name := a, family := a_1 } { name := b, family := b_1 } = (a == b && a_1 == b_1)
• Theories.Phonology.StratalOT.instBEqConstraintId.beq x✝¹ x✝ = false

instance Theories.Phonology.StratalOT.instBEqConstraintId : BEq ConstraintId

Equations

• Theories.Phonology.StratalOT.instBEqConstraintId = { beq := Theories.Phonology.StratalOT.instBEqConstraintId.beq }

def Theories.Phonology.StratalOT.instReprConstraintId.repr : ConstraintId → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Theories.Phonology.StratalOT.instReprConstraintId : Repr ConstraintId

Equations

• Theories.Phonology.StratalOT.instReprConstraintId = { reprPrec := Theories.Phonology.StratalOT.instReprConstraintId.repr }

def Theories.Phonology.StratalOT.NamedConstraint.toId {C : Type} (nc : Core.OT.NamedConstraint C) : ConstraintId

Extract the identity from a named constraint.

Equations

• Theories.Phonology.StratalOT.NamedConstraint.toId nc = { name := nc.name, family := nc.family }

def Theories.Phonology.StratalOT.findRank {C : Type} (name : String) (ranking : List (Core.OT.NamedConstraint C)) : Option Nat

Find the rank (position) of a constraint by name within a ranking. Position 0 = highest-ranked. Returns none if the constraint is not active at this stratum.

Equations

• Theories.Phonology.StratalOT.findRank name ranking = Theories.Phonology.StratalOT.findRank.go name ranking 0

def Theories.Phonology.StratalOT.findRank.go {C : Type} (name : String) : List (Core.OT.NamedConstraint C) → Nat → Option Nat

Equations

• Theories.Phonology.StratalOT.findRank.go name [] x✝ = none
• Theories.Phonology.StratalOT.findRank.go name (c :: cs) x✝ = if (c.name == name) = true then some x✝ else Theories.Phonology.StratalOT.findRank.go name cs (x✝ + 1)

def Theories.Phonology.StratalOT.isPromoted {C : Type} (name : String) (r₁ r₂ : List (Core.OT.NamedConstraint C)) : Bool

Is constraint name ranked higher (closer to position 0) in ranking r₁ than in r₂? Captures promotion across strata.

Example: ONSET is promoted from Word to Phrase level in Telugu (@cite{aitha-2026} §5.3), switching from below IDENT-STRESS to above it.

Equations

• One or more equations did not get rendered due to their size.

def Theories.Phonology.StratalOT.isDemoted {C : Type} (name : String) (r₁ r₂ : List (Core.OT.NamedConstraint C)) : Bool

Is constraint name ranked lower in r₁ than in r₂? Captures demotion across strata.

Example: *DIST-0 is demoted from Word to Phrase level in Telugu (@cite{aitha-2026} §5.3), allowing consonant retention at phrase boundaries.

Equations

• Theories.Phonology.StratalOT.isDemoted name r₁ r₂ = Theories.Phonology.StratalOT.isPromoted name r₂ r₁

@[reducible, inline]

abbrev Theories.Phonology.StratalOT.RankingSpec : Type

A Hasse pair (a, b) means constraint a strictly dominates constraint b (a ≫ b). Lists of such pairs specify a partial order on constraints.

For classical OT, the transitive closure must be a total order. For comparative tableaux (@cite{prince-2002}), partial specifications suffice.

Example: the Stem-level ranking in Telugu (@cite{aitha-2026} §5.1) is specified as:

[("FT-BIN(μ)", "PARSE-SYL"), ("PARSE-SYL", "ALL-FT-LEFT")]

Equations

• Theories.Phonology.StratalOT.RankingSpec = List (String × String)

def Theories.Phonology.StratalOT.immediatelyDominates (spec : RankingSpec) (a b : String) : Bool

Does constraint a immediately dominate b in the specification?

Equations

• Theories.Phonology.StratalOT.immediatelyDominates spec a b = List.any spec fun (x : String × String) => match x with | (x, y) => x == a && y == b

def Theories.Phonology.StratalOT.dominates (spec : RankingSpec) (a b : String) : Bool

Does constraint a dominate b (reflexive transitive closure, depth ≤ 3)? Sufficient for the ranking chains encountered in practice (typically 5–8 constraints per stratum).

Equations

• One or more equations did not get rendered due to their size.

def Theories.Phonology.StratalOT.isOutputFeeding (s : Stratum) : Stratum → Bool

Output feeding: the output of stratum s is well-formed input for stratum s+1. This is the fundamental architectural claim of Stratal OT — phonological computation is cyclic, and each cycle can change the representation in ways that feed or bleed processes at the next cycle.

Key empirical consequence (@cite{aitha-2026}): compensatory lengthening is optimal at the Word level (MAX ≫ ALIGN-RIGHT) but not at the Phrase level (constraint reranking), producing different outputs for the same segmental configuration at different strata.

Equations

• Theories.Phonology.StratalOT.isOutputFeeding s Theories.Phonology.StratalOT.Stratum.stem = (s == Theories.Phonology.StratalOT.Stratum.stem)
• Theories.Phonology.StratalOT.isOutputFeeding s Theories.Phonology.StratalOT.Stratum.word = (s == Theories.Phonology.StratalOT.Stratum.stem)
• Theories.Phonology.StratalOT.isOutputFeeding s Theories.Phonology.StratalOT.Stratum.phrase = (s == Theories.Phonology.StratalOT.Stratum.word)

theorem Theories.Phonology.StratalOT.stem_feeds_word : isOutputFeeding Stratum.stem Stratum.word = true

theorem Theories.Phonology.StratalOT.word_feeds_phrase : isOutputFeeding Stratum.word Stratum.phrase = true

theorem Theories.Phonology.StratalOT.stem_not_feeds_phrase : isOutputFeeding Stratum.stem Stratum.phrase = false