Documentation

Linglib.Phenomena.Pronouns.ProDropRegistry

Pro-Drop / Overt-PRO Registry @cite{ostrove-2026} #

Coverage registry for the languages currently formalized against @cite{ostrove-2026}'s implicational universal (overt PRO ⇒ non-pro-drop). Each language constructor names a profile defined in a study file; profile : Language → ProDropProfile is the unified endpoint.

The two universal claims — "every formalized language satisfies the universal" and "the forbidden cell stays empty" — are both decide- closed ∀ theorems over the Language enum. Adding a new language fires both proofs at typecheck. If a future formalization placed a language into the overtPROProDrop cell, forbidden_cell_empty would fail and the universal would be falsified by an explicit witness rather than a side observation.

This file is the closest thing in linglib to a "cross-linguistic typological database" for pro-drop / overt-PRO: every entry is verified against the universal by construction.

Coverage (as of writing) #

LanguageSourceCell
English@cite{ostrove-2026}nullPRONoProDrop
SMPM@cite{ostrove-2026}overtPRONoProDrop
Büli@cite{ostrove-2026} via Sulemana 2021overtPRONoProDrop
Gã@cite{allotey-2021}overtPRONoProDrop

The forbidden cell overtPROProDrop has no formalized witness, in agreement with the universal.

WALS F101A bridge (@cite{dryer-2013-wals}) #

F101A.toAllowsProDrop derives a partial allowsProDrop : Option Bool from Dryer's "Expression of Pronominal Subjects" classification (711 languages). The mapping is the standard typological reading:

F101A valueallowsProDrop
obligatoryPronounsInSubjectPositionsome false
subjectAffixesOnVerbsome true
subjectCliticsOnVariableHostsome true
subjectPronounsInDifferentPositionsome true
optionalPronounsInSubjectPositionsome true
mixednone

The classification is lossy: WALS does not record overt PRO (so hasOvertPRO cannot be derived from F101A alone), and the agreement-as-pro-drop reading inflates the pro-drop count for languages whose "subject affixes" are arguably overt pronominal clitics. Gã is exactly such a case: WALS classifies its subject proclitic as a "subject affix" (→ pro-drop), while @cite{allotey-2021} treats it as an overt pronominal clitic that fills subject position (→ non-pro-drop and overt PRO). The disagreement is surfaced as a named theorem (ga_disagrees_with_F101A) rather than papered over.

source
inductive Phenomena.Pronouns.ProDropRegistry.Language :
Type

The languages currently formalized in linglib for the pro-drop / overt-PRO universal. Adding a constructor here requires extending profile and re-fires the two universal theorems by decide.

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.Pronouns.ProDropRegistry.instDecidableEqLanguage :
    DecidableEq Language
    Equations
    source
    @[implicit_reducible]
    instance Phenomena.Pronouns.ProDropRegistry.instReprLanguage :
    Repr Language
    Equations
    source
    def Phenomena.Pronouns.ProDropRegistry.instReprLanguage.repr :
    Language → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.Pronouns.ProDropRegistry.instFintypeLanguage :
      Fintype Language
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Phenomena.Pronouns.ProDropRegistry.profile :
      Language → NullSubject.ProDropProfile

      The unified endpoint: each formalized language's profile, sourced from its study file.

      Equations
      Instances For
        source
        theorem Phenomena.Pronouns.ProDropRegistry.all_satisfy (L : Language) :
        (profile L).Satisfies

        Every language formalized in linglib satisfies @cite{ostrove-2026}'s implicational universal. Closed by cases L <;> decide: case-checks all constructors of Language, decides Satisfies for each profile. Adding a constructor that lands in overtPROProDrop will break this proof at typecheck.

        source
        theorem Phenomena.Pronouns.ProDropRegistry.forbidden_cell_empty (L : Language) :
        (profile L).classify ≠ NullSubject.Typology.overtPROProDrop

        The forbidden cell of @cite{ostrove-2026}'s typology (overtPROProDrop) has no formalized witness. This is the explicit, falsifiable form of the universal: a future language formalization that placed its profile in the forbidden cell would falsify this theorem.

        source
        def Phenomena.Pronouns.ProDropRegistry.cellCount (c : NullSubject.Typology) :
        ℕ

        How many formalized languages fall into a given typological cell.

        Equations
        Instances For
          source
          theorem Phenomena.Pronouns.ProDropRegistry.cellCount_overtPROProDrop_eq_zero :
          cellCount NullSubject.Typology.overtPROProDrop = 0

          The forbidden cell is empty (cardinality form).

          source
          def Phenomena.Pronouns.ProDropRegistry.F101A.toAllowsProDrop :
          Data.WALS.F101A.ExpressionOfPronominalSubjects → Option Bool

          Derived pro-drop classification from a WALS F101A strategy. none means WALS leaves the question open (the mixed cell).

          Equations
          Instances For
            source
            def Phenomena.Pronouns.ProDropRegistry.F101A.allowsProDropOf (walsCode : String) :
            Option Bool

            WALS-derived allowsProDrop for a language by WALS code. none if the language is absent from F101A or its value is mixed.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.Pronouns.ProDropRegistry.walsCodeOf :
              Language → Option String

              A registry language's WALS code, when one exists. SMPM (Chalcatongo Mixtec is the closest WALS proxy but is not the same variety) and Büli are absent from F101A.

              Equations
              Instances For
                source
                theorem Phenomena.Pronouns.ProDropRegistry.english_agrees_with_F101A :
                F101A.allowsProDropOf "eng" = some (profile Language.english).allowsProDrop

                English agrees with WALS F101A: obligatory subject pronouns → allowsProDrop = false, matching the registry profile.

                source
                theorem Phenomena.Pronouns.ProDropRegistry.ga_disagrees_with_F101A :
                F101A.allowsProDropOf "ga" ≠ some (profile Language.ga).allowsProDrop

                Gã disagreement. WALS classifies Gã's subject proclitic as a "subject affix on verb" (→ pro-drop under the standard reading), while @cite{allotey-2021} treats it as an overt pronominal clitic that fills subject position (→ non-pro-drop, overt PRO). The project deliberately surfaces the disagreement rather than papering over it with a fudge in the WALS-bridging direction.

                source
                theorem Phenomena.Pronouns.ProDropRegistry.walsCovered_languages :
                {L : Language | (walsCodeOf L).isSome = true} = {Language.english, Language.ga}

                The two registry languages with WALS F101A coverage are exactly English and Gã (SMPM and Büli are absent).