Documentation

Linglib.Morphology.TenseAspect

Tense-aspect typology — substrate types and WALS data #

[DH13b] (Chs 65–69, 78) [Com85] [DV13b] [dH13b] [DH13a] [BPP94]

Type-level enums + per-language profile struct for tense-aspect-mood- evidentiality systems across [DH13b] chapters 65–69 and 78, plus WALS distribution data and the principal cross-linguistic generalizations.

Schema #

AspectMarking (Ch 65): grammatical perfective/imperfective marking
PastMarking (Ch 66): past tense marking + remoteness distinctions
FutureMarking (Ch 67): inflectional future tense
PerfectType (Ch 68): perfect category and its diachronic source
TAAffixPosition (Ch 69): position of tense-aspect affixes
EvidentialityCoding (Ch 78): coding strategy for evidentiality
TAProfile: per-language bundle (Chs 65–69 + optional Ch 78)

Per-language data lives in Fragments/{Lang}/TenseAspect.lean.

Note on EvidentialityCoding #

A parallel enum EvidentialCoding was consolidated into Linglib/Studies/Aikhenvald2004.lean (during the Typology/ dissolution). The two enums have overlapping values; consumers requiring full WALS Ch 78 round-tripping should use Aikhenvald2004.EvidentialCoding.

inductive Morphology.TenseAspect.AspectMarking :

WALS Ch 65: whether the perfective/imperfective distinction is grammaticalized. "Grammatical marking" includes both morphological and periphrastic constructions.

grammatical : AspectMarking
Grammatical perfective/imperfective marking present.
none : AspectMarking
No grammatical marking.

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqAspectMarking :

DecidableEq AspectMarking

Equations

Morphology.TenseAspect.instDecidableEqAspectMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.TenseAspect.instReprAspectMarking :

Repr AspectMarking

Equations

Morphology.TenseAspect.instReprAspectMarking = { reprPrec := Morphology.TenseAspect.instReprAspectMarking.repr }

def Morphology.TenseAspect.instReprAspectMarking.repr :

AspectMarking → Nat → Std.Format

Equations

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

Instances For

inductive Morphology.TenseAspect.PastMarking :

WALS Ch 66: past tense marking and remoteness distinctions. Past imperfectives (Armenian-style, restricted to imperfective contexts) count as past marking.

marked : PastMarking
Past/non-past marked, no remoteness distinctions.
markedRemoteness2_3 : PastMarking
Past/non-past marked + 2–3 degrees of remoteness.
markedRemoteness4plus : PastMarking
Past/non-past marked + 4+ degrees of remoteness.
none : PastMarking
No grammatical past/non-past distinction.

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqPastMarking :

DecidableEq PastMarking

Equations

Morphology.TenseAspect.instDecidableEqPastMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.TenseAspect.instReprPastMarking :

Repr PastMarking

Equations

Morphology.TenseAspect.instReprPastMarking = { reprPrec := Morphology.TenseAspect.instReprPastMarking.repr }

def Morphology.TenseAspect.instReprPastMarking.repr :

PastMarking → Nat → Std.Format

Equations

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

Instances For

def Morphology.TenseAspect.PastMarking.hasMarking :

PastMarking → Bool

Whether a language has any past tense marking.

Equations

Instances For

inductive Morphology.TenseAspect.FutureMarking :

WALS Ch 67: inflectional future marking. Only inflectional marking is counted (not periphrastic will + V). Irrealis markers that obligatorily encode future reference are included.

inflectional : FutureMarking
Inflectional future/nonfuture distinction.
none : FutureMarking
No inflectional future.

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqFutureMarking :

DecidableEq FutureMarking

Equations

Morphology.TenseAspect.instDecidableEqFutureMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.TenseAspect.instReprFutureMarking.repr :

FutureMarking → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprFutureMarking :

Repr FutureMarking

Equations

Morphology.TenseAspect.instReprFutureMarking = { reprPrec := Morphology.TenseAspect.instReprFutureMarking.repr }

inductive Morphology.TenseAspect.PerfectType :

WALS Ch 68: perfect category and its diachronic source. A form counts as a perfect only if it has both resultative and experiential uses (not a general past, not a dedicated resultative).

fromPossessive : PerfectType
'have'-perfect from possessive construction (almost exclusively western Europe).
fromFinishAlready : PerfectType
Perfect from 'finish' or 'already' (concentrated in SE Asia and West Africa).
other : PerfectType
Other perfect (dedicated resultative source, or undetermined).
none : PerfectType
No perfect category.

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqPerfectType :

DecidableEq PerfectType

Equations

Morphology.TenseAspect.instDecidableEqPerfectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.TenseAspect.instReprPerfectType :

Repr PerfectType

Equations

Morphology.TenseAspect.instReprPerfectType = { reprPrec := Morphology.TenseAspect.instReprPerfectType.repr }

def Morphology.TenseAspect.instReprPerfectType.repr :

PerfectType → Nat → Std.Format

Equations

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

Instances For

def Morphology.TenseAspect.PerfectType.hasPerfect :

PerfectType → Bool

Whether a language has any perfect category.

Equations

Instances For

inductive Morphology.TenseAspect.TAAffixPosition :

WALS Ch 69: primary morphological strategy for tense-aspect marking. Mixed strategies with no dominant type are coded as mixed; infixes and stem changes are subsumed under prefix/suffix when localized at edges.

prefixing : TAAffixPosition
Tense-aspect prefixes.
suffixing : TAAffixPosition
Tense-aspect suffixes.
tonal : TAAffixPosition
Tonal tense-aspect (almost exclusively African).
mixed : TAAffixPosition
Mixed strategies, none primary.
noInflection : TAAffixPosition
No tense-aspect inflection.

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqTAAffixPosition :

DecidableEq TAAffixPosition

Equations

Morphology.TenseAspect.instDecidableEqTAAffixPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.TenseAspect.instReprTAAffixPosition :

Repr TAAffixPosition

Equations

Morphology.TenseAspect.instReprTAAffixPosition = { reprPrec := Morphology.TenseAspect.instReprTAAffixPosition.repr }

def Morphology.TenseAspect.instReprTAAffixPosition.repr :

TAAffixPosition → Nat → Std.Format

Equations

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

Instances For

def Morphology.TenseAspect.TAAffixPosition.hasAffixes :

TAAffixPosition → Bool

Whether a language has any tense-aspect affixation.

Equations

Instances For

inductive Morphology.TenseAspect.EvidentialityCoding :

WALS Ch 78: how evidentiality is coded. "Evidentiality" means grammaticalized marking of information source.

none : EvidentialityCoding
No grammatical evidentiality.
partOfTense : EvidentialityCoding
Evidentiality is part of the tense paradigm (e.g., Turkish -miş).
verbalAffix : EvidentialityCoding
Verbal affix.
clitic : EvidentialityCoding
Clitic.
particle : EvidentialityCoding
Particle.
other : EvidentialityCoding
Other strategy.

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqEvidentialityCoding :

DecidableEq EvidentialityCoding

Equations

Morphology.TenseAspect.instDecidableEqEvidentialityCoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.TenseAspect.instReprEvidentialityCoding :

Repr EvidentialityCoding

Equations

Morphology.TenseAspect.instReprEvidentialityCoding = { reprPrec := Morphology.TenseAspect.instReprEvidentialityCoding.repr }

def Morphology.TenseAspect.instReprEvidentialityCoding.repr :

EvidentialityCoding → Nat → Std.Format

Equations

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

Instances For

def Morphology.TenseAspect.EvidentialityCoding.hasEvidentiality :

EvidentialityCoding → Bool

Whether a language has any grammatical evidentiality.

Equations

Morphology.TenseAspect.EvidentialityCoding.none.hasEvidentiality = false
x✝.hasEvidentiality = true

Instances For

structure Morphology.TenseAspect.TAProfile :

A language's tense-aspect-mood-evidentiality profile across [DH13b] Chs 65–69 (mandatory) and Ch 78 (optional).

language : String
iso : String
family : String
aspect : AspectMarking
Ch 65: perfective/imperfective aspect.
past : PastMarking
Ch 66: past tense marking.
future : FutureMarking
Ch 67: inflectional future.
perfect : PerfectType
Ch 68: perfect category.
affixPosition : TAAffixPosition
Ch 69: tense-aspect affix position.
evidentialityCoding : Option EvidentialityCoding
Ch 78: evidentiality coding (none if not in WALS Ch 78 sample).

Instances For

def Morphology.TenseAspect.instReprTAProfile.repr :

TAProfile → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprTAProfile :

Equations

Morphology.TenseAspect.instReprTAProfile = { reprPrec := Morphology.TenseAspect.instReprTAProfile.repr }

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqTAProfile :

DecidableEq TAProfile

Equations

Morphology.TenseAspect.instDecidableEqTAProfile = Morphology.TenseAspect.instDecidableEqTAProfile.decEq

def Morphology.TenseAspect.instDecidableEqTAProfile.decEq (x✝ x✝¹ : TAProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Morphology.TenseAspect.TAProfile.hasTenseOrAspect (p : TAProfile) :

Bool

Whether a profile has any tense or aspect marking.

Equations

p.hasTenseOrAspect = (p.aspect == Morphology.TenseAspect.AspectMarking.grammatical || p.past.hasMarking || p.future == Morphology.TenseAspect.FutureMarking.inflectional)

Instances For

def Morphology.TenseAspect.TAProfile.lacksMajorTAGrams (p : TAProfile) :

Bool

Whether a profile lacks all three major T/A gram types (the SE Asian isolating signature).

Equations

p.lacksMajorTAGrams = (p.aspect == Morphology.TenseAspect.AspectMarking.none && p.past == Morphology.TenseAspect.PastMarking.none && p.future == Morphology.TenseAspect.FutureMarking.none)

Instances For

def Morphology.TenseAspect.fromWALS65A :

Data.WALS.F65A.PerfectiveImperfective → AspectMarking

Equations

Instances For

def Morphology.TenseAspect.fromWALS66A :

Data.WALS.F66A.PastTenseType → PastMarking

Equations

Instances For

def Morphology.TenseAspect.fromWALS67A :

Data.WALS.F67A.FutureTenseType → FutureMarking

Equations

Instances For

def Morphology.TenseAspect.fromWALS68A :

Data.WALS.F68A.PerfectType → PerfectType

Equations

Instances For

def Morphology.TenseAspect.fromWALS69A :

Data.WALS.F69A.TenseAspectAffixPosition → TAAffixPosition

Equations

Instances For

structure Morphology.TenseAspect.Ch65Counts :

WALS Ch 65 distribution (n = 222).

grammatical : Nat
noMarking : Nat

Instances For

def Morphology.TenseAspect.instReprCh65Counts.repr :

Ch65Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprCh65Counts :

Repr Ch65Counts

Equations

Morphology.TenseAspect.instReprCh65Counts = { reprPrec := Morphology.TenseAspect.instReprCh65Counts.repr }

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqCh65Counts :

DecidableEq Ch65Counts

Equations

Morphology.TenseAspect.instDecidableEqCh65Counts = Morphology.TenseAspect.instDecidableEqCh65Counts.decEq

def Morphology.TenseAspect.instDecidableEqCh65Counts.decEq (x✝ x✝¹ : Ch65Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Morphology.TenseAspect.Ch65Counts.total (c : Ch65Counts) :

Nat

Equations

c.total = c.grammatical + c.noMarking

Instances For

def Morphology.TenseAspect.walsCh65 :

WALS Ch 65 counts (222 languages).

Equations

Morphology.TenseAspect.walsCh65 = { grammatical := 101, noMarking := 121 }

Instances For

structure Morphology.TenseAspect.Ch66Counts :

WALS Ch 66 distribution (n = 222).

markedNoRemoteness : Nat
markedRemoteness2_3 : Nat
markedRemoteness4plus : Nat
noMarking : Nat

Instances For

def Morphology.TenseAspect.instReprCh66Counts.repr :

Ch66Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprCh66Counts :

Repr Ch66Counts

Equations

Morphology.TenseAspect.instReprCh66Counts = { reprPrec := Morphology.TenseAspect.instReprCh66Counts.repr }

def Morphology.TenseAspect.instDecidableEqCh66Counts.decEq (x✝ x✝¹ : Ch66Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqCh66Counts :

DecidableEq Ch66Counts

Equations

Morphology.TenseAspect.instDecidableEqCh66Counts = Morphology.TenseAspect.instDecidableEqCh66Counts.decEq

def Morphology.TenseAspect.Ch66Counts.total (c : Ch66Counts) :

Nat

Equations

c.total = c.markedNoRemoteness + c.markedRemoteness2_3 + c.markedRemoteness4plus + c.noMarking

Instances For

def Morphology.TenseAspect.Ch66Counts.totalWithPast (c : Ch66Counts) :

Nat

Equations

c.totalWithPast = c.markedNoRemoteness + c.markedRemoteness2_3 + c.markedRemoteness4plus

Instances For

def Morphology.TenseAspect.walsCh66 :

WALS Ch 66 counts (222 languages).

Equations

Morphology.TenseAspect.walsCh66 = { markedNoRemoteness := 94, markedRemoteness2_3 := 38, markedRemoteness4plus := 2, noMarking := 88 }

Instances For

structure Morphology.TenseAspect.Ch67Counts :

WALS Ch 67 distribution (n = 222).

inflectional : Nat
noInflectional : Nat

Instances For

def Morphology.TenseAspect.instReprCh67Counts.repr :

Ch67Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprCh67Counts :

Repr Ch67Counts

Equations

Morphology.TenseAspect.instReprCh67Counts = { reprPrec := Morphology.TenseAspect.instReprCh67Counts.repr }

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqCh67Counts :

DecidableEq Ch67Counts

Equations

Morphology.TenseAspect.instDecidableEqCh67Counts = Morphology.TenseAspect.instDecidableEqCh67Counts.decEq

def Morphology.TenseAspect.instDecidableEqCh67Counts.decEq (x✝ x✝¹ : Ch67Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Morphology.TenseAspect.Ch67Counts.total (c : Ch67Counts) :

Nat

Equations

c.total = c.inflectional + c.noInflectional

Instances For

def Morphology.TenseAspect.walsCh67 :

WALS Ch 67 counts (222 languages).

Equations

Morphology.TenseAspect.walsCh67 = { inflectional := 110, noInflectional := 112 }

Instances For

structure Morphology.TenseAspect.Ch68Counts :

WALS Ch 68 distribution (n = 222).

fromPossessive : Nat
fromFinishAlready : Nat
otherPerfect : Nat
noPerfect : Nat

Instances For

def Morphology.TenseAspect.instReprCh68Counts.repr :

Ch68Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprCh68Counts :

Repr Ch68Counts

Equations

Morphology.TenseAspect.instReprCh68Counts = { reprPrec := Morphology.TenseAspect.instReprCh68Counts.repr }

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqCh68Counts :

DecidableEq Ch68Counts

Equations

Morphology.TenseAspect.instDecidableEqCh68Counts = Morphology.TenseAspect.instDecidableEqCh68Counts.decEq

def Morphology.TenseAspect.instDecidableEqCh68Counts.decEq (x✝ x✝¹ : Ch68Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Morphology.TenseAspect.Ch68Counts.total (c : Ch68Counts) :

Nat

Equations

c.total = c.fromPossessive + c.fromFinishAlready + c.otherPerfect + c.noPerfect

Instances For

def Morphology.TenseAspect.walsCh68 :

WALS Ch 68 counts (222 languages).

Equations

Morphology.TenseAspect.walsCh68 = { fromPossessive := 7, fromFinishAlready := 21, otherPerfect := 80, noPerfect := 114 }

Instances For

structure Morphology.TenseAspect.Ch69Counts :

WALS Ch 69 distribution (n = 1131).

prefixing : Nat
suffixing : Nat
tonal : Nat
mixed : Nat
noInflection : Nat

Instances For

def Morphology.TenseAspect.instReprCh69Counts.repr :

Ch69Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instReprCh69Counts :

Repr Ch69Counts

Equations

Morphology.TenseAspect.instReprCh69Counts = { reprPrec := Morphology.TenseAspect.instReprCh69Counts.repr }

def Morphology.TenseAspect.instDecidableEqCh69Counts.decEq (x✝ x✝¹ : Ch69Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Morphology.TenseAspect.instDecidableEqCh69Counts :

DecidableEq Ch69Counts

Equations

Morphology.TenseAspect.instDecidableEqCh69Counts = Morphology.TenseAspect.instDecidableEqCh69Counts.decEq

def Morphology.TenseAspect.Ch69Counts.total (c : Ch69Counts) :

Nat

Equations

c.total = c.prefixing + c.suffixing + c.tonal + c.mixed + c.noInflection

Instances For

def Morphology.TenseAspect.walsCh69 :

WALS Ch 69 counts (1131 languages).

Equations

Morphology.TenseAspect.walsCh69 = { prefixing := 153, suffixing := 667, tonal := 13, mixed := 24, noInflection := 274 }

Instances For

theorem Morphology.TenseAspect.past_marking_majority :

walsCh66.totalWithPast > walsCh66.noMarking

A majority of [DH13b] Ch 66 languages have past marking (134 of 222 = 60%).

theorem Morphology.TenseAspect.suffix_dominant_over_prefix :

walsCh69.suffixing > 4 * walsCh69.prefixing

Suffix dominance: [DH13b] Ch 69 suffixes outnumber prefixes by more than 4:1 (667 vs 153).

theorem Morphology.TenseAspect.suffix_most_common :

walsCh69.suffixing > walsCh69.prefixing ∧ walsCh69.suffixing > walsCh69.tonal ∧ walsCh69.suffixing > walsCh69.mixed ∧ walsCh69.suffixing > walsCh69.noInflection

Suffixing is the most common T/A strategy overall.

theorem Morphology.TenseAspect.suffix_absolute_majority :

walsCh69.suffixing * 2 > walsCh69.total

Suffixing accounts for more than half of all languages in Ch 69.

theorem Morphology.TenseAspect.tone_ta_rare :

walsCh69.tonal < 15

Tone as a primary T/A strategy is rare (~13/1131 ≈ 1%), almost exclusively in Africa.

theorem Morphology.TenseAspect.future_near_even_split :

walsCh67.inflectional > 100 ∧ walsCh67.noInflectional > 100

The future-tense split is approximately even (110 vs 112). Neither inflectional future nor its absence is a strong majority.

theorem Morphology.TenseAspect.have_perfect_rare :

walsCh68.fromPossessive < 10

'have'-perfects are extremely rare cross-linguistically (only 7/222), restricted almost exclusively to western Europe.

theorem Morphology.TenseAspect.finish_perfect_more_common_than_have :

walsCh68.fromFinishAlready > walsCh68.fromPossessive

'finish'/'already' perfects are more common than 'have'-perfects (21 vs 7), concentrated in SE Asia and West Africa.

theorem Morphology.TenseAspect.no_perfect_majority :

walsCh68.noPerfect > walsCh68.fromPossessive + walsCh68.fromFinishAlready + walsCh68.otherPerfect

Most languages lack a distinct perfect category entirely.

theorem Morphology.TenseAspect.remoteness_uncommon :

walsCh66.markedNoRemoteness > walsCh66.markedRemoteness2_3 + walsCh66.markedRemoteness4plus

Most past-marking languages make no remoteness distinctions (94 of 134). Languages with 4+ degrees of remoteness are extremely rare (only 2; Yagua being the richest with 5 degrees).

theorem Morphology.TenseAspect.extreme_remoteness_very_rare :

walsCh66.markedRemoteness4plus = 2

Extreme remoteness (4+ degrees) is attested in only 2 languages worldwide in the [DH13b] sample.