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.

Sibling derivational architectures

Stratal OT keeps a derivational architecture (strata) inside an otherwise constraint-based framework. Linglib's siblings:

• Theories/Phonology/Process/LocalRewrite.lean — full extrinsic- ordering derivation via local rewrite rules; the modern subregular characterization grounds these as Input Strictly Local functions (@cite{chandlee-heinz-2018}).
• Core/Constraint/OT/HarmonicSerialism.lean — gradual constraint optimization, no strata.
• Core/Computability/Subregular/Function/ — function-level subregular hierarchy (ISL ⊊ OSL ⊊ Subsequential ⊊ Weakly Deterministic) that classifies what each architecture can express (@cite{aksenova-rawski-graf-heinz-2020}; @cite{meinhardt-mai-bakovic-mccollum-2024}).

Connection to Linglib

Each individual stratum is evaluated using Core.Constraint.OT.mkTableau and Tableau.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 Phonology.Stratal.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

@[implicit_reducible]

instance Phonology.Stratal.instDecidableEqStratum : DecidableEq Stratum

Equations

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

def Phonology.Stratal.instReprStratum.repr : Stratum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Stratal.instReprStratum : Repr Stratum

Equations

• Phonology.Stratal.instReprStratum = { reprPrec := Phonology.Stratal.instReprStratum.repr }

def Phonology.Stratal.Stratum.rank : Stratum → ℕ

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

Equations

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

@[implicit_reducible]

instance Phonology.Stratal.instLinearOrderStratum : LinearOrder Stratum

Equations

• Phonology.Stratal.instLinearOrderStratum = LinearOrder.lift' Phonology.Stratal.Stratum.rank Phonology.Stratal.instLinearOrderStratum._proof_1

def Phonology.Stratal.evalStratum {C : Type u_1} [DecidableEq C] (_stratum : Stratum) (candidates : List C) (ranking : List (Core.Constraint.OT.NamedConstraint C)) (h : candidates ≠ [] := by decide) : Finset C

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

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

Equations

• Phonology.Stratal.evalStratum _stratum candidates ranking h = (Core.Constraint.OT.mkTableau candidates ranking h).optimal

def Phonology.Stratal.chainEval {C₁ : Type u_1} {C₂ : Type u_2} [DecidableEq C₂] (_stratum : Stratum) (s₁Output : C₁) (bridge : C₁ → List C₂) (ranking : List (Core.Constraint.OT.NamedConstraint C₂)) (hBridge : bridge s₁Output ≠ []) : Finset 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

• Phonology.Stratal.chainEval _stratum s₁Output bridge ranking hBridge = (Core.Constraint.OT.mkTableau (bridge s₁Output) ranking hBridge).optimal

structure Phonology.Stratal.StratalDerivation (S : Type u_1) (W : Type u_2) (P : Type u_3) : Type (max (max u_1 u_2) u_3)

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 Phonology.Stratal.StratalDerivation.surface {S : Type u_1} {W : Type u_2} {P : Type u_3} (d : StratalDerivation S W P) : P

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

Equations

• d.surface = d.phraseOutput

structure Phonology.Stratal.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.Constraint.OT.ConstraintFamily

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

Equations

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

@[implicit_reducible]

instance Phonology.Stratal.instDecidableEqConstraintId : DecidableEq ConstraintId

Equations

• Phonology.Stratal.instDecidableEqConstraintId = Phonology.Stratal.instDecidableEqConstraintId.decEq

def Phonology.Stratal.instReprConstraintId.repr : ConstraintId → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Stratal.instReprConstraintId : Repr ConstraintId

Equations

• Phonology.Stratal.instReprConstraintId = { reprPrec := Phonology.Stratal.instReprConstraintId.repr }

def Phonology.Stratal.NamedConstraint.toId {C : Type u_1} (nc : Core.Constraint.OT.NamedConstraint C) : ConstraintId

Extract the identity from a named constraint.

Equations

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

def Phonology.Stratal.findRank {C : Type u_1} (name : String) (ranking : List (Core.Constraint.OT.NamedConstraint C)) : Option ℕ

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

• Phonology.Stratal.findRank name ranking = Phonology.Stratal.findRank.go name ranking 0

def Phonology.Stratal.findRank.go {C : Type u_1} (name : String) : List (Core.Constraint.OT.NamedConstraint C) → ℕ → Option ℕ

Equations

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

def Phonology.Stratal.isPromoted {C : Type u_1} (name : String) (r₁ r₂ : List (Core.Constraint.OT.NamedConstraint C)) : Prop

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

• Phonology.Stratal.isPromoted name r₁ r₂ = match Phonology.Stratal.findRank name r₁, Phonology.Stratal.findRank name r₂ with | some p₁, some p₂ => p₁ < p₂ | x, x_1 => False

@[implicit_reducible]

instance Phonology.Stratal.instDecidableIsPromoted {C : Type u_1} (name : String) (r₁ r₂ : List (Core.Constraint.OT.NamedConstraint C)) : Decidable (isPromoted name r₁ r₂)

Equations

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

def Phonology.Stratal.isDemoted {C : Type u_1} (name : String) (r₁ r₂ : List (Core.Constraint.OT.NamedConstraint C)) : Prop

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

• Phonology.Stratal.isDemoted name r₁ r₂ = Phonology.Stratal.isPromoted name r₂ r₁

@[implicit_reducible]

instance Phonology.Stratal.instDecidableIsDemoted {C : Type u_1} (name : String) (r₁ r₂ : List (Core.Constraint.OT.NamedConstraint C)) : Decidable (isDemoted name r₁ r₂)

Equations

• Phonology.Stratal.instDecidableIsDemoted name r₁ r₂ = id inferInstance

def Phonology.Stratal.isPromotedAcross {C₁ : Type u_1} {C₂ : Type u_2} (name : String) (r₁ : List (Core.Constraint.OT.NamedConstraint C₁)) (r₂ : List (Core.Constraint.OT.NamedConstraint C₂)) : Prop

Cross-stratum promotion: name is ranked higher (closer to 0) in r₁ : List (NamedConstraint C₁) than in r₂ : List (NamedConstraint C₂). Generalises isPromoted to permit different candidate types between strata, which is the typical case in Stratal OT — e.g. Word-stratum candidates carry segmental modifications while Phrase-stratum candidates carry boundary-prosody modifications. The constraint inventory is shared by name, not by candidate type.

Example: ONSET is promoted from Word to Phrase level in Telugu (@cite{aitha-2026} §5.3), even though the Word and Phrase strata score different candidate types.

Equations

• Phonology.Stratal.isPromotedAcross name r₁ r₂ = match Phonology.Stratal.findRank name r₁, Phonology.Stratal.findRank name r₂ with | some p₁, some p₂ => p₁ < p₂ | x, x_1 => False

@[implicit_reducible]

instance Phonology.Stratal.instDecidableIsPromotedAcross {C₁ : Type u_1} {C₂ : Type u_2} (name : String) (r₁ : List (Core.Constraint.OT.NamedConstraint C₁)) (r₂ : List (Core.Constraint.OT.NamedConstraint C₂)) : Decidable (isPromotedAcross name r₁ r₂)

Equations

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

def Phonology.Stratal.isDemotedAcross {C₁ : Type u_1} {C₂ : Type u_2} (name : String) (r₁ : List (Core.Constraint.OT.NamedConstraint C₁)) (r₂ : List (Core.Constraint.OT.NamedConstraint C₂)) : Prop

Cross-stratum demotion. Dual of isPromotedAcross.

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

Equations

• Phonology.Stratal.isDemotedAcross name r₁ r₂ = Phonology.Stratal.isPromotedAcross name r₂ r₁

@[implicit_reducible]

instance Phonology.Stratal.instDecidableIsDemotedAcross {C₁ : Type u_1} {C₂ : Type u_2} (name : String) (r₁ : List (Core.Constraint.OT.NamedConstraint C₁)) (r₂ : List (Core.Constraint.OT.NamedConstraint C₂)) : Decidable (isDemotedAcross name r₁ r₂)

Equations

• Phonology.Stratal.instDecidableIsDemotedAcross name r₁ r₂ = id inferInstance

@[reducible, inline]

abbrev Phonology.Stratal.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

• Phonology.Stratal.RankingSpec = List (String × String)

def Phonology.Stratal.immediatelyDominates (spec : RankingSpec) (a b : String) : Prop

Does constraint a immediately dominate b in the specification?

Equations

• Phonology.Stratal.immediatelyDominates spec a b = ∃ p ∈ spec, p.1 = a ∧ p.2 = b

@[implicit_reducible]

instance Phonology.Stratal.instDecidableImmediatelyDominates (spec : RankingSpec) (a b : String) : Decidable (immediatelyDominates spec a b)

Equations

• Phonology.Stratal.instDecidableImmediatelyDominates spec a b = id inferInstance

def Phonology.Stratal.dominates (spec : RankingSpec) : String → String → Prop

Does constraint a dominate b? Reflexive-transitive closure of immediatelyDominates, decidable on any concrete spec via the Core.Relation.ReflTransGen substrate using the spec's vertex universe as the finite carrier. Captures dominance chains of any length (the previous depth-3 hardcoded version was incomplete for longer chains).

Equations

• Phonology.Stratal.dominates spec = Relation.ReflTransGen (Phonology.Stratal.immediatelyDominates spec)

@[implicit_reducible]

instance Phonology.Stratal.instDecidableDominates (spec : RankingSpec) (a b : String) : Decidable (dominates spec a b)

Equations

• Phonology.Stratal.instDecidableDominates spec a b = Relation.ReflTransGen.decidable_of_finite (Phonology.Stratal.specVerts✝ spec) ⋯ a b

def Phonology.Stratal.isOutputFeeding (s : Stratum) : Stratum → Prop

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

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

@[implicit_reducible]

instance Phonology.Stratal.instDecidableIsOutputFeeding (s t : Stratum) : Decidable (isOutputFeeding s t)

Equations

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

theorem Phonology.Stratal.stem_feeds_word : isOutputFeeding Stratum.stem Stratum.word

theorem Phonology.Stratal.word_feeds_phrase : isOutputFeeding Stratum.word Stratum.phrase

theorem Phonology.Stratal.stem_not_feeds_phrase : ¬isOutputFeeding Stratum.stem Stratum.phrase