Evidentials

An evidential is an exponent together with the information sources it covers. Following Aikhenvald, information source is carved into six semantic parameters, numbered I to VI: visual, non-visual sensory, inference, assumption, hearsay and quotative. Willett's three types of evidence, attested, inferring and reported, group them in pairs. A language's inventory is a List Evidential in its Fragment, well formed when its terms are pairwise disjoint.

Implementation notes

The six parameters are Aikhenvald's recurrent terms and nothing finer: no spoken language has an evidential for smell, taste or touch alone, and general knowledge is a meaning an assumed evidential may carry, often cast in the visual, rather than a parameter. A term whose source lies outside the six, such as the Kashaya performative for the speaker's own act, covers none of them. A term covers every parameter its source takes in, so a reported evidential with no quotative beside it covers quotation as well as hearsay. Lexical and parenthetical means are evidentiality strategies, not evidentials, and an inventory records none.

Main definitions

• Evidential.Parameter — the six semantic parameters of information source, in order.
• Evidential.EvidenceType, Parameter.evidenceType, EvidenceType.block — Willett's three types of evidence, the type of a parameter and the parameters of a type.
• Evidential — the lexical entry; Evidential.covers its information sources.
• Evidential.IsOfType, evidenceType? — the type of evidence a term lies within, and IsDirect, IsInferential, IsReportative, the kinds of term within one type.
• Evidential.WellFormed, Evidential.expressed — a paradigm's disjointness and its span.

References

• [Aik04]
• [Wil88]

inductive Evidential.Parameter : Type

The six recurrent semantic parameters of information source.

• visual : Parameter

  Information acquired through seeing.

• sensory : Parameter

  Information acquired through hearing, typically extended to smell and taste and sometimes to touch.

• inference : Parameter

  Inference from visible or tangible evidence or result.

• assumption : Parameter

  Assumption from evidence other than visible results, such as reasoning or general knowledge.

• hearsay : Parameter

  Reported information with no reference to its source.

• quotative : Parameter

  Reported information with overt reference to the quoted source.

@[instance_reducible]

instance Evidential.instDecidableEqParameter : DecidableEq Parameter

Equations

• Evidential.instDecidableEqParameter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Evidential.instReprParameter.repr : Parameter → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Evidential.instReprParameter : Repr Parameter

Equations

• Evidential.instReprParameter = { reprPrec := Evidential.instReprParameter.repr }

@[instance_reducible]

instance Evidential.instFintypeParameter : Fintype Parameter

Equations

• Evidential.instFintypeParameter = { elems := { val := ↑Evidential.Parameter.enumList, nodup := Evidential.Parameter.enumList_nodup }, complete := Evidential.instFintypeParameter._proof_1 }

@[instance_reducible]

instance Evidential.instLinearOrderParameter : LinearOrder Parameter

The parameters in Aikhenvald's order, from visual evidence to quotation.

Equations

• Evidential.instLinearOrderParameter = LinearOrder.lift' Evidential.Parameter.ctorIdx Evidential.instLinearOrderParameter._proof_1

@[instance_reducible]

instance Evidential.instLocallyFiniteOrderParameter : LocallyFiniteOrder Parameter

Equations

• Evidential.instLocallyFiniteOrderParameter = Fintype.toLocallyFiniteOrder

inductive Evidential.EvidenceType : Type

Willett's three types of evidence.

• attested : EvidenceType

  Evidence attested by the speaker's own senses.

• reported : EvidenceType

  Evidence reported to the speaker, at second or third hand or as folklore.

• inferring : EvidenceType

  Evidence inferred from results or by reasoning.

@[instance_reducible]

instance Evidential.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

• Evidential.instDecidableEqEvidenceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Evidential.instReprEvidenceType.repr : EvidenceType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Evidential.instReprEvidenceType : Repr EvidenceType

Equations

• Evidential.instReprEvidenceType = { reprPrec := Evidential.instReprEvidenceType.repr }

def Evidential.Parameter.evidenceType : Parameter → EvidenceType

Each parameter falls under a type of evidence, Willett's types grouping the six parameters in pairs.

Equations

• Evidential.Parameter.visual.evidenceType = Evidential.EvidenceType.attested
• Evidential.Parameter.sensory.evidenceType = Evidential.EvidenceType.attested
• Evidential.Parameter.inference.evidenceType = Evidential.EvidenceType.inferring
• Evidential.Parameter.assumption.evidenceType = Evidential.EvidenceType.inferring
• Evidential.Parameter.hearsay.evidenceType = Evidential.EvidenceType.reported
• Evidential.Parameter.quotative.evidenceType = Evidential.EvidenceType.reported

def Evidential.EvidenceType.block (t : EvidenceType) : Finset Parameter

The block of a type of evidence is the set of parameters falling under it.

Equations

• t.block = {x : Evidential.Parameter | x.evidenceType = t}

structure Evidential : Type

An evidential is an exponent with the information sources it covers.

• morphs : List Morphology.Morph

  The exponent, in surface order.

• covers : Finset Parameter

  The semantic parameters the term covers; a term for a source outside the six covers none.

@[instance_reducible]

instance instDecidableEqEvidential : DecidableEq Evidential

Equations

• instDecidableEqEvidential = instDecidableEqEvidential.decEq

def instDecidableEqEvidential.decEq (x✝ x✝¹ : Evidential) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqEvidential.decEq { morphs := a, covers := a_1 } { morphs := b, covers := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Evidential.IsOfType (e : Evidential) (t : EvidenceType) : Prop

A term is of a type of evidence when its coverage lies within that type's block.

Equations

• e.IsOfType t = (e.covers.Nonempty ∧ e.covers ⊆ t.block)

@[instance_reducible]

instance Evidential.instDecidableIsOfType (e : Evidential) (t : EvidenceType) : Decidable (e.IsOfType t)

Equations

• e.instDecidableIsOfType t = { decide := decide e.covers.Nonempty && decide (e.covers ⊆ t.block), reflects_decide := ⋯ }

@[reducible, inline]

abbrev Evidential.IsDirect (e : Evidential) : Prop

A direct evidential covers firsthand evidence only.

Equations

• e.IsDirect = e.IsOfType Evidential.EvidenceType.attested

@[reducible, inline]

abbrev Evidential.IsInferential (e : Evidential) : Prop

An inferential evidential covers inference or assumption only.

Equations

• e.IsInferential = e.IsOfType Evidential.EvidenceType.inferring

@[reducible, inline]

abbrev Evidential.IsReportative (e : Evidential) : Prop

A reportative evidential covers hearsay or quotation only.

Equations

• e.IsReportative = e.IsOfType Evidential.EvidenceType.reported

def Evidential.evidenceType? (e : Evidential) : Option EvidenceType

The type of evidence of an evidential, when its coverage lies within one of Willett's types; a non-firsthand term has none.

Equations

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

def Evidential.expressed (es : List Evidential) : Finset Parameter

The parameters an inventory expresses.

Equations

• Evidential.expressed es = (List.map Evidential.covers es).toFinset.sup id

def Evidential.WellFormed (es : List Evidential) : Prop

An inventory is well formed when its terms are pairwise disjoint, so that no parameter is covered twice; two entries with the same nonempty coverage count as one term covered twice.

Equations

• Evidential.WellFormed es = List.Pairwise (fun (a b : Evidential) => Disjoint a.covers b.covers) es

@[instance_reducible]

instance Evidential.instDecidablePredListWellFormed : DecidablePred WellFormed

Equations

• Evidential.instDecidablePredListWellFormed es = Evidential.instDecidablePredListWellFormed._aux_1 es