Documentation

Linglib.Theories.Phonology.Subregular.Agree

AGREE ↔ TSL_2 — the inequality instance (dual of OCP) #

AGREE-style markedness in OT phonology is the non-identity dual of the OCP: tier-adjacent symbols must agree (be equal) rather than differ. As an instance of the generic forbidden-pair constructor mkForbidPairsOnTier (see ForbidPairs.lean), AGREE is the specialization with R := (· ≠ ·), just as the OCP is the R := (· = ·) specialization.

The duality is structural, not metaphorical: the OCP penalizes adjacent identical tier elements (the "no double" rule, forcing dissimilation); AGREE penalizes adjacent distinct tier elements (the "no different" rule, forcing assimilation/harmony). Consonant harmony, vowel harmony, and tone spreading factor through TSLGrammar.agree; dissimilation, anti-geminate, and Meeussen's rule factor through TSLGrammar.ocp. The generic TSLGrammar.ofForbiddenPairs subsumes both — and asymmetric patterns that are neither pure agreement nor pure dissimilation (directional harmony driven by morphological geometry, e.g. Kikongo nasal harmony in Phenomena/Phonology/Studies/RoseWalker2004.lean) instantiate the generic constructor directly with their own asymmetric R.

Everything here is a one-line specialization of the generic forbidden-pair infrastructure to R := (· ≠ ·). The AGREE-specific names (agreeForbidden, AgreeCleanPair, TSLGrammar.agree, mkAgreeOnTier_zero_iff_in_agree_lang) are the canonical entry points downstream consumers reference.

source
def Phonology.Subregular.agreeForbidden (α : Type) [DecidableEq α] :
Set (Core.Computability.Subregular.Augmented α)

Forbidden 2-factors for AGREE: pairs [some x, some y] of two distinct non-boundary symbols. The inequality-relation specialization of forbiddenPairsSet.

Equations
Instances For
    source
    def Phonology.Subregular.TSLGrammar.agree {α : Type} [DecidableEq α] (p : α → Prop) [DecidablePred p] :
    Core.Computability.Subregular.TSLGrammar 2 α

    The TSL_2 grammar capturing "no two adjacent distinct symbols on the tier defined by p" — equivalently, every tier-adjacent pair agrees. The inequality-relation specialization of TSLGrammar.ofForbiddenPairs.

    Equations
    Instances For
      source
      def Phonology.Subregular.AgreeCleanPair {α : Type} [DecidableEq α] :
      Option α → Option α → Prop

      The AGREE relation on Option α: two augmented symbols are AGREE-clean as a pair iff they are not both some of distinct values. The inequality-relation specialization of CleanPair.

      Equations
      Instances For
        source
        theorem Phonology.Subregular.agreeCleanPair_some_some {α : Type} [DecidableEq α] (a b : α) :
        AgreeCleanPair (some a) (some b) ↔ a = b
        source
        theorem Phonology.Subregular.AgreeCleanPair.isBoundaryVacuous {α : Type} [DecidableEq α] :
        Core.Computability.Subregular.IsBoundaryVacuous AgreeCleanPair

        The AGREE relation is boundary-vacuous (inequality-relation instance of CleanPair.isBoundaryVacuous).

        source
        theorem Phonology.Subregular.mkAgreeOnTier_zero_iff_isChain {α : Type} [DecidableEq α] {C : Type} (name : String) (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) :
        (Constraints.mkAgreeOnTier name (Core.Tier.byClass p) extract).eval c = 0 ↔ List.IsChain (fun (a b : α) => ¬a ≠ b) (List.filter (fun (x : α) => decide (p x)) (extract c))

        Bridge (relational form): a candidate's AGREE score is zero iff its raw string projects (under Tier.byClass p) to a list with no two adjacent distinct elements — i.e. all on-tier elements are equal. Inequality-relation specialization of mkForbidPairsOnTier_zero_iff_isChain.

        source
        theorem Phonology.Subregular.mkAgreeOnTier_zero_iff_in_agree_lang {α : Type} [DecidableEq α] {C : Type} (name : String) (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) :
        (Constraints.mkAgreeOnTier name (Core.Tier.byClass p) extract).eval c = 0 ↔ extract c ∈ (TSLGrammar.agree p).lang

        Bridge (full TSL_2 language form): a candidate's AGREE score is zero iff its raw string is in the language of the TSL_2 grammar TSLGrammar.agree p. The two perspectives on AGREE — optimality-theoretic constraint and subregular-complexity class — are co-extensive. Inequality-relation specialization of mkForbidPairsOnTier_zero_iff_in_lang.

        source
        theorem Phonology.Subregular.mkAgreeOnTier_zeroSet_eq {α : Type} [DecidableEq α] (name : String) (p : α → Prop) [DecidablePred p] :
        (Constraints.mkAgreeOnTier name (Core.Tier.byClass p) id).zeroSet = (TSLGrammar.agree p).lang

        Zero-set bridge (AGREE on tier): the Language α-form restatement of mkAgreeOnTier_zero_iff_in_agree_lang (with extract := id). The AGREE markedness constraint's zero-set is the corresponding AGREE-TSL_2 language. Sibling of mkForbidPairsOnTier_zeroSet_eq in OTBound.lean and mkOCPOnTier_zeroSet_eq in OCP.lean.