Documentation

Linglib.Semantics.Quantification.Indefinite

The implicational map of indefinite series #

An indefinite series (English some-, Russian -nibud') is used in some of nine functions, which Haspelmath arranges on an implicational map: a graph on the functions whose adjacency requirement says that the functions a series covers form a connected region. The map is implicationalMap, and a region s meets the requirement when (implicationalMap.induce ↑s).Connected, so the book's requirement is a statement of graph theory. The series themselves are IndefinitePronoun.Series.

Main declarations #

Indefinite.HaspelmathFunction: the nine functions, with the book's numbering number and the neighbours adjacent of each on the map.
Indefinite.implicationalMap: the map as a SimpleGraph.
Indefinite.SpecificityFunction: the specific known, specific unknown and non-specific functions in the order the map chains them, with their embedding toFunction in the map and the ones a region covers, specificityFunctions. A set of them is an interval unless it has the two ends without the middle (SpecificityFunction.ordConnected_iff).

Implementation notes #

The empty region is not connected, as SimpleGraph.Connected requires a vertex; a series covers at least one function. The book counts the possible regions of the map differently from the graph encoded here; see the TODO of Studies/Haspelmath1997.lean.

References #

[Has97]

The functions and the map #

inductive Indefinite.HaspelmathFunction :

The nine functions of [Has97]'s implicational map.

specificKnown : HaspelmathFunction
In the specific known function the speaker has a referent in mind.
specificUnknown : HaspelmathFunction
In the specific unknown function the speaker presupposes a referent but cannot identify it.
irrealis : HaspelmathFunction
In the irrealis non-specific function no specific referent is intended.
question : HaspelmathFunction
The indefinite stands in a question.
conditional : HaspelmathFunction
The indefinite stands in the protasis of a conditional.
comparative : HaspelmathFunction
The indefinite stands in the standard of a comparative.
indirectNeg : HaspelmathFunction
Indirect negation is superordinate or implicit negation (without, doubt, deny).
directNeg : HaspelmathFunction
Direct negation is clause-mate negation.
freeChoice : HaspelmathFunction
The indefinite is a free-choice item.

Instances For

@[instance_reducible]

instance Indefinite.instDecidableEqHaspelmathFunction :

DecidableEq HaspelmathFunction

Equations

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

@[instance_reducible]

instance Indefinite.instFintypeHaspelmathFunction :

Fintype HaspelmathFunction

Equations

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

@[instance_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.

Instances For

def Indefinite.HaspelmathFunction.number :

HaspelmathFunction → ℕ

The book's numbering of the functions, in which it states the distribution of a series.

Equations

Instances For

def Indefinite.HaspelmathFunction.adjacent :

HaspelmathFunction → List HaspelmathFunction

adjacent f lists the neighbours of f on the map. The map is a chain from specific known through specific unknown to irrealis, which feeds two parallel tracks, question to indirect negation to direct negation and conditional to comparative to free choice, the tracks joined at question and conditional and at indirect negation and comparative.

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

Equations

Instances For

def Indefinite.implicationalMap :

SimpleGraph HaspelmathFunction

The implicational map is the graph on the functions with the edges of HaspelmathFunction.adjacent.

Equations

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

Instances For

@[instance_reducible]

instance Indefinite.instDecidableRelHaspelmathFunctionAdjImplicationalMap :

DecidableRel implicationalMap.Adj

Equations

Indefinite.instDecidableRelHaspelmathFunctionAdjImplicationalMap f g = { decide := decide (List.elem g f.adjacent = true), reflects_decide := ⋯ }

@[simp]

theorem Indefinite.implicationalMap_adj {f g : HaspelmathFunction} :

implicationalMap.Adj f g ↔ g ∈ f.adjacent

The specificity functions #

inductive Indefinite.SpecificityFunction :

The three functions at the specific end of the map, which differ in whether the indefinite has a specific referent and in whether the speaker can identify it. They are ordered as the map chains them, from specific known through specific unknown to non-specific.

specificKnown : SpecificityFunction
The speaker has the referent in mind.
specificUnknown : SpecificityFunction
The speaker presupposes a referent but cannot identify it.
nonSpecific : SpecificityFunction
No specific referent is intended.

Instances For

@[instance_reducible]

instance Indefinite.instDecidableEqSpecificityFunction :

DecidableEq SpecificityFunction

Equations

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

@[instance_reducible]

instance Indefinite.instFintypeSpecificityFunction :

Fintype SpecificityFunction

Equations

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

def Indefinite.instReprSpecificityFunction.repr :

SpecificityFunction → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Indefinite.instReprSpecificityFunction :

Repr SpecificityFunction

Equations

Indefinite.instReprSpecificityFunction = { reprPrec := Indefinite.instReprSpecificityFunction.repr }

@[instance_reducible]

instance Indefinite.SpecificityFunction.instLinearOrder :

LinearOrder SpecificityFunction

Equations

Indefinite.SpecificityFunction.instLinearOrder = LinearOrder.lift' Indefinite.SpecificityFunction.ctorIdx Indefinite.SpecificityFunction.instLinearOrder._proof_1

theorem Indefinite.SpecificityFunction.ordConnected_iff {s : Set SpecificityFunction} :

s.OrdConnected ↔ specificKnown ∈ s → nonSpecific ∈ s → specificUnknown ∈ s

A set of specificity functions is an interval exactly when it does not have the two ends without the middle.

@[instance_reducible]

instance Indefinite.SpecificityFunction.instDecidableOrdConnectedCoeFinset (s : Finset SpecificityFunction) :

Decidable (↑s).OrdConnected

Equations

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

def Indefinite.SpecificityFunction.toFunction :

SpecificityFunction → HaspelmathFunction

toFunction embeds the specificity functions in the map, the non-specific function as the irrealis one.

Equations

Instances For

theorem Indefinite.SpecificityFunction.toFunction_injective :

Function.Injective toFunction

def Indefinite.specificityFunctions (s : Finset HaspelmathFunction) :

Finset SpecificityFunction

The specificity functions a region of the map covers.

Equations

Indefinite.specificityFunctions s = {x : Indefinite.SpecificityFunction | x.toFunction ∈ s}

Instances For

@[simp]

theorem Indefinite.mem_specificityFunctions {s : Finset HaspelmathFunction} {u : SpecificityFunction} :

u ∈ specificityFunctions s ↔ u.toFunction ∈ s