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/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

• Indefinite.HaspelmathFunction — the 9 functions on [Has97]'s implicational map, with the map's intrinsic adjacency / contiguity structure.
• Indefinite.OntologicalCategory, Indefinite.MorphologicalBasis — the ontology and derivation-strategy feature dimensions.
• Indefinite — the capability mixin [Indefinite α]: a carrier exposing the indefinite-series feature data (ontology / basis / function-coverage), word-class-neutral.

The implicational-map function inventory ([Has97])

inductive Indefinite.HaspelmathFunction : Type

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

• specificKnown : HaspelmathFunction

  Function 1: Specific known. Speaker has a referent in mind.

• specificUnknown : HaspelmathFunction

  Function 2: Specific unknown. Speaker presupposes a referent but cannot identify it.

• irrealis : HaspelmathFunction

  Function 3: Irrealis non-specific. No specific referent intended.

• question : HaspelmathFunction

  Function 4: Polar / content question.

• conditional : HaspelmathFunction

  Function 5: Conditional protasis.

• comparative : HaspelmathFunction

  Function 6: Standard of comparison.

• indirectNeg : HaspelmathFunction

  Function 7: Indirect (clause-mate) negation.

• directNeg : HaspelmathFunction

  Function 8: Direct negation.

• freeChoice : HaspelmathFunction

  Function 9: Free choice.

@[implicit_reducible]

instance Indefinite.instDecidableEqHaspelmathFunction : DecidableEq HaspelmathFunction

Equations

• Indefinite.instDecidableEqHaspelmathFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Indefinite.instReprHaspelmathFunction : Repr HaspelmathFunction

Equations

• Indefinite.instReprHaspelmathFunction = { reprPrec := Indefinite.instReprHaspelmathFunction.repr }

def Indefinite.instReprHaspelmathFunction.repr : HaspelmathFunction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Indefinite.instBEqHaspelmathFunction : BEq HaspelmathFunction

Equations

• Indefinite.instBEqHaspelmathFunction = { beq := Indefinite.instBEqHaspelmathFunction.beq }

def Indefinite.instBEqHaspelmathFunction.beq : HaspelmathFunction → HaspelmathFunction → Bool

Equations

• Indefinite.instBEqHaspelmathFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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.

def Indefinite.HaspelmathFunction.adjacent : HaspelmathFunction → List HaspelmathFunction

Adjacency on [Has97]'s implicational map.

specKnown — specUnknown — irrealis — question — conditional — indNeg — dirNeg
                                                                          |
                                                freeChoice — comparative —+

Crucial typological claim: any indefinite series covers a contiguous region.

Equations

• Indefinite.HaspelmathFunction.specificKnown.adjacent = [Indefinite.HaspelmathFunction.specificUnknown]
• Indefinite.HaspelmathFunction.specificUnknown.adjacent = [Indefinite.HaspelmathFunction.specificKnown, Indefinite.HaspelmathFunction.irrealis]
• Indefinite.HaspelmathFunction.irrealis.adjacent = [Indefinite.HaspelmathFunction.specificUnknown, Indefinite.HaspelmathFunction.question]
• Indefinite.HaspelmathFunction.question.adjacent = [Indefinite.HaspelmathFunction.irrealis, Indefinite.HaspelmathFunction.conditional]
• Indefinite.HaspelmathFunction.conditional.adjacent = [Indefinite.HaspelmathFunction.question, Indefinite.HaspelmathFunction.indirectNeg]
• Indefinite.HaspelmathFunction.indirectNeg.adjacent = [Indefinite.HaspelmathFunction.conditional, Indefinite.HaspelmathFunction.directNeg]
• Indefinite.HaspelmathFunction.directNeg.adjacent = [Indefinite.HaspelmathFunction.indirectNeg, Indefinite.HaspelmathFunction.comparative]
• Indefinite.HaspelmathFunction.comparative.adjacent = [Indefinite.HaspelmathFunction.directNeg, Indefinite.HaspelmathFunction.freeChoice]
• Indefinite.HaspelmathFunction.freeChoice.adjacent = [Indefinite.HaspelmathFunction.comparative]

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

• Indefinite.HaspelmathFunction.question.isDE = true
• Indefinite.HaspelmathFunction.conditional.isDE = true
• Indefinite.HaspelmathFunction.indirectNeg.isDE = true
• Indefinite.HaspelmathFunction.directNeg.isDE = true
• x✝.isDE = false

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

• Indefinite.HaspelmathFunction.comparative.isFC = true
• Indefinite.HaspelmathFunction.freeChoice.isFC = true
• x✝.isFC = false

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

• Indefinite.HaspelmathFunction.bfsReachable funcs start fuel = Indefinite.HaspelmathFunction.bfsReachable.go funcs [start] [start] fuel

def Indefinite.HaspelmathFunction.bfsReachable.go (funcs queue visited : List HaspelmathFunction) (fuel : ℕ) : List HaspelmathFunction

Equations

• One or more equations did not get rendered due to their size.
• Indefinite.HaspelmathFunction.bfsReachable.go funcs queue visited 0 = visited
• Indefinite.HaspelmathFunction.bfsReachable.go funcs [] visited fuel = visited

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

• Indefinite.HaspelmathFunction.isContiguous [] = true
• Indefinite.HaspelmathFunction.isContiguous (f :: tail) = (f :: tail).all (Indefinite.HaspelmathFunction.bfsReachable (f :: tail) f 15).contains

Ontological categories ([Has97] §3.1.3)

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).

• person : OntologicalCategory

  Person: somebody/someone (interrogative who?).

• thing : OntologicalCategory

  Thing: something (interrogative what?).

• property : OntologicalCategory

  Property / kind: some kind of (interrogative what kind?).

• place : OntologicalCategory

  Place: somewhere (interrogative where?).

• time : OntologicalCategory

  Time: sometime (interrogative when?).

• manner : OntologicalCategory

  Manner: somehow (interrogative how?).

• amount : OntologicalCategory

  Amount: some amount (interrogative how much?).

• determiner : OntologicalCategory

  Determiner: some N / 'which' — non-universal, distinct from the substantival 'who'/'what'.

• reason : OntologicalCategory

  Reason / cause: 'for some reason' (interrogative why?) — non-universal.

@[implicit_reducible]

instance Indefinite.instDecidableEqOntologicalCategory : DecidableEq OntologicalCategory

Equations

• Indefinite.instDecidableEqOntologicalCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Indefinite.instReprOntologicalCategory.repr : OntologicalCategory → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Indefinite.instReprOntologicalCategory : Repr OntologicalCategory

Equations

• Indefinite.instReprOntologicalCategory = { reprPrec := Indefinite.instReprOntologicalCategory.repr }

def Indefinite.instBEqOntologicalCategory.beq : OntologicalCategory → OntologicalCategory → Bool

Equations

• Indefinite.instBEqOntologicalCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Indefinite.instBEqOntologicalCategory : BEq OntologicalCategory

Equations

• Indefinite.instBEqOntologicalCategory = { beq := Indefinite.instBEqOntologicalCategory.beq }

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.

def Indefinite.OntologicalCategory.all : List OntologicalCategory

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

Equations

• Indefinite.OntologicalCategory.all = Indefinite.OntologicalCategory.core ++ [Indefinite.OntologicalCategory.determiner, Indefinite.OntologicalCategory.reason]

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

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).

• interrogative : MorphologicalBasis

  Built from interrogative pronouns (who-, what-, …).

• genericNoun : MorphologicalBasis

  Built from generic nouns ('person', 'thing', 'place').

• special : MorphologicalBasis

  A dedicated indefinite morpheme.

• existentialConstruction : MorphologicalBasis

  An existential predication construction.

@[implicit_reducible]

instance Indefinite.instDecidableEqMorphologicalBasis : DecidableEq MorphologicalBasis

Equations

• Indefinite.instDecidableEqMorphologicalBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Indefinite.instReprMorphologicalBasis.repr : MorphologicalBasis → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Indefinite.instReprMorphologicalBasis : Repr MorphologicalBasis

Equations

• Indefinite.instReprMorphologicalBasis = { reprPrec := Indefinite.instReprMorphologicalBasis.repr }

@[implicit_reducible]

instance Indefinite.instBEqMorphologicalBasis : BEq MorphologicalBasis

Equations

• Indefinite.instBEqMorphologicalBasis = { beq := Indefinite.instBEqMorphologicalBasis.beq }

def Indefinite.instBEqMorphologicalBasis.beq : MorphologicalBasis → MorphologicalBasis → Bool

Equations

• Indefinite.instBEqMorphologicalBasis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

The capability

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/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.

• ontology : α → OntologicalCategory

  The ontological category the carrier realizes (fixes its word class).

• basis : α → MorphologicalBasis

  The morphological derivation strategy.

• functions : α → Finset HaspelmathFunction

  The implicational-map functions the carrier covers.