Documentation

Linglib.Theories.Phonology.Subregular.OCP

OCP (Obligatory Contour Principle) ↔ TSL_2 — the identity instance #

The OCP @cite{goldsmith-1976} @cite{mccarthy-1986} is the identity-relation instance of the generic forbidden-pair markedness constructor mkForbidPairsOnTier (see ForbidPairs.lean): the forbidden 2-factor is [some x, some x], and the corresponding TSL_2 grammar is TSLGrammar.ofForbiddenPairs (· = ·) p.

Mathematically, the unprojected (single-tier, full-alphabet) case is the linguistic instance of the classical theory of square-free words @cite{thue-1906}: a word is OCP-clean iff it contains no factor x x. Thue's construction shows infinite square-free words exist over a 3-letter alphabet, while every binary string of length ≥ 4 contains a square — i.e. binary tonal alphabets cannot satisfy a strict OCP at length, which is itself a phonological prediction.

Everything in this file is a one-line specialization of the generic forbidden-pair infrastructure to R := (· = ·). The OCP-specific names (ocpForbidden, OCPCleanPair, TSLGrammar.ocp, mkOCPOnTier_zero_iff_in_ocp_lang) are kept as the canonical entry points downstream consumers reference.

OCP-as-prohibition vs OCP-as-merger #

This file formalizes the prohibition reading of the OCP — strings containing adjacent identical (tier-projected) autosegments are rejected by TSLGrammar.ocp p. The classical autosegmental tradition (@cite{goldsmith-1976}) instead reads the OCP as a merger transformation: adjacent identical autosegments are collapsed into a single multiply-linked autosegment. The merger reading is formalized by Phonology.Autosegmental.RegisterTier.mergeTRN (and the underlying FeatureBundle.merge) — a repair operation on representations, not a language predicate. The two readings are operationally distinct, both trace to the same body of literature, and coexist in linglib without a master bridge — the prohibition reading classifies a stringset; the merger reading fixes a representation.

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

Forbidden 2-factors for the OCP: pairs [some x, some x] of two identical non-boundary symbols. The identity-relation specialization of forbiddenPairsSet.

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

    The TSL_2 grammar capturing "no two adjacent identical symbols on the tier defined by p". The identity-relation specialization of TSLGrammar.ofForbiddenPairs.

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

      The OCP relation on Option α: two augmented symbols are OCP-clean as a pair iff they are not both some of the same value. The identity-relation specialization of CleanPair.

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

        The OCP relation is boundary-vacuous (identity-relation instance of CleanPair.isBoundaryVacuous).

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

        Bridge (relational form): a candidate's OCP score is zero iff its raw string projects (under Tier.byClass p) to a list with no two adjacent identical elements. Identity-relation specialization of mkForbidPairsOnTier_zero_iff_isChain.

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

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

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

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