Documentation

Linglib.Typology.Case

Case typology — WALS substrate (Chapters 49–52) #

@cite{dryer-haspelmath-2013} @cite{iggesen-2013} @cite{stolz-veselinova-2013}

Theory-neutral case-typology substrate distilled from four WALS chapters, in the same Linglib/Typology/{Domain}.lean mould as WordOrder.lean, Adposition.lean, etc.:

Ch 49 (Iggesen 2013): Number of Cases — five-bin classification of morphological case inventory size, plus the noMorphologicalCaseMarking cell.
Ch 50 (Iggesen 2013): Asymmetrical Case-Marking — Iggesen's actual five-way WALS partition (symmetrical, additiveQuantitativelyAsymmetrical, subtractiveQuantitativelyAsymmetrical, qualitativelyAsymmetrical, syncretismInRelevantNpTypes). Note: an earlier Phenomena/Case/Typology.lean file silently re-coded this dimension in Aissen-friendly conditioning-factor categories (animacyOnly / definitenessOnly / pronounOnly / etc.); that re-coding was deleted in the dissolution because (a) it didn't match the WALS data the same chapter referenced, (b) it served only a per-language hand-curated sample that was itself unsourced, and (c) post-Aissen conditioning-factor analyses live in Studies/Aissen2003.lean and Features/Prominence.lean::DifferentialMarkingProfile, not in substrate.
Ch 51 (Iggesen 2013): Position of Case Affixes — suffix / prefix / tone / mixed.
Ch 52 (Stolz & Veselinova 2013): Comitatives & Instrumentals — identity vs differentiation vs mixed.

The substrate exposes:

Enum types per chapter (CaseCount, AsymmetricalCaseMarking, CaseAffixPosition, ComitativeInstrumental)
Convenience helpers (hasDCM, hasBoundCase, isSyncretic, etc.)
Forward maps from the generated WALS feature types to these enums where a clean mapping exists (fromWALS49A); sparse where Iggesen's WALS bins don't align cleanly (Ch 50's WALS-vs-Aissen issue noted above)
WALS distributional facts proved by native_decide over Data.WALS.F{49,50,51,52}A.allData

No Fragment imports (substrate discipline). Theory-specific apparatus (Aissen 2003 OT factorial typology, DeHoop-Malchukov BiOT, Grimm 2011 agentivity lattice, Haspelmath 2021 form-frequency correspondences) lives in Phenomena/Case/Studies/. Abstract-case theory (Marantz 1991, Pesetsky 2013, Caha 2009 nanosyntax, Baker 2015 dependent case, Woolford 1997 lexical case) lives in Linglib/Theories/Syntax/Case/ over a different ontology and does NOT consume this WALS substrate.

inductive Typology.Case.CaseCount :

Number-of-cases categories (WALS Ch 49, @cite{iggesen-2013}).

Languages are classified by the number of morphological case distinctions in their nominal paradigm. WALS additionally distinguishes exclusivelyBorderlineCaseMarking (e.g., English with case only on pronouns) from the noMorphologicalCaseMarking cell, but that distinction is deliberately not collapsed into a single bin here — see fromWALS49A for the explicit none mapping.

none : CaseCount
two : CaseCount
threeFour : CaseCount
fiveSeven : CaseCount
eightNine : CaseCount
tenPlus : CaseCount

Instances For

@[implicit_reducible]

instance Typology.Case.instDecidableEqCaseCount :

DecidableEq CaseCount

Equations

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

def Typology.Case.instReprCaseCount.repr :

CaseCount → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Case.instReprCaseCount :

Equations

Typology.Case.instReprCaseCount = { reprPrec := Typology.Case.instReprCaseCount.repr }

@[implicit_reducible]

instance Typology.Case.instInhabitedCaseCount :

Inhabited CaseCount

Equations

Typology.Case.instInhabitedCaseCount = { default := Typology.Case.instInhabitedCaseCount.default }

def Typology.Case.instInhabitedCaseCount.default :

Equations

Typology.Case.instInhabitedCaseCount.default = Typology.Case.CaseCount.none

Instances For

def Typology.Case.CaseCount.lowerBound :

CaseCount → Nat

Numeric lower bound for each CaseCount category.

Equations

Instances For

def Typology.Case.CaseCount.contains (cc : CaseCount) (n : Nat) :

Bool

Whether a raw case count falls in a given CaseCount category.

Equations

Typology.Case.CaseCount.none.contains n = (n == 0)
Typology.Case.CaseCount.two.contains n = (n == 2)
Typology.Case.CaseCount.threeFour.contains n = (decide (n ≥ 3) && decide (n ≤ 4))
Typology.Case.CaseCount.fiveSeven.contains n = (decide (n ≥ 5) && decide (n ≤ 7))
Typology.Case.CaseCount.eightNine.contains n = (decide (n ≥ 8) && decide (n ≤ 9))
Typology.Case.CaseCount.tenPlus.contains n = decide (n ≥ 10)

Instances For

def Typology.Case.fromWALS49A :

Data.WALS.F49A.CaseCount → Option CaseCount

Forward map from the generated WALS Ch 49 type to CaseCount. Iggesen's exclusivelyBorderlineCaseMarking cell (e.g., English with case only on pronouns) has no clean mapping into the size-bin scheme and returns Option.none.

Equations

Instances For

inductive Typology.Case.AsymmetricalCaseMarking :

WALS Ch 50 (Iggesen 2013): Asymmetrical (differential) case-marking typology. Iggesen's actual five-way classification — these are the categories the WALS data carries. Conditioning-factor analyses (animacy / definiteness / pronoun status) are theory-side projections over Features.Prominence.DifferentialMarkingProfile, not substrate.

symmetrical : AsymmetricalCaseMarking
Symmetrical: case marking is uniform across NP types.
additiveQuantitativelyAsymmetrical : AsymmetricalCaseMarking
Additive quantitatively asymmetrical: more case distinctions on some NP types than others.
subtractiveQuantitativelyAsymmetrical : AsymmetricalCaseMarking
Subtractive quantitatively asymmetrical: fewer case distinctions on some NP types.
qualitativelyAsymmetrical : AsymmetricalCaseMarking
Qualitatively asymmetrical: different markers in the same case cell across NP types.
syncretismInRelevantNpTypes : AsymmetricalCaseMarking
Syncretism in relevant NP types: case distinctions collapse on certain NP types.

Instances For

@[implicit_reducible]

instance Typology.Case.instDecidableEqAsymmetricalCaseMarking :

DecidableEq AsymmetricalCaseMarking

Equations

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

def Typology.Case.instReprAsymmetricalCaseMarking.repr :

AsymmetricalCaseMarking → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Case.instReprAsymmetricalCaseMarking :

Repr AsymmetricalCaseMarking

Equations

Typology.Case.instReprAsymmetricalCaseMarking = { reprPrec := Typology.Case.instReprAsymmetricalCaseMarking.repr }

@[implicit_reducible]

instance Typology.Case.instInhabitedAsymmetricalCaseMarking :

Inhabited AsymmetricalCaseMarking

Equations

Typology.Case.instInhabitedAsymmetricalCaseMarking = { default := Typology.Case.instInhabitedAsymmetricalCaseMarking.default }

def Typology.Case.instInhabitedAsymmetricalCaseMarking.default :

AsymmetricalCaseMarking

Equations

Typology.Case.instInhabitedAsymmetricalCaseMarking.default = Typology.Case.AsymmetricalCaseMarking.symmetrical

Instances For

def Typology.Case.AsymmetricalCaseMarking.isAsymmetric :

AsymmetricalCaseMarking → Bool

Whether this Ch 50 value indicates any case-marking asymmetry (everything other than symmetrical).

Equations

Typology.Case.AsymmetricalCaseMarking.symmetrical.isAsymmetric = false
x✝.isAsymmetric = true

Instances For

def Typology.Case.fromWALS50A :

Data.WALS.F50A.AsymmetricalCaseMarking → Option AsymmetricalCaseMarking

Forward map from generated WALS Ch 50 to local enum. The WALS source has a noCaseMarking cell as well (no morphological case at all); we omit it from this enum since asymmetry is undefined when there is no case to be asymmetric about.

Equations

Instances For

inductive Typology.Case.CaseAffixPosition :

Position of case affixes (WALS Ch 51, @cite{iggesen-2013}).

noAffixes : CaseAffixPosition
suffixesOnly : CaseAffixPosition
prefixesOnly : CaseAffixPosition
toneOnly : CaseAffixPosition
bothSuffixPrefix : CaseAffixPosition

Instances For

@[implicit_reducible]

instance Typology.Case.instDecidableEqCaseAffixPosition :

DecidableEq CaseAffixPosition

Equations

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

def Typology.Case.instReprCaseAffixPosition.repr :

CaseAffixPosition → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Case.instReprCaseAffixPosition :

Repr CaseAffixPosition

Equations

Typology.Case.instReprCaseAffixPosition = { reprPrec := Typology.Case.instReprCaseAffixPosition.repr }

def Typology.Case.instInhabitedCaseAffixPosition.default :

CaseAffixPosition

Equations

Typology.Case.instInhabitedCaseAffixPosition.default = Typology.Case.CaseAffixPosition.noAffixes

Instances For

@[implicit_reducible]

instance Typology.Case.instInhabitedCaseAffixPosition :

Inhabited CaseAffixPosition

Equations

Typology.Case.instInhabitedCaseAffixPosition = { default := Typology.Case.instInhabitedCaseAffixPosition.default }

def Typology.Case.CaseAffixPosition.hasBoundCase :

CaseAffixPosition → Bool

Whether this position type involves bound case morphology.

Equations

Typology.Case.CaseAffixPosition.noAffixes.hasBoundCase = false
x✝.hasBoundCase = true

Instances For

def Typology.Case.CaseAffixPosition.hasSuffix :

CaseAffixPosition → Bool

Whether suffixal case marking is present.

Equations

Typology.Case.CaseAffixPosition.suffixesOnly.hasSuffix = true
Typology.Case.CaseAffixPosition.bothSuffixPrefix.hasSuffix = true
x✝.hasSuffix = false

Instances For

inductive Typology.Case.ComitativeInstrumental :

Comitative–instrumental relation (WALS Ch 52, @cite{stolz-veselinova-2013}).

In many languages the marker for 'with X' (comitative: accompaniment) and 'by means of X' (instrumental: means/instrument) is the same morpheme (e.g. Russian instrumental case -om ~ -oj); other languages distinguish them (e.g. Japanese -to vs -de).

identity : ComitativeInstrumental
differentiation : ComitativeInstrumental
mixed : ComitativeInstrumental

Instances For

@[implicit_reducible]

instance Typology.Case.instDecidableEqComitativeInstrumental :

DecidableEq ComitativeInstrumental

Equations

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

def Typology.Case.instReprComitativeInstrumental.repr :

ComitativeInstrumental → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Case.instReprComitativeInstrumental :

Repr ComitativeInstrumental

Equations

Typology.Case.instReprComitativeInstrumental = { reprPrec := Typology.Case.instReprComitativeInstrumental.repr }

def Typology.Case.instInhabitedComitativeInstrumental.default :

ComitativeInstrumental

Equations

Typology.Case.instInhabitedComitativeInstrumental.default = Typology.Case.ComitativeInstrumental.identity

Instances For

@[implicit_reducible]

instance Typology.Case.instInhabitedComitativeInstrumental :

Inhabited ComitativeInstrumental

Equations

Typology.Case.instInhabitedComitativeInstrumental = { default := Typology.Case.instInhabitedComitativeInstrumental.default }

def Typology.Case.ComitativeInstrumental.isSyncretic :

ComitativeInstrumental → Bool

Whether the language uses the same morpheme for both functions.

Equations

Typology.Case.ComitativeInstrumental.identity.isSyncretic = true
x✝.isSyncretic = false

Instances For

theorem Typology.Case.ch49_ch50_same_sample :

Typology.Case.ch49✝.length = Typology.Case.ch50✝.length

Ch 49 and Ch 50 share the same 261-language sample.

theorem Typology.Case.ch49_no_case_modal :

have noCases := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F49A.CaseCount) => x.value == Data.WALS.F49A.CaseCount.noMorphologicalCaseMarking) Typology.Case.ch49✝).length; noCases > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F49A.CaseCount) => x.value == Data.WALS.F49A.CaseCount.cases2) Typology.Case.ch49✝).length ∧ noCases > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F49A.CaseCount) => x.value == Data.WALS.F49A.CaseCount.cases6_7) Typology.Case.ch49✝).length

Ch 49: Languages with no morphological case-marking are the modal category.

theorem Typology.Case.ch49_case_languages_majority :

have noCases := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F49A.CaseCount) => x.value == Data.WALS.F49A.CaseCount.noMorphologicalCaseMarking) Typology.Case.ch49✝).length; Typology.Case.ch49✝.length - noCases > noCases

Ch 49: Case-bearing languages (any non-zero category) outnumber caseless ones.

theorem Typology.Case.ch50_asymmetry_common :

have symmetrical := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F50A.AsymmetricalCaseMarking) => x.value == Data.WALS.F50A.AsymmetricalCaseMarking.symmetrical) Typology.Case.ch50✝).length; have additive := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F50A.AsymmetricalCaseMarking) => x.value == Data.WALS.F50A.AsymmetricalCaseMarking.additiveQuantitativelyAsymmetrical) Typology.Case.ch50✝).length; have subtractive := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F50A.AsymmetricalCaseMarking) => x.value == Data.WALS.F50A.AsymmetricalCaseMarking.subtractiveQuantitativelyAsymmetrical) Typology.Case.ch50✝).length; have qualitative := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F50A.AsymmetricalCaseMarking) => x.value == Data.WALS.F50A.AsymmetricalCaseMarking.qualitativelyAsymmetrical) Typology.Case.ch50✝).length; have syncretism := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F50A.AsymmetricalCaseMarking) => x.value == Data.WALS.F50A.AsymmetricalCaseMarking.syncretismInRelevantNpTypes) Typology.Case.ch50✝).length; additive + subtractive + qualitative + syncretism > symmetrical

Ch 50: Languages with some asymmetrical case-marking outnumber those with purely symmetrical case.

theorem Typology.Case.ch51_suffix_dominant :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F51A.CaseAffixPosition) => x.value == Data.WALS.F51A.CaseAffixPosition.caseSuffixes) Typology.Case.ch51✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F51A.CaseAffixPosition) => x.value == Data.WALS.F51A.CaseAffixPosition.casePrefixes) Typology.Case.ch51✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F51A.CaseAffixPosition) => x.value == Data.WALS.F51A.CaseAffixPosition.caseSuffixes) Typology.Case.ch51✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F51A.CaseAffixPosition) => x.value == Data.WALS.F51A.CaseAffixPosition.postpositionalClitics) Typology.Case.ch51✝).length

Ch 51: Suffixal case is the dominant strategy among case-marking languages.

theorem Typology.Case.ch52_differentiation_majority :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F52A.ComitativesAndInstrumentals) => x.value == Data.WALS.F52A.ComitativesAndInstrumentals.differentiation) Typology.Case.ch52✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F52A.ComitativesAndInstrumentals) => x.value == Data.WALS.F52A.ComitativesAndInstrumentals.identity) Typology.Case.ch52✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F52A.ComitativesAndInstrumentals) => x.value == Data.WALS.F52A.ComitativesAndInstrumentals.differentiation) Typology.Case.ch52✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F52A.ComitativesAndInstrumentals) => x.value == Data.WALS.F52A.ComitativesAndInstrumentals.mixed) Typology.Case.ch52✝).length

Ch 52: Differentiation is the majority pattern.