Documentation

Linglib.Features.Indefinite

Indefinite series — feature taxonomy and the word-class-neutral capability #

[Has97]

The indefinite series is cross-categorial: a single series (English some-) spans pronouns (someone, something), determiners (some book), and pro-adverbs (somewhere, somehow, sometime). [Has97]'s cover term "indefinite pronoun" notwithstanding, indefiniteness is not inherently pronominal — the ontological category fixes the member's word class (person/ thing → pronoun, place/manner/time → pro-adverb, determiner → determiner).

This file is therefore word-class-neutral: the [Has97] feature dimensions (function coverage, ontology, morphological basis) and the Indefinite capability ([Indefinite α]) that exposes them over any carrier. The capability is the indefinite analogue of mathlib's MonoidHomClass-over-MonoidHom: a carrier-class-specific indefinite object (IndefinitePronoun in Syntax/Category/Pronoun/Indefinite.lean; a future IndefiniteDeterminer over Semantics.Definiteness's Determiner) supplies one instance : Indefinite That, and generic code reads the series data via [Indefinite α].

Main declarations #

The implicational-map function inventory ([Has97]) #

source
inductive Indefinite.HaspelmathFunction :
Type

The 9 indefinite-series functions on [Has97]'s implicational map. A single form covers a contiguous region of the map.

Instances For
    source
    @[implicit_reducible]
    instance Indefinite.instDecidableEqHaspelmathFunction :
    DecidableEq HaspelmathFunction
    Equations
    source
    @[implicit_reducible]
    instance Indefinite.instReprHaspelmathFunction :
    Repr HaspelmathFunction
    Equations
    source
    def Indefinite.instReprHaspelmathFunction.repr :
    HaspelmathFunction → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Indefinite.instBEqHaspelmathFunction.beq :
      HaspelmathFunction → HaspelmathFunction → Bool
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Indefinite.instBEqHaspelmathFunction :
        BEq HaspelmathFunction
        Equations
        source
        def Indefinite.HaspelmathFunction.all :
        List HaspelmathFunction

        All nine functions, listed in map order.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Indefinite.HaspelmathFunction.adjacent :
          HaspelmathFunction → List HaspelmathFunction

          Adjacency on [Has97]'s implicational map (Fig. 4.4, verified against the book): two-dimensional, with the specificity chain feeding parallel question and conditional tracks.

                                (4) question —— (6) indirect neg —— (7) direct neg
                           |                |
(1) SK — (2) SU — (3) irr <
                           |                |
                      (5) conditional — (8) comparative — (9) free choice

          Edges: 1–2, 2–3, 3–4, 3–5, 4–5, 4–6, 5–8, 6–7, 6–8, 8–9. Note direct negation hangs off indirect negation only, and comparative links conditional, indirect negation, and free choice. Crucial typological claim: any indefinite series covers a contiguous region.

          Equations
          Instances For
            source
            def Indefinite.HaspelmathFunction.isDE :
            HaspelmathFunction → Bool

            Is f a downward-entailing / nonveridical context (the classical NPI-licensing region: question, conditional, indirect/direct negation)? Used by [Chi06]-style polarity-item typologies to predict NPI distribution.

            Equations
            Instances For
              source
              def Indefinite.HaspelmathFunction.isFC :
              HaspelmathFunction → Bool

              Is f a free-choice context (comparative + freeChoice)? Comparative standards are universal-flavored and pattern with FC cross-linguistically ([Has97]).

              Equations
              Instances For
                source
                def Features.LicensingContext.haspelmathFunction :
                LicensingContext → Option Indefinite.HaspelmathFunction

                The [Has97] map function a licensing environment realizes, for the polarity-relevant reading of an indefinite in that environment. Partial: none for environments outside the map's function inventory (the Ladusaw-tradition rows few, atMost, superlative, onlyFocus, tooTo, universalRestrictor, sinceTemporal; also nobody, beforeClause, adversative, whose placement between direct and indirect negation is not verified against the book and is left unmapped). Interpretation-light judgment calls, documented: the modal, imperative, generic, and free-relative rows map to freeChoice — their polarity-relevant realization — although the same environments host plain irrealis uses of non-polarity indefinites; both comparative rows realize the standard-of-comparison function regardless of NPI-licensability (comparativeNP licenses no NPIs, [Hoe83]).

                Equations
                Instances For
                  source
                  def Indefinite.HaspelmathFunction.contexts (f : HaspelmathFunction) :
                  Finset Features.LicensingContext

                  The licensing environments realizing a map function — the preimage of Features.LicensingContext.haspelmathFunction. Empty for the specificity triangle (specificKnown, specificUnknown, irrealis), whose realizations are positive or irrealis clauses outside the licensing-context inventory (matching the Fragment convention that an empty licensingContexts list means the item needs positive contexts).

                  Equations
                  Instances For
                    source
                    def Indefinite.HaspelmathFunction.bfsReachable (funcs : List HaspelmathFunction) (start : HaspelmathFunction) (fuel : ℕ := 10) :
                    List HaspelmathFunction

                    BFS on the implicational map restricted to a given set of functions. Returns the set of nodes reachable from start through edges whose endpoints both lie in funcs.

                    Equations
                    Instances For
                      source
                      def Indefinite.HaspelmathFunction.bfsReachable.go (funcs queue visited : List HaspelmathFunction) (fuel : ℕ) :
                      List HaspelmathFunction
                      Equations
                      Instances For
                        source
                        def Indefinite.HaspelmathFunction.isContiguous (funcs : List HaspelmathFunction) :
                        Bool

                        A list of functions is contiguous on the implicational map iff BFS from any element reaches all others. [Has97]'s key constraint: every indefinite series must cover a contiguous region.

                        Equations
                        Instances For

                          Ontological categories ([Has97] §3.1.3) #

                          source
                          inductive Indefinite.OntologicalCategory :
                          Type

                          The ontological categories of the indefinite series ([Has97] §3.1.3, Table 3.1). The seven core categories — person, thing, property, place, time, manner, amount — are the categories "most often expressed by simple means in the languages of the world"; the human/non-human cut (person vs thing, somebody vs something) is made practically everywhere. The category also fixes the member's word class: person/thing are pronouns, place/time/manner pro-adverbs, determiner ('which', some N) a determiner — reason ('why') is, like determiner, common but non-universal (English and German have no indefinite somewhy).

                          Instances For
                            source
                            @[implicit_reducible]
                            instance Indefinite.instDecidableEqOntologicalCategory :
                            DecidableEq OntologicalCategory
                            Equations
                            source
                            def Indefinite.instReprOntologicalCategory.repr :
                            OntologicalCategory → ℕ → Std.Format
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[implicit_reducible]
                              instance Indefinite.instReprOntologicalCategory :
                              Repr OntologicalCategory
                              Equations
                              source
                              @[implicit_reducible]
                              instance Indefinite.instBEqOntologicalCategory :
                              BEq OntologicalCategory
                              Equations
                              source
                              def Indefinite.instBEqOntologicalCategory.beq :
                              OntologicalCategory → OntologicalCategory → Bool
                              Equations
                              Instances For
                                source
                                def Indefinite.OntologicalCategory.core :
                                List OntologicalCategory

                                The seven core ontological categories realized "practically everywhere" ([Has97] §3.1.3); excludes the non-universal determiner and reason.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def Indefinite.OntologicalCategory.all :
                                  List OntologicalCategory

                                  All nine ontological categories (the seven core plus determiner, reason).

                                  Equations
                                  Instances For

                                    Morphological basis ([Has97]; = WALS F46A categories) #

                                    source
                                    inductive Indefinite.MorphologicalBasis :
                                    Type

                                    [Has97]'s four morphological strategies for deriving indefinite-series forms. Aligns with the four single-strategy values of [DH13b] F46A; F46A's .mixed cell arises only at the paradigm level (see IndefiniteParadigm.toWALS46A, in Typology/Indefinite.lean).

                                    Instances For
                                      source
                                      @[implicit_reducible]
                                      instance Indefinite.instDecidableEqMorphologicalBasis :
                                      DecidableEq MorphologicalBasis
                                      Equations
                                      source
                                      def Indefinite.instReprMorphologicalBasis.repr :
                                      MorphologicalBasis → ℕ → Std.Format
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[implicit_reducible]
                                        instance Indefinite.instReprMorphologicalBasis :
                                        Repr MorphologicalBasis
                                        Equations
                                        source
                                        def Indefinite.instBEqMorphologicalBasis.beq :
                                        MorphologicalBasis → MorphologicalBasis → Bool
                                        Equations
                                        Instances For
                                          source
                                          @[implicit_reducible]
                                          instance Indefinite.instBEqMorphologicalBasis :
                                          BEq MorphologicalBasis
                                          Equations

                                          The capability #

                                          source
                                          class Indefinite (α : Type u_1) :
                                          Type u_1

                                          The indefinite-series capability [Indefinite α]: a carrier α exposing the [Has97] series data — its ontological category, morphological basis, and the contiguous region of the implicational map it covers — over any word-class representation.

                                          Word-class-neutral by design (Indefinite ≠ pronoun): the sole current carrier is Indefinite.IndefinitePronoun (Syntax/Category/Pronoun/Indefinite.lean), but an indefinite determiner (over Semantics.Definiteness's Determiner) or pro-adverb supplies its own instance : Indefinite That and is then read by the same generic [Indefinite α] code. This is the indefinite analogue of mathlib's MonoidHomClass-over-MonoidHom/RingHom.

                                          Instances