Documentation

Linglib.Typology.TenseAspect

Tense-aspect typology — substrate types and WALS data #

@cite{wals-2013} (Chs 65–69, 78) @cite{comrie-1985} @cite{dahl-velupillai-2013} @cite{de-haan-2013} @cite{dryer-haspelmath-2013} @cite{bybee-perkins-pagliuca-1994}

Type-level enums + per-language profile struct for tense-aspect-mood- evidentiality systems across @cite{wals-2013} 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 lives in Linglib/Typology/Modality.lean (promoted there during the Modality/Typology dissolution). The two enums have overlapping values; consumers requiring full WALS Ch 78 round-tripping should use Typology.Modality.EvidentialCoding.

inductive Typology.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 Typology.instDecidableEqAspectMarking :

DecidableEq AspectMarking

Equations

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

def Typology.instReprAspectMarking.repr :

AspectMarking → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprAspectMarking :

Repr AspectMarking

Equations

Typology.instReprAspectMarking = { reprPrec := Typology.instReprAspectMarking.repr }

inductive Typology.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 Typology.instDecidableEqPastMarking :

DecidableEq PastMarking

Equations

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

@[implicit_reducible]

instance Typology.instReprPastMarking :

Repr PastMarking

Equations

Typology.instReprPastMarking = { reprPrec := Typology.instReprPastMarking.repr }

def Typology.instReprPastMarking.repr :

PastMarking → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Typology.instReprPastMarking.repr Typology.PastMarking.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.PastMarking.none")).group prec✝

Instances For

def Typology.PastMarking.hasMarking :

PastMarking → Bool

Whether a language has any past tense marking.

Equations

Typology.PastMarking.marked.hasMarking = true
Typology.PastMarking.markedRemoteness2_3.hasMarking = true
Typology.PastMarking.markedRemoteness4plus.hasMarking = true
Typology.PastMarking.none.hasMarking = false

Instances For

inductive Typology.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 Typology.instDecidableEqFutureMarking :

DecidableEq FutureMarking

Equations

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

def Typology.instReprFutureMarking.repr :

FutureMarking → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprFutureMarking :

Repr FutureMarking

Equations

Typology.instReprFutureMarking = { reprPrec := Typology.instReprFutureMarking.repr }

inductive Typology.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 Typology.instDecidableEqPerfectType :

DecidableEq PerfectType

Equations

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

def Typology.instReprPerfectType.repr :

PerfectType → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Typology.instReprPerfectType.repr Typology.PerfectType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.PerfectType.none")).group prec✝

Instances For

@[implicit_reducible]

instance Typology.instReprPerfectType :

Repr PerfectType

Equations

Typology.instReprPerfectType = { reprPrec := Typology.instReprPerfectType.repr }

def Typology.PerfectType.hasPerfect :

PerfectType → Bool

Whether a language has any perfect category.

Equations

Typology.PerfectType.fromPossessive.hasPerfect = true
Typology.PerfectType.fromFinishAlready.hasPerfect = true
Typology.PerfectType.other.hasPerfect = true
Typology.PerfectType.none.hasPerfect = false

Instances For

inductive Typology.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 Typology.instDecidableEqTAAffixPosition :

DecidableEq TAAffixPosition

Equations

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

def Typology.instReprTAAffixPosition.repr :

TAAffixPosition → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprTAAffixPosition :

Repr TAAffixPosition

Equations

Typology.instReprTAAffixPosition = { reprPrec := Typology.instReprTAAffixPosition.repr }

def Typology.TAAffixPosition.hasAffixes :

TAAffixPosition → Bool

Whether a language has any tense-aspect affixation.

Equations

Typology.TAAffixPosition.prefixing.hasAffixes = true
Typology.TAAffixPosition.suffixing.hasAffixes = true
Typology.TAAffixPosition.tonal.hasAffixes = true
Typology.TAAffixPosition.mixed.hasAffixes = true
Typology.TAAffixPosition.noInflection.hasAffixes = false

Instances For

inductive Typology.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 Typology.instDecidableEqEvidentialityCoding :

DecidableEq EvidentialityCoding

Equations

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

@[implicit_reducible]

instance Typology.instReprEvidentialityCoding :

Repr EvidentialityCoding

Equations

Typology.instReprEvidentialityCoding = { reprPrec := Typology.instReprEvidentialityCoding.repr }

def Typology.instReprEvidentialityCoding.repr :

EvidentialityCoding → Nat → Std.Format

Equations

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

Instances For

def Typology.EvidentialityCoding.hasEvidentiality :

EvidentialityCoding → Bool

Whether a language has any grammatical evidentiality.

Equations

Typology.EvidentialityCoding.none.hasEvidentiality = false
x✝.hasEvidentiality = true

Instances For

structure Typology.TAProfile :

A language's tense-aspect-mood-evidentiality profile across @cite{wals-2013} 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 Typology.instReprTAProfile.repr :

TAProfile → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprTAProfile :

Equations

Typology.instReprTAProfile = { reprPrec := Typology.instReprTAProfile.repr }

def Typology.instDecidableEqTAProfile.decEq (x✝ x✝¹ : TAProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instDecidableEqTAProfile :

DecidableEq TAProfile

Equations

Typology.instDecidableEqTAProfile = Typology.instDecidableEqTAProfile.decEq

def Typology.TAProfile.hasTenseOrAspect (p : TAProfile) :

Bool

Whether a profile has any tense or aspect marking.

Equations

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

Instances For

def Typology.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 == Typology.AspectMarking.none && p.past == Typology.PastMarking.none && p.future == Typology.FutureMarking.none)

Instances For

def Typology.fromWALS65A :

Data.WALS.F65A.PerfectiveImperfective → AspectMarking

Equations

Instances For

def Typology.fromWALS66A :

Data.WALS.F66A.PastTenseType → PastMarking

Equations

Instances For

def Typology.fromWALS67A :

Data.WALS.F67A.FutureTenseType → FutureMarking

Equations

Instances For

def Typology.fromWALS68A :

Data.WALS.F68A.PerfectType → PerfectType

Equations

Instances For

def Typology.fromWALS69A :

Data.WALS.F69A.TenseAspectAffixPosition → TAAffixPosition

Equations

Instances For

structure Typology.Ch65Counts :

WALS Ch 65 distribution (n = 222).

grammatical : Nat
noMarking : Nat

Instances For

def Typology.instReprCh65Counts.repr :

Ch65Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprCh65Counts :

Repr Ch65Counts

Equations

Typology.instReprCh65Counts = { reprPrec := Typology.instReprCh65Counts.repr }

def Typology.instDecidableEqCh65Counts.decEq (x✝ x✝¹ : Ch65Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instDecidableEqCh65Counts :

DecidableEq Ch65Counts

Equations

Typology.instDecidableEqCh65Counts = Typology.instDecidableEqCh65Counts.decEq

def Typology.Ch65Counts.total (c : Ch65Counts) :

Nat

Equations

c.total = c.grammatical + c.noMarking

Instances For

def Typology.walsCh65 :

WALS Ch 65 counts (222 languages).

Equations

Typology.walsCh65 = { grammatical := 101, noMarking := 121 }

Instances For

structure Typology.Ch66Counts :

WALS Ch 66 distribution (n = 222).

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

Instances For

@[implicit_reducible]

instance Typology.instReprCh66Counts :

Repr Ch66Counts

Equations

Typology.instReprCh66Counts = { reprPrec := Typology.instReprCh66Counts.repr }

def Typology.instReprCh66Counts.repr :

Ch66Counts → Nat → Std.Format

Equations

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

Instances For

def Typology.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 Typology.instDecidableEqCh66Counts :

DecidableEq Ch66Counts

Equations

Typology.instDecidableEqCh66Counts = Typology.instDecidableEqCh66Counts.decEq

def Typology.Ch66Counts.total (c : Ch66Counts) :

Nat

Equations

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

Instances For

def Typology.Ch66Counts.totalWithPast (c : Ch66Counts) :

Nat

Equations

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

Instances For

def Typology.walsCh66 :

WALS Ch 66 counts (222 languages).

Equations

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

Instances For

structure Typology.Ch67Counts :

WALS Ch 67 distribution (n = 222).

inflectional : Nat
noInflectional : Nat

Instances For

def Typology.instReprCh67Counts.repr :

Ch67Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprCh67Counts :

Repr Ch67Counts

Equations

Typology.instReprCh67Counts = { reprPrec := Typology.instReprCh67Counts.repr }

def Typology.instDecidableEqCh67Counts.decEq (x✝ x✝¹ : Ch67Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instDecidableEqCh67Counts :

DecidableEq Ch67Counts

Equations

Typology.instDecidableEqCh67Counts = Typology.instDecidableEqCh67Counts.decEq

def Typology.Ch67Counts.total (c : Ch67Counts) :

Nat

Equations

c.total = c.inflectional + c.noInflectional

Instances For

def Typology.walsCh67 :

WALS Ch 67 counts (222 languages).

Equations

Typology.walsCh67 = { inflectional := 110, noInflectional := 112 }

Instances For

structure Typology.Ch68Counts :

WALS Ch 68 distribution (n = 222).

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

Instances For

def Typology.instReprCh68Counts.repr :

Ch68Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instReprCh68Counts :

Repr Ch68Counts

Equations

Typology.instReprCh68Counts = { reprPrec := Typology.instReprCh68Counts.repr }

def Typology.instDecidableEqCh68Counts.decEq (x✝ x✝¹ : Ch68Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instDecidableEqCh68Counts :

DecidableEq Ch68Counts

Equations

Typology.instDecidableEqCh68Counts = Typology.instDecidableEqCh68Counts.decEq

def Typology.Ch68Counts.total (c : Ch68Counts) :

Nat

Equations

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

Instances For

def Typology.walsCh68 :

WALS Ch 68 counts (222 languages).

Equations

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

Instances For

structure Typology.Ch69Counts :

WALS Ch 69 distribution (n = 1131).

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

Instances For

@[implicit_reducible]

instance Typology.instReprCh69Counts :

Repr Ch69Counts

Equations

Typology.instReprCh69Counts = { reprPrec := Typology.instReprCh69Counts.repr }

def Typology.instReprCh69Counts.repr :

Ch69Counts → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.instDecidableEqCh69Counts :

DecidableEq Ch69Counts

Equations

Typology.instDecidableEqCh69Counts = Typology.instDecidableEqCh69Counts.decEq

def Typology.instDecidableEqCh69Counts.decEq (x✝ x✝¹ : Ch69Counts) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Typology.Ch69Counts.total (c : Ch69Counts) :

Nat

Equations

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

Instances For

def Typology.walsCh69 :

WALS Ch 69 counts (1131 languages).

Equations

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

Instances For

theorem Typology.past_marking_majority :

walsCh66.totalWithPast > walsCh66.noMarking

A majority of @cite{wals-2013} Ch 66 languages have past marking (134 of 222 = 60%).

theorem Typology.suffix_dominant_over_prefix :

walsCh69.suffixing > 4 * walsCh69.prefixing

Suffix dominance: @cite{wals-2013} Ch 69 suffixes outnumber prefixes by more than 4:1 (667 vs 153).

theorem Typology.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 Typology.suffix_absolute_majority :

walsCh69.suffixing * 2 > walsCh69.total

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

theorem Typology.tone_ta_rare :

walsCh69.tonal < 15

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

theorem Typology.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 Typology.have_perfect_rare :

walsCh68.fromPossessive < 10

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

theorem Typology.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 Typology.no_perfect_majority :

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

Most languages lack a distinct perfect category entirely.

theorem Typology.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 Typology.extreme_remoteness_very_rare :

walsCh66.markedRemoteness4plus = 2

Extreme remoteness (4+ degrees) is attested in only 2 languages worldwide in the @cite{wals-2013} sample.