Documentation

Linglib.Phonology.OptimalityTheory.Stratal

Stratal Optimality Theory #

[Kip00]

Stratal OT is a theory of the phonology–morphology interface where phonological computation is cyclic: it applies at multiple levels (strata) of morphological structure (Stem → Word → Phrase), with the output of each stratum feeding the next as input. The crucial property is constraint reranking: the same constraint can occupy different positions in different strata's rankings, capturing level-ordering effects without ad hoc rules or extrinsic ordering.

Per-stratum evaluation uses OptimalityTheory.Tableau.ofRanking / Tableau.optimal in the consuming study file (e.g. the Telugu weak alternation, [Ait26]). This module provides the cross-stratal vocabulary: a StratalDerivation record of the per-stratum outputs, and the reranking predicates. The latter are cross-stratum because strata typically score different candidate types — the constraint inventory is shared by name, not by candidate type.

Main definitions #

Stratal derivation record #

source
structure OptimalityTheory.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, recording the input and output at each level. Candidate types differ across strata because GEN produces different representations at each level (e.g. metrical parses at the Stem level, segmental modifications at the 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).

Instances For

    Constraint reranking #

    source
    def OptimalityTheory.Stratal.findRank {L : Type u_1} [DecidableEq L] {C : Type u_2} (l : L) (ranking : List (L × Constraints.Constraint C)) :
    Option ℕ

    The rank (position) of the constraint labeled l in a ranking: 0 is the highest rank; none if the constraint is not active at this stratum.

    Equations
    Instances For
      source
      def OptimalityTheory.Stratal.IsPromotedAcross {L : Type u_1} [DecidableEq L] {C₁ : Type u_3} {C₂ : Type u_4} (l : L) (r₁ : List (L × Constraints.Constraint C₁)) (r₂ : List (L × Constraints.Constraint C₂)) :
      Prop

      Cross-stratum promotion: l is ranked higher (closer to 0) in r₁ than in r₂. Different candidate types between strata are permitted — the constraint inventory is shared by label, not by candidate type (e.g. ONSET is promoted from Word to Phrase level in Telugu, [Ait26] §5.3).

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance OptimalityTheory.Stratal.instDecidableIsPromotedAcross {L : Type u_1} [DecidableEq L] {C₁ : Type u_3} {C₂ : Type u_4} (l : L) (r₁ : List (L × Constraints.Constraint C₁)) (r₂ : List (L × Constraints.Constraint C₂)) :
        Decidable (IsPromotedAcross l r₁ r₂)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def OptimalityTheory.Stratal.IsDemotedAcross {L : Type u_1} [DecidableEq L] {C₁ : Type u_3} {C₂ : Type u_4} (l : L) (r₁ : List (L × Constraints.Constraint C₁)) (r₂ : List (L × Constraints.Constraint C₂)) :
        Prop

        Cross-stratum demotion. Dual of IsPromotedAcross (e.g. *DIST-0 is demoted from Word to Phrase level in Telugu, [Ait26] §5.3).

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance OptimalityTheory.Stratal.instDecidableIsDemotedAcross {L : Type u_1} [DecidableEq L] {C₁ : Type u_3} {C₂ : Type u_4} (l : L) (r₁ : List (L × Constraints.Constraint C₁)) (r₂ : List (L × Constraints.Constraint C₂)) :
          Decidable (IsDemotedAcross l r₁ r₂)
          Equations