Documentation

Linglib.Core.Nominal.ArticleInventory

Article Inventory: Surface Forms → Derived Typology #

@cite{schwarz-2009} @cite{schwarz-2013} @cite{patel-grosz-grosz-2017} @cite{moroney-2021} @cite{jenks-2018}

A language's surface inventory of nominal forms (indefinite article, unique article, anaphoric article, demonstrative, possessive, plus the syncretism between unique and anaphoric forms) is a richer object than the DefMarkingStrategy typology cells of @cite{moroney-2021} or the ArticleType cells of @cite{schwarz-2009}. The latter are derivable from the former.

ArticleInventory is the single source of truth for per-language definiteness data. Per-language strategy/article-type assignments are not stipulated separately — they are computed from the inventory:

Bare nominals are always licensed (every language allows bare nouns at some level — the question is only what readings they admit, which is a matter of the type-shift hierarchy, not the article inventory).

source
structure Core.Nominal.ArticleInventory :
Type

The morphological inventory of nominal forms a language has.

Each field is a Prop recording whether the language has an overt form of the named kind, with a [Decidable] instance field so values are computable. uniqueAnaphoricSyncretism records whether hasUniqueArticle and hasAnaphoricArticle are realized by the same form (English the) or different forms (German weak vs strong). When either article is missing the syncretism flag is uninformative; only (hasUniqueArticle ∧ hasAnaphoricArticle) makes the distinction load-bearing.

  • hasIndefinite : Prop

    An overt indefinite article (English a/an, German ein-).

  • hasUniqueArticle : Prop

    An overt article for uniqueness/situational definites (German weak, English the).

  • hasAnaphoricArticle : Prop

    An overt article for anaphoric/familiarity definites (German strong, English the).

  • uniqueAnaphoricSyncretism : Prop

    If both unique and anaphoric articles exist, are they the same form (English the) or distinct (German weak vs strong)?

  • hasDemonstrative : Prop

    An overt demonstrative paradigm (English this/that; almost universal).

  • hasPossessive : Prop

    An overt possessive paradigm (English my/your, German mein-).

  • decHasIndefinite : Decidable self.hasIndefinite
  • decHasUniqueArticle : Decidable self.hasUniqueArticle
  • decHasAnaphoricArticle : Decidable self.hasAnaphoricArticle
  • decUniqueAnaphoricSyncretism : Decidable self.uniqueAnaphoricSyncretism
  • decHasDemonstrative : Decidable self.hasDemonstrative
  • decHasPossessive : Decidable self.hasPossessive
Instances For
    source
    def Core.Nominal.ArticleInventory.licensesKind {F : Logic.Intensional.Frame} (inv : ArticleInventory) :
    NominalKind F → Prop

    Does this inventory have the surface form needed to realize the given NominalKind constructor? Bare and unique are licensed by availability of the form; anaphoric may be expressed either by a distinct anaphoric article (German strong) or by the syncretic article (English the); demonstratives and possessives need their respective paradigms.

    This is not a grammaticality claim about every NP — it is a claim about morphological availability of the licensing form.

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Core.Nominal.ArticleInventory.decLicensesKind {F : Logic.Intensional.Frame} (inv : ArticleInventory) (k : NominalKind F) :
      Decidable (inv.licensesKind k)
      Equations
      source
      @[simp]
      theorem Core.Nominal.ArticleInventory.licensesKind_bare {F : Logic.Intensional.Frame} (inv : ArticleInventory) (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) :
      inv.licensesKind (NominalKind.bare R)

      Bare nominals are universally licensed by the inventory.

      source
      def Core.Nominal.ArticleInventory.toMarkingStrategy (inv : ArticleInventory) :
      Features.Definiteness.DefMarkingStrategy

      Compute Moroney's 4-cell strategy directly from the inventory bools.

      • both forms, syncretic → .generallyMarked (English the)
      • both forms, distinct → .bipartite (German weak vs strong)
      • only anaphoric form → .markedAnaphoric (Mandarin/Thai dem)
      • only unique form → .generallyMarked (the unique form covers both)
      • neither form → .unmarked (Shan, Serbian, Kannada bare)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Core.Nominal.ArticleInventory.toArticleType (inv : ArticleInventory) :
        Features.Definiteness.ArticleType

        Derived classification into the Schwarz/Patel-Grosz–Grosz 3-cell ArticleType typology. Lossy: collapses .generallyMarked and .markedAnaphoric to .weakOnly, as Features.Definiteness strategyToArticleType already documents.

        Equations
        Instances For
          source
          theorem Core.Nominal.ArticleInventory.toArticleType_eq_strategyToArticleType (inv : ArticleInventory) :
          inv.toArticleType = Features.Definiteness.strategyToArticleType inv.toMarkingStrategy

          The inventory-derived ArticleType agrees with the strategyToArticleType collapse of the inventory-derived strategy. By definition.