Cross-Linguistic Typology of Tense and Aspect (WALS Chapters 65--69)

@cite{comrie-1985} @cite{dryer-haspelmath-2013} @cite{dahl-velupillai-2013} @cite{de-haan-2013}

Cross-linguistic data on tense-aspect systems from the World Atlas of Language Structures (WALS), covering five parameters:

• Ch 65 (Perfective/Imperfective Aspect): Whether a language grammaticalizes the perfective/imperfective distinction. 222 languages, two values.

• Ch 66 (The Past Tense): Whether a language has grammatical marking of past tense, and if so how many remoteness distinctions it makes. 222 languages, four values.

• Ch 67 (The Future Tense): Whether a language has inflectional marking of future tense. 222 languages, two values.

• Ch 68 (The Perfect): Whether a language has a distinct perfect category (resultative + experiential uses), and its diachronic source. 222 languages, four values.

• Ch 69 (Position of Tense-Aspect Affixes): How tense-aspect is morphologically expressed. 1062 languages, five values.

Key findings

@cite{dahl-velupillai-2013} @cite{bybee-perkins-pagliuca-1994} note that there is no evidence for a typological division into "tense languages" vs "aspect languages" -- languages that have aspectual marking tend also to have tense marking. Suffixing is overwhelmingly the dominant strategy for tense-aspect morphology. South-East Asian languages consistently lack morphological tense-aspect marking.

inductive Phenomena.TenseAspect.Typology.AspectMarking : Type

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

• grammatical : AspectMarking

  Language has grammatical marking of perfective/imperfective

• none : AspectMarking

  Language has no grammatical marking of perfective/imperfective

instance Phenomena.TenseAspect.Typology.instDecidableEqAspectMarking : DecidableEq AspectMarking

Equations

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

def Phenomena.TenseAspect.Typology.instBEqAspectMarking.beq : AspectMarking → AspectMarking → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqAspectMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Typology.instBEqAspectMarking : BEq AspectMarking

Equations

• Phenomena.TenseAspect.Typology.instBEqAspectMarking = { beq := Phenomena.TenseAspect.Typology.instBEqAspectMarking.beq }

def Phenomena.TenseAspect.Typology.instReprAspectMarking.repr : AspectMarking → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprAspectMarking : Repr AspectMarking

Equations

• Phenomena.TenseAspect.Typology.instReprAspectMarking = { reprPrec := Phenomena.TenseAspect.Typology.instReprAspectMarking.repr }

inductive Phenomena.TenseAspect.Typology.PastMarking : Type

WALS Ch 66: Past tense marking and remoteness distinctions.

Past marking includes both inflectional and periphrastic constructions. Past imperfectives (restricted to imperfective contexts, as in the Armenian Imperfect) count as past marking.

• marked : PastMarking

  Past/non-past distinction marked, no remoteness distinctions

• markedRemoteness2_3 : PastMarking

  Past/non-past distinction marked, 2-3 degrees of remoteness

• markedRemoteness4plus : PastMarking

  Past/non-past distinction marked, 4+ degrees of remoteness

• none : PastMarking

  No grammatical marking of past/non-past distinction

instance Phenomena.TenseAspect.Typology.instDecidableEqPastMarking : DecidableEq PastMarking

Equations

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

def Phenomena.TenseAspect.Typology.instBEqPastMarking.beq : PastMarking → PastMarking → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqPastMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Typology.instBEqPastMarking : BEq PastMarking

Equations

• Phenomena.TenseAspect.Typology.instBEqPastMarking = { beq := Phenomena.TenseAspect.Typology.instBEqPastMarking.beq }

def Phenomena.TenseAspect.Typology.instReprPastMarking.repr : PastMarking → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprPastMarking : Repr PastMarking

Equations

• Phenomena.TenseAspect.Typology.instReprPastMarking = { reprPrec := Phenomena.TenseAspect.Typology.instReprPastMarking.repr }

def Phenomena.TenseAspect.Typology.PastMarking.hasMarking : PastMarking → Bool

Whether a language has any past tense marking (any of the three marked categories).

Equations

• Phenomena.TenseAspect.Typology.PastMarking.marked.hasMarking = true
• Phenomena.TenseAspect.Typology.PastMarking.markedRemoteness2_3.hasMarking = true
• Phenomena.TenseAspect.Typology.PastMarking.markedRemoteness4plus.hasMarking = true
• Phenomena.TenseAspect.Typology.PastMarking.none.hasMarking = false

inductive Phenomena.TenseAspect.Typology.FutureMarking : Type

WALS Ch 67: Whether the language has inflectional future marking.

Only inflectional marking is counted here (not periphrastic constructions like English "will" + V). Irrealis markers that obligatorily encode future reference are included.

• inflectional : FutureMarking

  Inflectional marking of future/nonfuture distinction

• none : FutureMarking

  No inflectional marking of future/nonfuture distinction

instance Phenomena.TenseAspect.Typology.instDecidableEqFutureMarking : DecidableEq FutureMarking

Equations

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

def Phenomena.TenseAspect.Typology.instBEqFutureMarking.beq : FutureMarking → FutureMarking → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqFutureMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Typology.instBEqFutureMarking : BEq FutureMarking

Equations

• Phenomena.TenseAspect.Typology.instBEqFutureMarking = { beq := Phenomena.TenseAspect.Typology.instBEqFutureMarking.beq }

instance Phenomena.TenseAspect.Typology.instReprFutureMarking : Repr FutureMarking

Equations

• Phenomena.TenseAspect.Typology.instReprFutureMarking = { reprPrec := Phenomena.TenseAspect.Typology.instReprFutureMarking.repr }

def Phenomena.TenseAspect.Typology.instReprFutureMarking.repr : FutureMarking → Nat → Std.Format

Equations

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

inductive Phenomena.TenseAspect.Typology.PerfectType : Type

WALS Ch 68: Whether the language has a distinct 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

  Perfect derived from possessive construction ('have'-perfect). Restricted almost exclusively to western Europe.

• fromFinishAlready : PerfectType

  Perfect derived from word meaning 'finish' or 'already'. Concentrated in South-East Asia and West Africa.

• other : PerfectType

  Other perfect (including from dedicated resultatives, or diachronic source undetermined).

• none : PerfectType

  No perfect category.

instance Phenomena.TenseAspect.Typology.instDecidableEqPerfectType : DecidableEq PerfectType

Equations

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

instance Phenomena.TenseAspect.Typology.instBEqPerfectType : BEq PerfectType

Equations

• Phenomena.TenseAspect.Typology.instBEqPerfectType = { beq := Phenomena.TenseAspect.Typology.instBEqPerfectType.beq }

def Phenomena.TenseAspect.Typology.instBEqPerfectType.beq : PerfectType → PerfectType → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqPerfectType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Typology.instReprPerfectType : Repr PerfectType

Equations

• Phenomena.TenseAspect.Typology.instReprPerfectType = { reprPrec := Phenomena.TenseAspect.Typology.instReprPerfectType.repr }

def Phenomena.TenseAspect.Typology.instReprPerfectType.repr : PerfectType → Nat → Std.Format

Equations

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

def Phenomena.TenseAspect.Typology.PerfectType.hasPerfect : PerfectType → Bool

Whether a language has any perfect category.

Equations

• Phenomena.TenseAspect.Typology.PerfectType.fromPossessive.hasPerfect = true
• Phenomena.TenseAspect.Typology.PerfectType.fromFinishAlready.hasPerfect = true
• Phenomena.TenseAspect.Typology.PerfectType.other.hasPerfect = true
• Phenomena.TenseAspect.Typology.PerfectType.none.hasPerfect = false

inductive Phenomena.TenseAspect.Typology.TAAffixPosition : Type

WALS Ch 69: Primary morphological strategy for tense-aspect marking.

Languages with heterogeneous strategies where no single type is dominant are classified as mixed. Infixes and stem changes are treated as subtypes of prefixes/suffixes when localized at edges.

• prefixing : TAAffixPosition

  Tense-aspect prefixes (primary strategy)

• suffixing : TAAffixPosition

  Tense-aspect suffixes (primary strategy)

• tonal : TAAffixPosition

  Tense-aspect tone (primary strategy). Almost exclusively African.

• mixed : TAAffixPosition

  Combination of strategies with none primary

• noInflection : TAAffixPosition

  No tense-aspect inflection

instance Phenomena.TenseAspect.Typology.instDecidableEqTAAffixPosition : DecidableEq TAAffixPosition

Equations

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

def Phenomena.TenseAspect.Typology.instBEqTAAffixPosition.beq : TAAffixPosition → TAAffixPosition → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqTAAffixPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Typology.instBEqTAAffixPosition : BEq TAAffixPosition

Equations

• Phenomena.TenseAspect.Typology.instBEqTAAffixPosition = { beq := Phenomena.TenseAspect.Typology.instBEqTAAffixPosition.beq }

def Phenomena.TenseAspect.Typology.instReprTAAffixPosition.repr : TAAffixPosition → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprTAAffixPosition : Repr TAAffixPosition

Equations

• Phenomena.TenseAspect.Typology.instReprTAAffixPosition = { reprPrec := Phenomena.TenseAspect.Typology.instReprTAAffixPosition.repr }

def Phenomena.TenseAspect.Typology.TAAffixPosition.hasAffixes : TAAffixPosition → Bool

Whether a language has any tense-aspect affixation.

Equations

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

structure Phenomena.TenseAspect.Typology.TAProfile : Type

A language's tense-aspect typological profile across WALS chapters 65-69.

• language : String

  Language name

• iso : String

  ISO 639-3 code

• family : String

  Language family

• aspect : AspectMarking

  WALS Ch 65: perfective/imperfective aspect

• past : PastMarking

  WALS Ch 66: past tense marking

• future : FutureMarking

  WALS Ch 67: inflectional future

• perfect : PerfectType

  WALS Ch 68: perfect category

• affixPosition : TAAffixPosition

  WALS Ch 69: tense-aspect affix position

instance Phenomena.TenseAspect.Typology.instReprTAProfile : Repr TAProfile

Equations

• Phenomena.TenseAspect.Typology.instReprTAProfile = { reprPrec := Phenomena.TenseAspect.Typology.instReprTAProfile.repr }

def Phenomena.TenseAspect.Typology.instReprTAProfile.repr : TAProfile → Nat → Std.Format

Equations

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

def Phenomena.TenseAspect.Typology.instDecidableEqTAProfile.decEq (x✝ x✝¹ : TAProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Typology.instDecidableEqTAProfile : DecidableEq TAProfile

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqTAProfile = Phenomena.TenseAspect.Typology.instDecidableEqTAProfile.decEq

instance Phenomena.TenseAspect.Typology.instBEqTAProfile : BEq TAProfile

Equations

• Phenomena.TenseAspect.Typology.instBEqTAProfile = { beq := Phenomena.TenseAspect.Typology.instBEqTAProfile.beq }

def Phenomena.TenseAspect.Typology.instBEqTAProfile.beq : TAProfile → TAProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Typology.instBEqTAProfile.beq x✝¹ x✝ = false

structure Phenomena.TenseAspect.Typology.Ch65Counts : Type

WALS Ch 65 distribution: perfective/imperfective aspect.

• grammatical : Nat
• noMarking : Nat

def Phenomena.TenseAspect.Typology.instReprCh65Counts.repr : Ch65Counts → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprCh65Counts : Repr Ch65Counts

Equations

• Phenomena.TenseAspect.Typology.instReprCh65Counts = { reprPrec := Phenomena.TenseAspect.Typology.instReprCh65Counts.repr }

instance Phenomena.TenseAspect.Typology.instDecidableEqCh65Counts : DecidableEq Ch65Counts

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqCh65Counts = Phenomena.TenseAspect.Typology.instDecidableEqCh65Counts.decEq

def Phenomena.TenseAspect.Typology.instDecidableEqCh65Counts.decEq (x✝ x✝¹ : Ch65Counts) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Typology.instBEqCh65Counts : BEq Ch65Counts

Equations

• Phenomena.TenseAspect.Typology.instBEqCh65Counts = { beq := Phenomena.TenseAspect.Typology.instBEqCh65Counts.beq }

def Phenomena.TenseAspect.Typology.instBEqCh65Counts.beq : Ch65Counts → Ch65Counts → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqCh65Counts.beq { grammatical := a, noMarking := a_1 } { grammatical := b, noMarking := b_1 } = (a == b && a_1 == b_1)
• Phenomena.TenseAspect.Typology.instBEqCh65Counts.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Typology.ch65Dist : Ch65Counts

Equations

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

structure Phenomena.TenseAspect.Typology.Ch66Counts : Type

WALS Ch 66 distribution: past tense.

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

def Phenomena.TenseAspect.Typology.instReprCh66Counts.repr : Ch66Counts → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprCh66Counts : Repr Ch66Counts

Equations

• Phenomena.TenseAspect.Typology.instReprCh66Counts = { reprPrec := Phenomena.TenseAspect.Typology.instReprCh66Counts.repr }

instance Phenomena.TenseAspect.Typology.instDecidableEqCh66Counts : DecidableEq Ch66Counts

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqCh66Counts = Phenomena.TenseAspect.Typology.instDecidableEqCh66Counts.decEq

def Phenomena.TenseAspect.Typology.instDecidableEqCh66Counts.decEq (x✝ x✝¹ : Ch66Counts) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Typology.instBEqCh66Counts : BEq Ch66Counts

Equations

• Phenomena.TenseAspect.Typology.instBEqCh66Counts = { beq := Phenomena.TenseAspect.Typology.instBEqCh66Counts.beq }

def Phenomena.TenseAspect.Typology.instBEqCh66Counts.beq : Ch66Counts → Ch66Counts → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Typology.instBEqCh66Counts.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Typology.ch66Dist : Ch66Counts

Equations

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

structure Phenomena.TenseAspect.Typology.Ch67Counts : Type

WALS Ch 67 distribution: inflectional future.

• inflectional : Nat
• noInflectional : Nat

instance Phenomena.TenseAspect.Typology.instReprCh67Counts : Repr Ch67Counts

Equations

• Phenomena.TenseAspect.Typology.instReprCh67Counts = { reprPrec := Phenomena.TenseAspect.Typology.instReprCh67Counts.repr }

def Phenomena.TenseAspect.Typology.instReprCh67Counts.repr : Ch67Counts → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instDecidableEqCh67Counts : DecidableEq Ch67Counts

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqCh67Counts = Phenomena.TenseAspect.Typology.instDecidableEqCh67Counts.decEq

def Phenomena.TenseAspect.Typology.instDecidableEqCh67Counts.decEq (x✝ x✝¹ : Ch67Counts) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Typology.instBEqCh67Counts : BEq Ch67Counts

Equations

• Phenomena.TenseAspect.Typology.instBEqCh67Counts = { beq := Phenomena.TenseAspect.Typology.instBEqCh67Counts.beq }

def Phenomena.TenseAspect.Typology.instBEqCh67Counts.beq : Ch67Counts → Ch67Counts → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqCh67Counts.beq { inflectional := a, noInflectional := a_1 } { inflectional := b, noInflectional := b_1 } = (a == b && a_1 == b_1)
• Phenomena.TenseAspect.Typology.instBEqCh67Counts.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Typology.ch67Dist : Ch67Counts

Equations

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

structure Phenomena.TenseAspect.Typology.Ch68Counts : Type

WALS Ch 68 distribution: the perfect.

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

def Phenomena.TenseAspect.Typology.instReprCh68Counts.repr : Ch68Counts → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprCh68Counts : Repr Ch68Counts

Equations

• Phenomena.TenseAspect.Typology.instReprCh68Counts = { reprPrec := Phenomena.TenseAspect.Typology.instReprCh68Counts.repr }

instance Phenomena.TenseAspect.Typology.instDecidableEqCh68Counts : DecidableEq Ch68Counts

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqCh68Counts = Phenomena.TenseAspect.Typology.instDecidableEqCh68Counts.decEq

def Phenomena.TenseAspect.Typology.instDecidableEqCh68Counts.decEq (x✝ x✝¹ : Ch68Counts) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.TenseAspect.Typology.instBEqCh68Counts.beq : Ch68Counts → Ch68Counts → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Typology.instBEqCh68Counts.beq x✝¹ x✝ = false

instance Phenomena.TenseAspect.Typology.instBEqCh68Counts : BEq Ch68Counts

Equations

• Phenomena.TenseAspect.Typology.instBEqCh68Counts = { beq := Phenomena.TenseAspect.Typology.instBEqCh68Counts.beq }

def Phenomena.TenseAspect.Typology.ch68Dist : Ch68Counts

Equations

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

structure Phenomena.TenseAspect.Typology.Ch69Counts : Type

WALS Ch 69 distribution: position of tense-aspect affixes.

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

def Phenomena.TenseAspect.Typology.instReprCh69Counts.repr : Ch69Counts → Nat → Std.Format

Equations

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

instance Phenomena.TenseAspect.Typology.instReprCh69Counts : Repr Ch69Counts

Equations

• Phenomena.TenseAspect.Typology.instReprCh69Counts = { reprPrec := Phenomena.TenseAspect.Typology.instReprCh69Counts.repr }

instance Phenomena.TenseAspect.Typology.instDecidableEqCh69Counts : DecidableEq Ch69Counts

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqCh69Counts = Phenomena.TenseAspect.Typology.instDecidableEqCh69Counts.decEq

def Phenomena.TenseAspect.Typology.instDecidableEqCh69Counts.decEq (x✝ x✝¹ : Ch69Counts) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Typology.instBEqCh69Counts : BEq Ch69Counts

Equations

• Phenomena.TenseAspect.Typology.instBEqCh69Counts = { beq := Phenomena.TenseAspect.Typology.instBEqCh69Counts.beq }

def Phenomena.TenseAspect.Typology.instBEqCh69Counts.beq : Ch69Counts → Ch69Counts → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Typology.instBEqCh69Counts.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Typology.ch69Dist : Ch69Counts

Equations

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

theorem Phenomena.TenseAspect.Typology.ch65_total : ch65Dist.grammatical + ch65Dist.noMarking = 222

Ch 65 sample size: 222 languages.

theorem Phenomena.TenseAspect.Typology.ch66_total : ch66Dist.markedNoRemoteness + ch66Dist.markedRemoteness2_3 + ch66Dist.markedRemoteness4plus + ch66Dist.noMarking = 222

Ch 66 sample size: 222 languages.

theorem Phenomena.TenseAspect.Typology.ch67_total : ch67Dist.inflectional + ch67Dist.noInflectional = 222

Ch 67 sample size: 222 languages.

theorem Phenomena.TenseAspect.Typology.ch68_total : ch68Dist.fromPossessive + ch68Dist.fromFinishAlready + ch68Dist.otherPerfect + ch68Dist.noPerfect = 222

Ch 68 sample size: 222 languages.

theorem Phenomena.TenseAspect.Typology.ch69_total : ch69Dist.prefixing + ch69Dist.suffixing + ch69Dist.tonal + ch69Dist.mixed + ch69Dist.noInflection = 1131

Ch 69 sample size: 1131 languages.

def Phenomena.TenseAspect.Typology.english : TAProfile

English (Indo-European, Germanic). Periphrastic perfective (simple past vs progressive), inflectional past, no inflectional future (uses "will" — periphrastic), 'have'-perfect, suffixing (-ed, -ing).

Equations

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

def Phenomena.TenseAspect.Typology.russian : TAProfile

Russian (Indo-European, Slavic). Robust perfective/imperfective (typically via prefixation), inflectional past, no inflectional future (periphrastic "budet" + infinitive for imperfective future, perfective present = future), no perfect, suffixing (-l, -la for past).

Equations

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

def Phenomena.TenseAspect.Typology.french : TAProfile

French (Indo-European, Romance). Imparfait/passé composé aspect distinction, inflectional past (passé simple), inflectional future (-ai, -as, -a...), 'have'-perfect (avoir + past participle), suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.spanish : TAProfile

Spanish (Indo-European, Romance). Imperfecto/preterito (imperfective/perfective), inflectional past and future, 'have'-perfect (haber + participle), suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.finnish : TAProfile

Finnish (Uralic). No grammatical perfective/imperfective, inflectional past (-i), no inflectional future (present tense used for future reference), perfect (on + past participle, 'be'-type), suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.turkish : TAProfile

Turkish (Turkic). Perfective/imperfective (-di vs -iyor), inflectional past, inflectional future (-ecek), other perfect (-miş, from evidential/inferential), suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.japanese : TAProfile

Japanese (Japonic). Perfective/imperfective (ta-form vs te-iru), inflectional past (-ta, -da), no inflectional future, no distinct perfect, suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.korean : TAProfile

Korean (Koreanic). Perfective/imperfective (-었- vs -고 있-), inflectional past (-었-), inflectional future (-겠-), no distinct perfect, suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.mandarin : TAProfile

Mandarin Chinese (Sino-Tibetan). Perfective le/guo, but these are particles (not inflectional), no inflectional past, no inflectional future, no distinct perfect, no tense-aspect inflection. Quintessential isolating language.

Equations

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

def Phenomena.TenseAspect.Typology.vietnamese : TAProfile

Vietnamese (Austroasiatic). No grammatical perfective/imperfective, no inflectional past, no inflectional future, no perfect. Tense-aspect expressed by separate particles (da, se). Part of the South-East Asian isolating area.

Equations

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

def Phenomena.TenseAspect.Typology.thai : TAProfile

Thai (Tai-Kadai). No grammatical perfective/imperfective, no inflectional past, no inflectional future, no perfect. South-East Asian isolating type.

Equations

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

def Phenomena.TenseAspect.Typology.indonesian : TAProfile

Indonesian (Austronesian, Malayo-Polynesian). No grammatical aspect, no past marking, no inflectional future, no perfect. Classic example of tenselessness (air itu dingin = 'the water is/was cold'). Minor tense-aspect suffix exists (-i repetitive), but marginal.

Equations

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

def Phenomena.TenseAspect.Typology.swahili : TAProfile

Swahili (Niger-Congo, Bantu). Perfective/imperfective (-li-, -na-), past marking, no inflectional future, other perfect (-me-), prefixing (T/A markers are verbal prefixes).

Equations

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

def Phenomena.TenseAspect.Typology.yoruba : TAProfile

Yoruba (Niger-Congo, Atlantic-Congo). Perfective/imperfective distinction, no past tense marking, no inflectional future, perfect from 'already' (ti), no tense-aspect inflection (preverbal particles).

Equations

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

def Phenomena.TenseAspect.Typology.hindi : TAProfile

Hindi (Indo-European, Indo-Aryan). Perfective/imperfective (-aa, -taa), inflectional past, inflectional future (-egaa), other perfect, suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.arabic : TAProfile

Arabic (Egyptian) (Afro-Asiatic, Semitic). Perfective/imperfective (katab/yiktib), inflectional past (perfective form encodes past), no inflectional future (uses preverbal particles), no distinct perfect, suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.quechua : TAProfile

Quechua (Quechuan). No grammatical perfective/imperfective, inflectional past with 2-3 remoteness distinctions (direct vs indirect past), inflectional future (-saq), other perfect (-sqa resultative), suffixing.

Equations

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

def Phenomena.TenseAspect.Typology.tagalog : TAProfile

Tagalog (Austronesian, Malayo-Polynesian). Perfective/imperfective (completed vs contemplated aspect), no inflectional past or future (aspect-based system), no distinct perfect, prefixing (mag-, nag-, -um- etc.).

Equations

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

def Phenomena.TenseAspect.Typology.lango : TAProfile

Lango (Nilotic, Eastern Sudanic). Perfective/imperfective/progressive marked primarily by tone, past tense marking, no inflectional future, other perfect, tonal T/A marking.

Equations

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

def Phenomena.TenseAspect.Typology.allLanguages : List TAProfile

All languages in the sample.

Equations

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

theorem Phenomena.TenseAspect.Typology.russian_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "rus") = some russian.aspect

theorem Phenomena.TenseAspect.Typology.french_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "fre") = some french.aspect

theorem Phenomena.TenseAspect.Typology.spanish_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "spa") = some spanish.aspect

theorem Phenomena.TenseAspect.Typology.finnish_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "fin") = some finnish.aspect

theorem Phenomena.TenseAspect.Typology.turkish_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "tur") = some turkish.aspect

theorem Phenomena.TenseAspect.Typology.korean_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "kor") = some korean.aspect

theorem Phenomena.TenseAspect.Typology.mandarin_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "mnd") = some mandarin.aspect

theorem Phenomena.TenseAspect.Typology.vietnamese_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "vie") = some vietnamese.aspect

theorem Phenomena.TenseAspect.Typology.thai_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "tha") = some thai.aspect

theorem Phenomena.TenseAspect.Typology.indonesian_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "ind") = some indonesian.aspect

theorem Phenomena.TenseAspect.Typology.hindi_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "hin") = some hindi.aspect

theorem Phenomena.TenseAspect.Typology.arabic_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "aeg") = some arabic.aspect

theorem Phenomena.TenseAspect.Typology.tagalog_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "tag") = some tagalog.aspect

theorem Phenomena.TenseAspect.Typology.lango_ch65 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F65A.PerfectiveImperfective) => Phenomena.TenseAspect.Typology.fromWALS65A✝ x.value) (Core.WALS.F65A.lookup "lan") = some lango.aspect

theorem Phenomena.TenseAspect.Typology.english_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "eng") = some english.past

theorem Phenomena.TenseAspect.Typology.russian_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "rus") = some russian.past

theorem Phenomena.TenseAspect.Typology.french_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "fre") = some french.past

theorem Phenomena.TenseAspect.Typology.spanish_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "spa") = some spanish.past

theorem Phenomena.TenseAspect.Typology.finnish_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "fin") = some finnish.past

theorem Phenomena.TenseAspect.Typology.turkish_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "tur") = some turkish.past

theorem Phenomena.TenseAspect.Typology.japanese_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "jpn") = some japanese.past

theorem Phenomena.TenseAspect.Typology.korean_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "kor") = some korean.past

theorem Phenomena.TenseAspect.Typology.mandarin_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "mnd") = some mandarin.past

theorem Phenomena.TenseAspect.Typology.vietnamese_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "vie") = some vietnamese.past

theorem Phenomena.TenseAspect.Typology.thai_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "tha") = some thai.past

theorem Phenomena.TenseAspect.Typology.indonesian_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "ind") = some indonesian.past

theorem Phenomena.TenseAspect.Typology.swahili_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "swa") = some swahili.past

theorem Phenomena.TenseAspect.Typology.yoruba_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "yor") = some yoruba.past

theorem Phenomena.TenseAspect.Typology.hindi_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "hin") = some hindi.past

theorem Phenomena.TenseAspect.Typology.arabic_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "aeg") = some arabic.past

theorem Phenomena.TenseAspect.Typology.tagalog_ch66 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F66A.PastTenseType) => Phenomena.TenseAspect.Typology.fromWALS66A✝ x.value) (Core.WALS.F66A.lookup "tag") = some tagalog.past

theorem Phenomena.TenseAspect.Typology.english_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "eng") = some english.future

theorem Phenomena.TenseAspect.Typology.russian_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "rus") = some russian.future

theorem Phenomena.TenseAspect.Typology.french_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "fre") = some french.future

theorem Phenomena.TenseAspect.Typology.spanish_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "spa") = some spanish.future

theorem Phenomena.TenseAspect.Typology.finnish_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "fin") = some finnish.future

theorem Phenomena.TenseAspect.Typology.turkish_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "tur") = some turkish.future

theorem Phenomena.TenseAspect.Typology.japanese_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "jpn") = some japanese.future

theorem Phenomena.TenseAspect.Typology.mandarin_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "mnd") = some mandarin.future

theorem Phenomena.TenseAspect.Typology.vietnamese_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "vie") = some vietnamese.future

theorem Phenomena.TenseAspect.Typology.thai_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "tha") = some thai.future

theorem Phenomena.TenseAspect.Typology.indonesian_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "ind") = some indonesian.future

theorem Phenomena.TenseAspect.Typology.hindi_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "hin") = some hindi.future

theorem Phenomena.TenseAspect.Typology.yoruba_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "yor") = some yoruba.future

theorem Phenomena.TenseAspect.Typology.lango_ch67 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F67A.FutureTenseType) => Phenomena.TenseAspect.Typology.fromWALS67A✝ x.value) (Core.WALS.F67A.lookup "lan") = some lango.future

theorem Phenomena.TenseAspect.Typology.english_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "eng") = some english.perfect

theorem Phenomena.TenseAspect.Typology.russian_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "rus") = some russian.perfect

theorem Phenomena.TenseAspect.Typology.french_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "fre") = some french.perfect

theorem Phenomena.TenseAspect.Typology.spanish_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "spa") = some spanish.perfect

theorem Phenomena.TenseAspect.Typology.finnish_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "fin") = some finnish.perfect

theorem Phenomena.TenseAspect.Typology.japanese_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "jpn") = some japanese.perfect

theorem Phenomena.TenseAspect.Typology.korean_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "kor") = some korean.perfect

theorem Phenomena.TenseAspect.Typology.mandarin_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "mnd") = some mandarin.perfect

theorem Phenomena.TenseAspect.Typology.swahili_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "swa") = some swahili.perfect

theorem Phenomena.TenseAspect.Typology.yoruba_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "yor") = some yoruba.perfect

theorem Phenomena.TenseAspect.Typology.hindi_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "hin") = some hindi.perfect

theorem Phenomena.TenseAspect.Typology.arabic_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "aeg") = some arabic.perfect

theorem Phenomena.TenseAspect.Typology.tagalog_ch68 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F68A.PerfectType) => Phenomena.TenseAspect.Typology.fromWALS68A✝ x.value) (Core.WALS.F68A.lookup "tag") = some tagalog.perfect

theorem Phenomena.TenseAspect.Typology.english_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "eng") = some english.affixPosition

theorem Phenomena.TenseAspect.Typology.french_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "fre") = some french.affixPosition

theorem Phenomena.TenseAspect.Typology.spanish_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "spa") = some spanish.affixPosition

theorem Phenomena.TenseAspect.Typology.finnish_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "fin") = some finnish.affixPosition

theorem Phenomena.TenseAspect.Typology.turkish_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "tur") = some turkish.affixPosition

theorem Phenomena.TenseAspect.Typology.japanese_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "jpn") = some japanese.affixPosition

theorem Phenomena.TenseAspect.Typology.korean_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "kor") = some korean.affixPosition

theorem Phenomena.TenseAspect.Typology.vietnamese_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "vie") = some vietnamese.affixPosition

theorem Phenomena.TenseAspect.Typology.thai_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "tha") = some thai.affixPosition

theorem Phenomena.TenseAspect.Typology.indonesian_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "ind") = some indonesian.affixPosition

theorem Phenomena.TenseAspect.Typology.swahili_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "swa") = some swahili.affixPosition

theorem Phenomena.TenseAspect.Typology.yoruba_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "yor") = some yoruba.affixPosition

theorem Phenomena.TenseAspect.Typology.hindi_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "hin") = some hindi.affixPosition

theorem Phenomena.TenseAspect.Typology.tagalog_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "tag") = some tagalog.affixPosition

theorem Phenomena.TenseAspect.Typology.lango_ch69 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F69A.TenseAspectAffixPosition) => Phenomena.TenseAspect.Typology.fromWALS69A✝ x.value) (Core.WALS.F69A.lookup "lan") = some lango.affixPosition

def Phenomena.TenseAspect.Typology.ch66TotalWithPast : Nat

Total languages with past marking in Ch 66.

Equations

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

theorem Phenomena.TenseAspect.Typology.past_marking_majority : ch66TotalWithPast > ch66Dist.noMarking

A majority (134/222 = 60%) of WALS Ch 66 languages have past marking.

theorem Phenomena.TenseAspect.Typology.suffix_dominant_over_prefix : ch69Dist.suffixing > 4 * ch69Dist.prefixing

Suffixes outnumber prefixes by more than 4:1 (667 vs 153).

theorem Phenomena.TenseAspect.Typology.suffix_most_common : ch69Dist.suffixing > ch69Dist.prefixing ∧ ch69Dist.suffixing > ch69Dist.tonal ∧ ch69Dist.suffixing > ch69Dist.mixed ∧ ch69Dist.suffixing > ch69Dist.noInflection

Suffixing is the most common T/A strategy overall.

theorem Phenomena.TenseAspect.Typology.suffix_absolute_majority : ch69Dist.suffixing * 2 > ch69Dist.prefixing + ch69Dist.suffixing + ch69Dist.tonal + ch69Dist.mixed + ch69Dist.noInflection

Suffixes account for more than half of all languages in Ch 69.

def Phenomena.TenseAspect.Typology.hasAspectAndPast (p : TAProfile) : Bool

In the sample, languages with BOTH aspect and past marking outnumber languages with ONLY one of the two.

@cite{dahl-velupillai-2013}: "there are considerably more languages in the sample that have both the aspectual and the temporal categories, or neither of the alternatives, than have one only."

Equations

• Phenomena.TenseAspect.Typology.hasAspectAndPast p = (p.aspect == Phenomena.TenseAspect.Typology.AspectMarking.grammatical && p.past.hasMarking)

def Phenomena.TenseAspect.Typology.hasAspectOnly (p : TAProfile) : Bool

Equations

• Phenomena.TenseAspect.Typology.hasAspectOnly p = (p.aspect == Phenomena.TenseAspect.Typology.AspectMarking.grammatical && !p.past.hasMarking)

def Phenomena.TenseAspect.Typology.hasPastOnly (p : TAProfile) : Bool

Equations

• Phenomena.TenseAspect.Typology.hasPastOnly p = (p.aspect != Phenomena.TenseAspect.Typology.AspectMarking.grammatical && p.past.hasMarking)

def Phenomena.TenseAspect.Typology.hasNeitherAspectNorPast (p : TAProfile) : Bool

Equations

• Phenomena.TenseAspect.Typology.hasNeitherAspectNorPast p = (p.aspect != Phenomena.TenseAspect.Typology.AspectMarking.grammatical && !p.past.hasMarking)

theorem Phenomena.TenseAspect.Typology.both_exceeds_aspect_only : (List.filter hasAspectAndPast allLanguages).length > (List.filter hasAspectOnly allLanguages).length

In our sample: more languages have both aspect+past than aspect-only.

theorem Phenomena.TenseAspect.Typology.both_exceeds_past_only : (List.filter hasAspectAndPast allLanguages).length > (List.filter hasPastOnly allLanguages).length

In our sample: more languages have both aspect+past than past-only.

def Phenomena.TenseAspect.Typology.lacksMajorTAGrams (p : TAProfile) : Bool

Whether a language lacks all three major T/A gram types from Chs 65-67 (no aspect, no past, no future). This is the hallmark of the South-East Asian isolating cluster.

Equations

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

theorem Phenomena.TenseAspect.Typology.se_asian_isolating_cluster : lacksMajorTAGrams vietnamese = true ∧ lacksMajorTAGrams thai = true ∧ lacksMajorTAGrams indonesian = true

Vietnamese, Thai, and Indonesian all lack the three major T/A gram types: no grammaticalized perfective/imperfective, no past marking, no inflectional future.

@cite{dahl-velupillai-2013}: "The languages in this area lack not only past tenses but also marking of the imperfective/perfective distinction and inflectional futures."

Note: Indonesian has a minor repetitive suffix (-i) and so WALS classifies it as having T/A suffixes, but it lacks the major T/A categories.

theorem Phenomena.TenseAspect.Typology.future_near_even_split : ch67Dist.inflectional + ch67Dist.noInflectional = 222 ∧ ch67Dist.inflectional > 100 ∧ ch67Dist.noInflectional > 100

Inflectional future is approximately 50/50 in Ch 67 (110 vs 112). Neither value constitutes a strong majority.

theorem Phenomena.TenseAspect.Typology.have_perfect_rare : ch68Dist.fromPossessive < 10

'Have'-perfects (from possessive constructions) are extremely rare cross-linguistically — only 7 out of 222 languages. They are restricted almost exclusively to western Europe.

theorem Phenomena.TenseAspect.Typology.no_perfect_majority : ch68Dist.noPerfect > ch68Dist.fromPossessive + ch68Dist.fromFinishAlready + ch68Dist.otherPerfect

Most languages lack a distinct perfect category entirely.

theorem Phenomena.TenseAspect.Typology.aspect_languages_mostly_have_past : have withAspect := List.filter (fun (x : TAProfile) => x.aspect == AspectMarking.grammatical) allLanguages; have withAspectAndPast := List.filter (fun (x : TAProfile) => x.past.hasMarking) withAspect; withAspectAndPast.length > withAspect.length / 2

Among languages in our sample with grammatical perfective/imperfective aspect, the majority also have past tense marking.

This supports Dahl & Velupillai's observation that aspect and tense tend to co-occur rather than being alternatives.

theorem Phenomena.TenseAspect.Typology.tone_ta_rare : ch69Dist.tonal < 15

Tone as the primary tense-aspect strategy is extremely rare (13/1131).

theorem Phenomena.TenseAspect.Typology.tone_in_sample : (List.filter (fun (x : TAProfile) => x.affixPosition == TAAffixPosition.tonal) allLanguages).length = 1

In our sample, only Lango uses tone as the primary T/A strategy.

theorem Phenomena.TenseAspect.Typology.remoteness_uncommon : ch66Dist.markedNoRemoteness > ch66Dist.markedRemoteness2_3 + ch66Dist.markedRemoteness4plus

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

theorem Phenomena.TenseAspect.Typology.extreme_remoteness_very_rare : ch66Dist.markedRemoteness4plus = 2

theorem Phenomena.TenseAspect.Typology.finish_perfect_more_common_than_have : ch68Dist.fromFinishAlready > ch68Dist.fromPossessive

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

def Phenomena.TenseAspect.Typology.lacksAllTA (p : TAProfile) : Bool

Languages in our sample that lack ALL four T/A categories (no aspect, no past, no future, no perfect).

Equations

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

theorem Phenomena.TenseAspect.Typology.ta_empty_nonempty : (List.filter lacksAllTA allLanguages).length ≥ 2

There exist at least 2 languages in our sample with no T/A categories.

theorem Phenomena.TenseAspect.Typology.ta_empty_and_no_inflection : have fullyIsolating := List.filter (fun (x : TAProfile) => x.affixPosition == TAAffixPosition.noInflection) (List.filter lacksAllTA allLanguages); fullyIsolating.length ≥ 2

Languages that lack all four T/A categories AND have no T/A inflection form the core of the South-East Asian isolating cluster.

This matches the pattern described by @cite{dahl-velupillai-2013}: the same languages that lack tense and aspect grams are the isolating languages that lack inflectional morphology.

Note: Indonesian has a minor repetitive suffix (-i) in WALS, so it has lacksAllTA but not noInflection. Vietnamese and Thai have both.

inductive Phenomena.TenseAspect.Typology.EvidentialityCoding : Type

WALS Ch 78: How evidentiality is coded in the language.

"Evidentiality" here means grammaticalized marking of information source. Languages differ in whether evidentiality is part of the tense system, expressed by verbal affixes, clitics, particles, or not grammaticalized.

• none : EvidentialityCoding

  No grammatical evidentiality

• partOfTense : EvidentialityCoding

  Evidentiality is part of the tense paradigm (e.g., Turkish -miş)

• verbalAffix : EvidentialityCoding

  Evidentiality marked by verbal affix

• clitic : EvidentialityCoding

  Evidentiality marked by clitic

• particle : EvidentialityCoding

  Evidentiality marked by particle

• other : EvidentialityCoding

  Other strategy

instance Phenomena.TenseAspect.Typology.instDecidableEqEvidentialityCoding : DecidableEq EvidentialityCoding

Equations

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

def Phenomena.TenseAspect.Typology.instBEqEvidentialityCoding.beq : EvidentialityCoding → EvidentialityCoding → Bool

Equations

• Phenomena.TenseAspect.Typology.instBEqEvidentialityCoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Typology.instBEqEvidentialityCoding : BEq EvidentialityCoding

Equations

• Phenomena.TenseAspect.Typology.instBEqEvidentialityCoding = { beq := Phenomena.TenseAspect.Typology.instBEqEvidentialityCoding.beq }

instance Phenomena.TenseAspect.Typology.instReprEvidentialityCoding : Repr EvidentialityCoding

Equations

• Phenomena.TenseAspect.Typology.instReprEvidentialityCoding = { reprPrec := Phenomena.TenseAspect.Typology.instReprEvidentialityCoding.repr }

def Phenomena.TenseAspect.Typology.instReprEvidentialityCoding.repr : EvidentialityCoding → Nat → Std.Format

Equations

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

def Phenomena.TenseAspect.Typology.EvidentialityCoding.hasEvidentiality : EvidentialityCoding → Bool

Whether a language has any grammatical evidentiality.

Equations

• Phenomena.TenseAspect.Typology.EvidentialityCoding.none.hasEvidentiality = false
• x✝.hasEvidentiality = true

structure Phenomena.TenseAspect.Typology.TAMEProfile : Type

A language's typological profile across the full TAME space: tense (Ch 66–67), aspect (Ch 65), perfect (Ch 68), morphological position (Ch 69), and evidentiality (Ch 78).

Extends TAProfile with the evidentiality dimension.

• language : String

  Language name

• iso : String

  ISO 639-3 code

• family : String

  Language family

• aspect : AspectMarking

  WALS Ch 65: perfective/imperfective aspect

• past : PastMarking

  WALS Ch 66: past tense marking

• future : FutureMarking

  WALS Ch 67: inflectional future

• perfect : PerfectType

  WALS Ch 68: perfect category

• affixPosition : TAAffixPosition

  WALS Ch 69: tense-aspect affix position

• evidentiality : EvidentialityCoding

  WALS Ch 78: coding of evidentiality

instance Phenomena.TenseAspect.Typology.instReprTAMEProfile : Repr TAMEProfile

Equations

• Phenomena.TenseAspect.Typology.instReprTAMEProfile = { reprPrec := Phenomena.TenseAspect.Typology.instReprTAMEProfile.repr }

def Phenomena.TenseAspect.Typology.instReprTAMEProfile.repr : TAMEProfile → Nat → Std.Format

Equations

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

def Phenomena.TenseAspect.Typology.instDecidableEqTAMEProfile.decEq (x✝ x✝¹ : TAMEProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.TenseAspect.Typology.instDecidableEqTAMEProfile : DecidableEq TAMEProfile

Equations

• Phenomena.TenseAspect.Typology.instDecidableEqTAMEProfile = Phenomena.TenseAspect.Typology.instDecidableEqTAMEProfile.decEq

def Phenomena.TenseAspect.Typology.instBEqTAMEProfile.beq : TAMEProfile → TAMEProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Typology.instBEqTAMEProfile.beq x✝¹ x✝ = false

instance Phenomena.TenseAspect.Typology.instBEqTAMEProfile : BEq TAMEProfile

Equations

• Phenomena.TenseAspect.Typology.instBEqTAMEProfile = { beq := Phenomena.TenseAspect.Typology.instBEqTAMEProfile.beq }

def Phenomena.TenseAspect.Typology.turkishTAME : TAMEProfile

Turkish (Turkic). Evidentiality is part of the tense paradigm: -miş marks indirect evidence (hearsay/inference) vs -di (direct).

Equations

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

def Phenomena.TenseAspect.Typology.quechuaTAME : TAMEProfile

Quechua (Quechuan). Evidentiality via verbal suffixes: -mi (direct), -si (hearsay), -chá (conjecture).

Equations

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

def Phenomena.TenseAspect.Typology.koreanTAME : TAMEProfile

Korean (Koreanic). Evidentiality via verbal suffixes: -te (retrospective evidential), -ney (contemporaneous evidential). @cite{cumming-2026} analyzes these as tense-evidential interactions.

Equations

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

def Phenomena.TenseAspect.Typology.englishTAME : TAMEProfile

English (Indo-European). No grammatical evidentiality. Evidential distinctions are expressed lexically ("apparently", "I heard that..."), not grammatically.

Equations

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

def Phenomena.TenseAspect.Typology.mandarinTAME : TAMEProfile

Mandarin Chinese (Sino-Tibetan). No grammatical evidentiality, no tense-aspect inflection. Isolating type.

Equations

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

def Phenomena.TenseAspect.Typology.allTAMELanguages : List TAMEProfile

All TAME-profiled languages.

Equations

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

def Phenomena.TenseAspect.Typology.TAMEProfile.hasTenseOrAspect (p : TAMEProfile) : Bool

Whether a TAMEProfile has any tense or aspect marking (aspect, past, or future).

Equations

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

theorem Phenomena.TenseAspect.Typology.evidential_implies_tense_aspect : ((List.filter (fun (x : TAMEProfile) => x.evidentiality.hasEvidentiality) allTAMELanguages).all fun (x : TAMEProfile) => x.hasTenseOrAspect) = true

In our TAME sample, every language with grammatical evidentiality also has tense or aspect marking.

This reinforces the "no tense-vs-aspect divide" finding (Generalization 3) by showing that evidentiality also clusters with tense/aspect marking rather than replacing it.