Stratal Optimality Theory

Stratal OT evaluates phonology cyclically, at successive levels of morphological structure (stem, word, phrase), the output of each level being the input to the next. Each level, or stratum, has its own constraint ranking, and the same constraint can be ranked differently at different strata. A stratum's ranking is its constraint order, a list of labels most dominant first, which OptimalityTheory.Tableau.ofOrder evaluates. One constraint outranks another at a stratum when it comes earlier in the order, [a, b] <+ order, which requires both to be active there.

Main definitions

• OptimalityTheory.Stratal.Reranked: the reversal of a domination between two strata.

References

• [Kip00]

def OptimalityTheory.Stratal.Reranked {L : Type u_1} (a b : L) (r₁ r₂ : List L) : Prop

a and b are reranked between the strata with orders r₁ and r₂ when a outranks b in r₁ and b outranks a in r₂.

Equations

• OptimalityTheory.Stratal.Reranked a b r₁ r₂ = ([a, b].Sublist r₁ ∧ [b, a].Sublist r₂)

@[instance_reducible]

instance OptimalityTheory.Stratal.instDecidableRerankedOfDecidableEq {L : Type u_1} [DecidableEq L] (a b : L) (r₁ r₂ : List L) : Decidable (Reranked a b r₁ r₂)

Equations

• OptimalityTheory.Stratal.instDecidableRerankedOfDecidableEq a b r₁ r₂ = { decide := decide ([a, b].Sublist r₁) && decide ([b, a].Sublist r₂), reflects_decide := ⋯ }