Documentation

Linglib.Studies.Aikhenvald2004

Aikhenvald (2004): Evidentiality typology #

[Aik04] [dH13b] [Bar84] [Osw86]

This file holds only the analytical disagreements: where [Aik04]'s own paradigm-type letter for a language differs from AikhenvaldSystem.fromInventory applied to the Fragment-declared inventory, or where the resulting classification differs from [dH13b]'s WALS Ch 77 coding.

Per-language Aikhenvald classifications are derived in Typology/Evidentiality.lean; per-language inventories live in Fragments/{Lang}/Evidentiality.lean. There are no per-language verification examples here — those would be unit tests of the derivation algorithm, not theorems about the typology.

Disagreements recorded #

§1: 4 paper-vs-derived disagreements (Turkish, Bulgarian, Abkhaz, Kashaya). Each is an analytical choice about which morphemes count as marked evidentials.
§2: Aikhenvald-vs-WALS disagreements for languages where the two classifications diverge. Three representative cases.

Evidentiality typology (consolidated from the former Typology/Modality + Typology/Evidentiality; single-paper [Aik04] apparatus) #

inductive Aikhenvald2004.EvidentialSystem :

WALS Ch 77: how many evidential distinctions a language grammaticalises. Extends the WALS 3-way classification with a threeOrMore value to distinguish Quechua/Tuyuca-style rich systems from canonical 2-way systems (Turkish/Bulgarian).

noGrammatical : EvidentialSystem
No grammatical evidentials (e.g. English, French, Mandarin).
indirectOnly : EvidentialSystem
Indirect evidential only (e.g. Georgian, West Greenlandic).
directAndIndirect : EvidentialSystem
Two-choice direct vs indirect (e.g. Turkish, Bulgarian, Tibetan, Abkhaz).
threeOrMore : EvidentialSystem
Three or more evidential choices (e.g. Quechua, Tuyuca, Aymara, Tariana).

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instDecidableEqEvidentialSystem :

DecidableEq EvidentialSystem

Equations

Aikhenvald2004.instDecidableEqEvidentialSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aikhenvald2004.instBEqEvidentialSystem.beq :

EvidentialSystem → EvidentialSystem → Bool

Equations

Aikhenvald2004.instBEqEvidentialSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instBEqEvidentialSystem :

BEq EvidentialSystem

Equations

Aikhenvald2004.instBEqEvidentialSystem = { beq := Aikhenvald2004.instBEqEvidentialSystem.beq }

def Aikhenvald2004.instReprEvidentialSystem.repr :

EvidentialSystem → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instReprEvidentialSystem :

Repr EvidentialSystem

Equations

Aikhenvald2004.instReprEvidentialSystem = { reprPrec := Aikhenvald2004.instReprEvidentialSystem.repr }

def Aikhenvald2004.EvidentialSystem.HasEvidentials :

EvidentialSystem → Prop

Whether a language has any grammatical evidential marking.

Equations

Instances For

@[simp]

theorem Aikhenvald2004.EvidentialSystem.hasEvidentials_iff (s : EvidentialSystem) :

s.HasEvidentials ↔ s ≠ noGrammatical

@[implicit_reducible]

instance Aikhenvald2004.EvidentialSystem.instDecidablePredHasEvidentials :

DecidablePred HasEvidentials

Equations

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

def Aikhenvald2004.EvidentialSystem.HasDirect :

EvidentialSystem → Prop

Whether a language grammaticalizes a direct evidence category.

Equations

Instances For

@[simp]

theorem Aikhenvald2004.EvidentialSystem.hasDirect_iff (s : EvidentialSystem) :

s.HasDirect ↔ s = directAndIndirect ∨ s = threeOrMore

@[implicit_reducible]

instance Aikhenvald2004.EvidentialSystem.instDecidablePredHasDirect :

DecidablePred HasDirect

Equations

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

def Aikhenvald2004.EvidentialSystem.numChoices :

EvidentialSystem → Nat

Number of evidential choices in the system (0, 1, 2, or 3+).

Equations

Instances For

inductive Aikhenvald2004.EvidentialCoding :

WALS Ch 78: how evidentiality is morphologically expressed.

verbalAffix : EvidentialCoding
Evidential is a verbal affix or clitic (bound morpheme). Dominant strategy worldwide (131/418 in WALS Ch 78).
clitic : EvidentialCoding
Evidential is a clitic (phrasal-level, not strictly verbal).
particle : EvidentialCoding
Evidential is a free separate particle (65/418).
partOfTAM : EvidentialCoding
Evidential distinctions fused into the TAM paradigm.
notApplicable : EvidentialCoding
Not applicable: language has no grammatical evidentials.

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instDecidableEqEvidentialCoding :

DecidableEq EvidentialCoding

Equations

Aikhenvald2004.instDecidableEqEvidentialCoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aikhenvald2004.instBEqEvidentialCoding :

BEq EvidentialCoding

Equations

Aikhenvald2004.instBEqEvidentialCoding = { beq := Aikhenvald2004.instBEqEvidentialCoding.beq }

def Aikhenvald2004.instBEqEvidentialCoding.beq :

EvidentialCoding → EvidentialCoding → Bool

Equations

Aikhenvald2004.instBEqEvidentialCoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instReprEvidentialCoding :

Repr EvidentialCoding

Equations

Aikhenvald2004.instReprEvidentialCoding = { reprPrec := Aikhenvald2004.instReprEvidentialCoding.repr }

def Aikhenvald2004.instReprEvidentialCoding.repr :

EvidentialCoding → Nat → Std.Format

Equations

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

Instances For

def Aikhenvald2004.EvidentialCoding.IsBound :

EvidentialCoding → Prop

Whether the coding strategy involves a bound morpheme (affix or clitic).

Equations

Aikhenvald2004.EvidentialCoding.verbalAffix.IsBound = True
Aikhenvald2004.EvidentialCoding.clitic.IsBound = True
Aikhenvald2004.EvidentialCoding.particle.IsBound = False
Aikhenvald2004.EvidentialCoding.partOfTAM.IsBound = False
Aikhenvald2004.EvidentialCoding.notApplicable.IsBound = False

Instances For

@[simp]

theorem Aikhenvald2004.EvidentialCoding.isBound_iff (c : EvidentialCoding) :

c.IsBound ↔ c = verbalAffix ∨ c = clitic

@[implicit_reducible]

instance Aikhenvald2004.EvidentialCoding.instDecidablePredIsBound :

DecidablePred IsBound

Equations

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

def Aikhenvald2004.fromWALS77A :

Data.WALS.F77A.EvidentialityDistinctions → EvidentialSystem

WALS Ch 77 → EvidentialSystem. WALS Ch 77's 3-way classification maps onto our 4-way; threeOrMore cannot be reached from WALS alone (WALS lumps three-or-more systems with directAndIndirect).

Equations

Instances For

def Aikhenvald2004.fromWALS78A :

Data.WALS.F78A.EvidentialityCoding → EvidentialCoding

WALS Ch 78 → EvidentialCoding. WALS lumps "verbal affix or clitic"; the mixed and modalMorpheme categories are mapped to closest local cells (best-effort).

Equations

Instances For

def Aikhenvald2004.walsEvidentialSystem (iso : String) :

Option EvidentialSystem

WALS Ch 77 lookup by ISO 639-3 code. none for languages WALS doesn't cover. Used by Aikhenvald-vs-WALS divergence theorems.

Equations

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

Instances For

def Aikhenvald2004.walsEvidentialCoding (iso : String) :

Option EvidentialCoding

WALS Ch 78 lookup by ISO 639-3 code.

Equations

Aikhenvald2004.walsEvidentialCoding iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F78A.EvidentialityCoding) => Aikhenvald2004.fromWALS78A x.value) (Data.WALS.F78A.lookupISO iso)

Instances For

inductive Aikhenvald2004.AikhenvaldSystem :

[Aik04] Ch 2 paradigm system-type classification. The letter encodes term count (A=2, B=3, C=4, D=5); the digit encodes paradigm shape.

A1 : AikhenvaldSystem
A1: Firsthand vs Non-firsthand. The most common 2-term type (Cherokee, Jarawara, Yukaghir, Tibetan). Aikhenvald 2004 Ch 2 §2.1.1.
A2 : AikhenvaldSystem
A2: Non-firsthand vs 'everything else'. The single marked term covers inference and report. Common in Turkic and Caucasian languages (Turkish, Abkhaz, Hunzib). Aikhenvald 2004 Ch 2 §2.1.1.
A3 : AikhenvaldSystem
A3: Reported (or 'hearsay') vs 'everything else'. The single marked term is the reportative. Widespread (Lezgian, Estonian, Enga, Kham, many North American Indian languages). Aikhenvald 2004 Ch 2 §2.1.1.
A4 : AikhenvaldSystem
A4: Sensory evidence and Reported. Both terms marked (Ngiyambaa, Diyari, Lakondê/Latundê, reduced Wintu). Aikhenvald 2004 Ch 2 §2.1.1.
A5 : AikhenvaldSystem
A5: Auditory vs 'everything else'. Attested only in Euchee. Aikhenvald 2004 Ch 2 §2.1.1.
B1 : AikhenvaldSystem
B1: Direct (or Visual) + Inferred + Reported. The most common 3-term system. The Quechua family (-mi, -chi, -shi), Wanka Quechua, Shasta, Amdo Tibetan, Qiang, Mosetén. Aikhenvald 2004 Ch 2 §2.2.
B2 : AikhenvaldSystem
B2: Visual + Non-visual sensory + Inferred. No reportative. Rare (Washo, Siona). Aikhenvald 2004 Ch 2 §2.2.
B3 : AikhenvaldSystem
B3: Visual + Non-visual sensory + Reported. No inferential. Oksapmin, Maricopa, Dulong. Aikhenvald 2004 Ch 2 §2.2.
B4 : AikhenvaldSystem
B4: Non-visual sensory + Inferred + Reported. Visual is unmarked default (Nganasan, Enets, Retuarã). Aikhenvald 2004 Ch 2 §2.2.
B5 : AikhenvaldSystem
B5: Reported + Quotative + 'everything else'. Two distinct reported-type evidentials, similar to A3 with quotative split (Comanche, Dakota, Tonkawa). Aikhenvald 2004 Ch 2 §2.2.
C1 : AikhenvaldSystem
C1: Visual + Non-visual sensory + Inferred + Reported. The most common 4-term system; East Tucanoan languages (Tucano, Barasano, Tatuyo, Siriano, Macuna), Eastern Pomo, traditional Tariana. Aikhenvald 2004 Ch 2 §2.3.
C2 : AikhenvaldSystem
C2: Direct (or Visual) + Inferred + Assumed + Reported. The sensory may be just visual (Tsafiki, Shipibo-Konibo, Pawnee, Mamainde). Aikhenvald 2004 Ch 2 §2.3.
C3 : AikhenvaldSystem
C3: Direct + Inferred + Reported + Quotative. Two distinct reportative types (Cora, Northern Embera, SE Tepehuan). Aikhenvald 2004 Ch 2 §2.3.
D1 : AikhenvaldSystem
D1: Visual + Non-visual sensory + Inferred + Assumed + Reported. The classical 5-term system: current Tariana, Tuyuca, Desano, traditional Wintu. Kashaya is comparable but distinguishes auditory within non-visual. Aikhenvald 2004 Ch 2 §2.4.

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instDecidableEqAikhenvaldSystem :

DecidableEq AikhenvaldSystem

Equations

Aikhenvald2004.instDecidableEqAikhenvaldSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aikhenvald2004.instBEqAikhenvaldSystem :

BEq AikhenvaldSystem

Equations

Aikhenvald2004.instBEqAikhenvaldSystem = { beq := Aikhenvald2004.instBEqAikhenvaldSystem.beq }

def Aikhenvald2004.instBEqAikhenvaldSystem.beq :

AikhenvaldSystem → AikhenvaldSystem → Bool

Equations

Aikhenvald2004.instBEqAikhenvaldSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Aikhenvald2004.instReprAikhenvaldSystem.repr :

AikhenvaldSystem → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Aikhenvald2004.instReprAikhenvaldSystem :

Repr AikhenvaldSystem

Equations

Aikhenvald2004.instReprAikhenvaldSystem = { reprPrec := Aikhenvald2004.instReprAikhenvaldSystem.repr }

@[implicit_reducible]

instance Aikhenvald2004.instInhabitedAikhenvaldSystem :

Inhabited AikhenvaldSystem

Equations

Aikhenvald2004.instInhabitedAikhenvaldSystem = { default := Aikhenvald2004.instInhabitedAikhenvaldSystem.default }

def Aikhenvald2004.AikhenvaldSystem.termCount :

AikhenvaldSystem → Nat

Number of evidential terms in the paradigm. The letter prefix encodes the count directly: A=2, B=3, C=4, D=5. Note: A2/A3/A5 have only one marked term but Aikhenvald counts the unmarked 'everything else' form, giving 2 (see Ch 2 §2.1).

Equations

Instances For

def Aikhenvald2004.AikhenvaldSystem.toWALS :

AikhenvaldSystem → EvidentialSystem

Projection to the WALS Ch 77 ([dH13b]) classification, extended with threeOrMore. A-systems map per their direct/indirect coverage; B/C/D map uniformly to .threeOrMore. WALS itself collapses B/C/D into .directAndIndirect; the .threeOrMore extension is linglib's, preserving Aikhenvald's richer typology (see Typology/Modality.lean and Aikhenvald 2004 Ch 2 §2.2).

Equations

Instances For

@[simp]

theorem Aikhenvald2004.AikhenvaldSystem.termCount_pos (s : AikhenvaldSystem) :

0 < s.termCount

The Aikhenvald typology is always richer-or-equal to the WALS one: .threeOrMore for all 3+-term systems (B/C/D), the appropriate 2-way value for 2-term systems (A).

@[simp]

theorem Aikhenvald2004.AikhenvaldSystem.termCount_le_5 (s : AikhenvaldSystem) :

s.termCount ≤ 5

Derivation from a typed inventory #

def Aikhenvald2004.AikhenvaldSystem.fromInventory (es : List Semantics.Evidential.Entry) :

Option AikhenvaldSystem

Derive [Aik04]'s paradigm system-type letter from a declared inventory by inspecting which cells of her paradigm space are covered. Mirrors Determiner.markingStrategy's derivation pattern. Returns none for inventories whose cell pattern doesn't fit any standard A–D letter; per-paper editorial overrides for such cases live in the relevant Studies/AuthorYear.lean.

Equations

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

Instances For

Worked examples documenting the API #

§1. Paper-vs-derived disagreements #

[Aik04]'s own letter assignment for the four sample languages where it differs from AikhenvaldSystem.fromInventory:

Turkish, Bulgarian, Abkhaz: Aikhenvald treats one term as unmarked default (A2 = single marked non-firsthand); Fragment counts both terms (A1).
Kashaya: Aikhenvald assigns D1 as closest fit; derivation returns none because the auditory cell plus missing nonvisualSensory and assumed cells break D1's structural pattern.

def Aikhenvald2004.paperType :

String → Option AikhenvaldSystem

Aikhenvald 2004's own letter for the four divergent languages. none for any language whose derivation matches the paper.

Equations

Aikhenvald2004.paperType "tur" = some Aikhenvald2004.AikhenvaldSystem.A2
Aikhenvald2004.paperType "bul" = some Aikhenvald2004.AikhenvaldSystem.A2
Aikhenvald2004.paperType "abk" = some Aikhenvald2004.AikhenvaldSystem.A2
Aikhenvald2004.paperType "kju" = some Aikhenvald2004.AikhenvaldSystem.D1
Aikhenvald2004.paperType x✝ = none

Instances For

theorem Aikhenvald2004.turkish_paper_vs_derived :

AikhenvaldSystem.fromInventory Turkish.Evidentiality.evidentials = some AikhenvaldSystem.A1 ∧ paperType "tur" = some AikhenvaldSystem.A2

theorem Aikhenvald2004.bulgarian_paper_vs_derived :

AikhenvaldSystem.fromInventory Bulgarian.Evidentiality.evidentials = some AikhenvaldSystem.A1 ∧ paperType "bul" = some AikhenvaldSystem.A2

theorem Aikhenvald2004.abkhaz_paper_vs_derived :

AikhenvaldSystem.fromInventory Abkhaz.Evidentiality.evidentials = some AikhenvaldSystem.A1 ∧ paperType "abk" = some AikhenvaldSystem.A2

theorem Aikhenvald2004.kashaya_paper_vs_derived :

AikhenvaldSystem.fromInventory Kashaya.Evidentiality.evidentials = none ∧ paperType "kju" = some AikhenvaldSystem.D1

§2. Aikhenvald-vs-WALS disagreements #

Representative cases — same structural pattern repeats across the other indirectOnly-via-modal cases (German, Korean, Finnish) and the other WALS-lumps-rich-systems cases (Tariana, Kashaya).

theorem Aikhenvald2004.french_wals_divergence :

AikhenvaldSystem.fromInventory French.Evidentiality.evidentials = none ∧ walsEvidentialSystem "fra" = some EvidentialSystem.indirectOnly

Empty inventory per Aikhenvald-strict vs WALS indirectOnly. French is the canonical case: the journalistic conditional has reportative use that WALS counts but Aikhenvald excludes. Same pattern holds for German, Japanese, Korean, Finnish.

theorem Aikhenvald2004.japanese_wals_divergence :

AikhenvaldSystem.fromInventory Japanese.Evidentiality.evidentials = none ∧ walsEvidentialSystem "jpn" = some EvidentialSystem.indirectOnly

theorem Aikhenvald2004.tuyuca_wals_divergence :

AikhenvaldSystem.fromInventory Tuyuca.Evidentiality.evidentials = some AikhenvaldSystem.D1 ∧ AikhenvaldSystem.D1.toWALS = EvidentialSystem.threeOrMore ∧ walsEvidentialSystem "tue" = some EvidentialSystem.directAndIndirect

The signature divergence: Tuyuca's D1 5-term system per Aikhenvald (projecting to threeOrMore) vs WALS's directAndIndirect lump. Same paradigm, two classifications, both kernel-verified.

theorem Aikhenvald2004.quechua_no_wals_entry :

AikhenvaldSystem.fromInventory Quechua.Evidentiality.evidentials = some AikhenvaldSystem.B1 ∧ walsEvidentialSystem "quz" = none

Andean B1: Aikhenvald has classification; WALS has no entry.

theorem Aikhenvald2004.turkish_wals_divergence :

AikhenvaldSystem.A2.toWALS = EvidentialSystem.indirectOnly ∧ walsEvidentialSystem "tur" = some EvidentialSystem.directAndIndirect

Turkish: derivation's A1 happens to project to the same WALS coding (directAndIndirect) WALS assigns directly; the Aikhenvald paper A2 projects to indirectOnly. Triple-comparison divergence.