Documentation

Linglib.Theories.Phonology.ParadigmUniformity.Transderivational

Transderivational Paradigm Uniformity — Benua 1997 #

@cite{benua-1997}

The paradigm-uniformity face of TCT: provides paradigm-typed Corr-style API for OO-Faith constraints between a base form and a derivative form. The asymmetric base-priority discipline lives in OptimalityTheory/TCT.lean (TCTGrammar structure); this file is the compositional face — building 3-role correspondence diagrams over input + base + derivative, and supplying the IDENT-OO and MAX-OO specializations to the (.base, .derivative) edge.

Compared to siblings #

The four ParadigmUniformity files differ only in their anchoring discipline on the same Corr.identViol substrate:

FileAnchoringPolarity
OptimalParadigms.lean (M 2005)Symmetric (no anchor)Positive (Ident)
LexicalConservatism.lean (Steriade 2000)Optional attestation anchorPositive (Ident)
Transderivational.lean (Benua 1997)Base-anchored, recursivePositive (Ident)
Antifaithfulness.lean (Alderete 2001)Symmetric or anchoredNegative (¬Ident)

The architectural distinction of TCT (vs. OP / LC) is not in the constraint or the lift — it is in the evaluation discipline (recursive base-priority), which is captured in TCT.TCTGrammar's type signatures.

source
@[inline]
def Phonology.ParadigmUniformity.Transderivational.Role.formOf {α : Type u_1} (input base derivative : List α) :
TCT.Role → List α

Form lookup helper: select the form for a TCT role from explicit input/base/derivative lists.

Equations
Instances For
    source
    def Phonology.ParadigmUniformity.Transderivational.diagramWithEdge {α : Type} (input base derivative : List α) (ooEdge : Finset (ℕ × ℕ)) (hOO : ∀ p ∈ ooEdge, p.1 < base.length ∧ p.2 < derivative.length) :
    Correspondence.Corr TCT.Role α

    The general TCT diagram constructor: takes the three forms plus an explicit OO correspondence relation ooEdge ⊆ Fin base.length × Fin derivative.length (subject to a well-formedness proof).

    The (.input, .base) and (.input, .derivative) IO edges are filled in trivially as the parallel-pair correspondence (one-to-one up to min length); only the OO edge requires the morphological alignment that a study file specifies.

    This is the load-bearing constructor for paradigmatic phonology studies that involve infixation, truncation, reduplication, or any non-identity morphological mapping — the OO edge is not generally parallel-pair (the singular [ɲĩãr] base maps to non-adjacent positions in the plural [ɲ-ar-ĩãr]). See Phenomena/Phonology/Studies/Benua1997.lean for the canonical Sundanese example.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Phonology.ParadigmUniformity.Transderivational.diagram {α : Type} (input base derivative : List α) :
      Correspondence.Corr TCT.Role α

      The parallel-pair specialization: when the OO edge is the parallel (i, i) correspondence up to min base.length derivative.length. Convenient for cases where base and derivative have no morphological re-alignment (rare in paradigm phonology — most studies need diagramWithEdge with an explicit alignment).

      Defined via Corr.diagram with off-diagonal edge predicate. The pre-Stage-2 version reduced to diagramWithEdge with a hand-rolled parallel-pair edge + length-bounds proof; Corr.diagram makes the pattern direct.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phonology.ParadigmUniformity.Transderivational.identOOViol {α : Type u_1} [DecidableEq α] (c : Correspondence.Corr TCT.Role α) :
        ℕ

        IDENT-OO: featural identity of corresponding base and derivative positions. The load-bearing constraint of @cite{benua-1997}'s misapplication unification — high-ranked IDENT-OO forces overapplication (Sundanese nasal harmony, Ch 3) and underapplication (Tiberian Hebrew spirantization, Ch 4) as duals of one mechanism.

        Equations
        Instances For
          source
          def Phonology.ParadigmUniformity.Transderivational.maxOOViol {α : Type u_1} (c : Correspondence.Corr TCT.Role α) :
          ℕ

          MAX-OO: every base position has a derivative correspondent. Penalizes truncation in the derivative relative to the base.

          Equations
          Instances For
            source
            def Phonology.ParadigmUniformity.Transderivational.depOOViol {α : Type u_1} (c : Correspondence.Corr TCT.Role α) :
            ℕ

            DEP-OO: every derivative position has a base correspondent. Penalizes epenthesis in the derivative relative to the base.

            Equations
            Instances For
              source
              def Phonology.ParadigmUniformity.Transderivational.toIdentOOConstraint (α : Type) [DecidableEq α] :
              Core.Constraint.OT.NamedConstraint (Correspondence.Corr TCT.Role α)

              Wrap IDENT-OO as a NamedConstraint.

              Equations
              Instances For
                source
                def Phonology.ParadigmUniformity.Transderivational.toMaxOOConstraint (α : Type) :
                Core.Constraint.OT.NamedConstraint (Correspondence.Corr TCT.Role α)

                Wrap MAX-OO as a NamedConstraint.

                Equations
                Instances For
                  source
                  def Phonology.ParadigmUniformity.Transderivational.toDepOOConstraint (α : Type) :
                  Core.Constraint.OT.NamedConstraint (Correspondence.Corr TCT.Role α)

                  Wrap DEP-OO as a NamedConstraint.

                  Equations
                  Instances For
                    source
                    theorem Phonology.ParadigmUniformity.Transderivational.identOO_when_equal {α : Type} [DecidableEq α] (input shared : List α) :
                    identOOViol (diagram input shared shared) = 0

                    When the derivative is identical to the base, IDENT-OO is satisfied (zero violations). The "perfect uniformity" baseline — paradigmatic identity is the trivial case where there is nothing to misapply.