Typology.Copulas

@cite{stassen-2013} @cite{hengeveld-1992} @cite{pustet-2003} @cite{haspelmath-2001}

Per-language typological substrate for copula and predication strategies, covering WALS chapters 117--120 (all four authored by Leon Stassen):

• Ch 117 (Stassen): Predicative possession ("I have a book"). N = 240.
• Ch 118 (Stassen): Predicative adjectives ("The book is red"). N = 386.
• Ch 119 (Stassen): Nominal and locational predication ("She is a doctor" vs "The cat is on the mat"). N = 386.
• Ch 120 (Stassen): Zero copula for predicate nominals. N = 386.

Mirrors the Linglib/Typology/{Possession,Negation,Comparison,Coordination, Modality,Gender,Alignment,ArgumentStructure} substrate-extension pattern. Fragment-importable.

What lives here

• PredAdjStrategy (Ch 118: verbal/mixed/nonVerbal).
• PredNounStrategy (binary verbal/nonVerbal — finer than any single WALS chapter; maps to neither F117A nor F118A).
• NomLocStrategy (Ch 119: identical/different).
• ZeroCopulaStatus (Ch 120 + finer: impossible/restricted/widespread, whereas WALS F120A only distinguishes impossible vs. possible).
• CopulaType (supplementary: verbal/pronominal/particle/zero, after @cite{pustet-2003} and @cite{hengeveld-1992}).
• CopulaProfile per-language struct.
• WALS converters fromWALS{118A, 119A, 120A} + the wals120A_allowsZero weakening predicate (since F120A collapses restricted/widespread).
• WALS aggregate sample-size + corpus-only theorems.

Theory-laden caveats

• predNoun is not anchored on a single WALS chapter. It cuts across Ch 119 + Ch 120: a language with verbal nominal predication needs a verbal copula form (visible across both chapters), but there is no WALS chapter asking the binary question directly.
• ZeroCopulaStatus is finer than WALS F120A. F120A has only impossible/possible; the substrate distinguishes restricted (e.g. Russian present-tense only) from widespread (e.g. Tagalog default). fromWALS120A returns Option ZeroCopulaStatus for the F120A.possible case (truly ambiguous). wals120A_allowsZero is the decidable weakening.

Out of scope

The 20-language CopulaProfile sample, cross-chapter correlations (Stassen's implication, areal patterns, copula-type distributions), and Fragment-bridge theorems live in Phenomena/Copulas/Studies/Stassen2013.lean. Partee's compositional BE type-shift bridge to copula typology is in Phenomena/Copulas/Studies/Partee1987.lean.

inductive Typology.Copulas.PredAdjStrategy : Type

WALS Ch 118: How a language expresses adjectival predication ("The book is red").

The three-way distinction reflects the categorial status of adjectives in the language. In "verbal" languages, adjectives inflect like verbs and need no copula. In "non-verbal" languages, adjectives are a distinct category requiring a copula. "Mixed" languages have adjectives that split between verbal and non-verbal behavior.

• verbal : PredAdjStrategy

  Adjectives behave like verbs: they take verbal morphology (tense, aspect, negation) and occur as predicates without a copula. Example: Mandarin shu hong 'book red' = 'The book is red', where hong can take aspect markers directly.

• mixed : PredAdjStrategy

  Some adjectives are verbal (typically core/frequent ones), others require a copula (typically peripheral/borrowed ones). Example: Japanese has verbal adjectives (i-adjectives: takai 'is expensive') and non-verbal adjectives (na-adjectives: shizuka-da 'quiet-COP').

• nonVerbal : PredAdjStrategy

  Adjectives are categorially distinct from verbs and require a copula or other linking element for predication. Example: English The book is red requires the copula is.

@[implicit_reducible]

instance Typology.Copulas.instDecidableEqPredAdjStrategy : DecidableEq PredAdjStrategy

Equations

• Typology.Copulas.instDecidableEqPredAdjStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Copulas.instReprPredAdjStrategy.repr : PredAdjStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Copulas.instReprPredAdjStrategy : Repr PredAdjStrategy

Equations

• Typology.Copulas.instReprPredAdjStrategy = { reprPrec := Typology.Copulas.instReprPredAdjStrategy.repr }

@[implicit_reducible]

instance Typology.Copulas.instInhabitedPredAdjStrategy : Inhabited PredAdjStrategy

Equations

• Typology.Copulas.instInhabitedPredAdjStrategy = { default := Typology.Copulas.PredAdjStrategy.nonVerbal }

inductive Typology.Copulas.PredNounStrategy : Type

How a language expresses nominal predication ("She is a doctor").

The binary distinction captures whether the language uses a verbal copula (a word that inflects like a verb and carries tense/agreement) or a non-verbal strategy (juxtaposition, pronominal copula, or invariant particle). Not anchored on a single WALS chapter; visible across F119A + F120A.

• verbal : PredNounStrategy

  Nominal predication uses a verbal copula that inflects for tense, agreement, etc. Example: English She is a doctor, where is is a fully inflecting verb (am/is/are/was/were).

• nonVerbal : PredNounStrategy

  Nominal predication uses juxtaposition or a non-verbal element (particle, pronoun, etc.), not a copula verb. Example: Russian present tense Ona vrach 'She doctor' = 'She is a doctor' (no copula in present tense).

@[implicit_reducible]

instance Typology.Copulas.instDecidableEqPredNounStrategy : DecidableEq PredNounStrategy

Equations

• Typology.Copulas.instDecidableEqPredNounStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Copulas.instReprPredNounStrategy : Repr PredNounStrategy

Equations

• Typology.Copulas.instReprPredNounStrategy = { reprPrec := Typology.Copulas.instReprPredNounStrategy.repr }

def Typology.Copulas.instReprPredNounStrategy.repr : PredNounStrategy → Nat → Std.Format

Equations

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

inductive Typology.Copulas.NomLocStrategy : Type

WALS Ch 119: Whether a language uses the same or different strategy for nominal predication ("She is a doctor") and locational predication ("The cat is on the mat").

Many languages use different verbs: e.g., Spanish ser (nominal) vs estar (locational), or have a copula for one but not the other. The "different" value is the majority pattern cross-linguistically.

• identical : NomLocStrategy

  The same copula or strategy is used for both nominal and locational predication. Example: English She is a doctor / The cat is on the mat -- both use be.

• different : NomLocStrategy

  Different copulas or strategies are used for nominal vs locational predication. Example: Spanish ser (nominal: Es doctora) vs estar (locational: Esta en la casa).

@[implicit_reducible]

instance Typology.Copulas.instDecidableEqNomLocStrategy : DecidableEq NomLocStrategy

Equations

• Typology.Copulas.instDecidableEqNomLocStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Copulas.instReprNomLocStrategy.repr : NomLocStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Copulas.instReprNomLocStrategy : Repr NomLocStrategy

Equations

• Typology.Copulas.instReprNomLocStrategy = { reprPrec := Typology.Copulas.instReprNomLocStrategy.repr }

inductive Typology.Copulas.ZeroCopulaStatus : Type

Zero copula status, extending WALS F120A's binary impossible/possible with the standard restricted/widespread distinction.

Zero copula is typically conditioned by tense (present only) or person (3rd person only). "Widespread" means zero copula is the default, unrestricted strategy.

• impossible : ZeroCopulaStatus

  Zero copula is impossible: the copula is always required in nominal predication, regardless of tense, person, or other factors. Example: English *She doctor is ungrammatical.

• restricted : ZeroCopulaStatus

  Zero copula is possible in restricted contexts: typically present tense, or 3rd person, or in certain clause types. The copula appears in other environments. Example: Russian allows zero copula in present tense (Ona vrach 'She doctor') but requires it in past tense (Ona byla vrach 'She was doctor').

• widespread : ZeroCopulaStatus

  Zero copula is the normal, widespread, or default strategy. The copula is absent in most environments. Example: Tagalog Doktor siya 'Doctor she' = 'She is a doctor'.

@[implicit_reducible]

instance Typology.Copulas.instDecidableEqZeroCopulaStatus : DecidableEq ZeroCopulaStatus

Equations

• Typology.Copulas.instDecidableEqZeroCopulaStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Copulas.instReprZeroCopulaStatus.repr : ZeroCopulaStatus → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Copulas.instReprZeroCopulaStatus : Repr ZeroCopulaStatus

Equations

• Typology.Copulas.instReprZeroCopulaStatus = { reprPrec := Typology.Copulas.instReprZeroCopulaStatus.repr }

inductive Typology.Copulas.CopulaType : Type

Morphosyntactic type of copula, when present.

Supplements the WALS classification with a finer-grained typology of copular elements, following @cite{pustet-2003} and @cite{hengeveld-1992}.

• verbalCopula : CopulaType

  Fully inflecting verbal copula: takes tense, agreement, negation like other verbs. Example: English be (am/is/are/was/were).

• pronominalCopula : CopulaType

  Pronominal copula: a pronoun-like element that agrees with the subject. Example: Hebrew hu/hi/hem/hen (he/she/they.m/they.f) used as a copula in present tense.

• particle : CopulaType

  Invariant particle: a non-inflecting element linking subject and predicate. Example: Swahili ni (affirmative copula, invariant).

• zero : CopulaType

  No copula: predication by juxtaposition.

@[implicit_reducible]

instance Typology.Copulas.instDecidableEqCopulaType : DecidableEq CopulaType

Equations

• Typology.Copulas.instDecidableEqCopulaType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Copulas.instReprCopulaType : Repr CopulaType

Equations

• Typology.Copulas.instReprCopulaType = { reprPrec := Typology.Copulas.instReprCopulaType.repr }

def Typology.Copulas.instReprCopulaType.repr : CopulaType → Nat → Std.Format

Equations

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

structure Typology.Copulas.CopulaProfile : Type

A language's copula and predication profile across WALS Chs 118--120

• supplementary copula-type information.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• family : String

  Language family.

• predAdj : PredAdjStrategy

  Ch 118: How adjectival predication is expressed.

• predNoun : PredNounStrategy

  How nominal predication is expressed (cross-cuts Ch 119/120).

• nomLoc : NomLocStrategy

  Ch 119: Whether nominal and locational predication use the same or different strategy.

• zeroCopula : ZeroCopulaStatus

  Ch 120: Whether zero copula is possible in nominal predication (extended with restricted/widespread).

• copulaType : CopulaType

  Primary copula type in the language (supplementary).

• copulaForms : List String

  Illustrative copula form(s).

• notes : String

  Notes on the predication system.

def Typology.Copulas.instReprCopulaProfile.repr : CopulaProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Copulas.instReprCopulaProfile : Repr CopulaProfile

Equations

• Typology.Copulas.instReprCopulaProfile = { reprPrec := Typology.Copulas.instReprCopulaProfile.repr }

def Typology.Copulas.CopulaProfile.hasVerbalAdj (p : CopulaProfile) : Bool

Does a language have verbal adjectives?

Equations

• p.hasVerbalAdj = (p.predAdj == Typology.Copulas.PredAdjStrategy.verbal)

def Typology.Copulas.CopulaProfile.hasVerbalNounCopula (p : CopulaProfile) : Bool

Does a language have a verbal copula for nominal predication?

Equations

• p.hasVerbalNounCopula = (p.predNoun == Typology.Copulas.PredNounStrategy.verbal)

def Typology.Copulas.CopulaProfile.allowsZeroCopula (p : CopulaProfile) : Bool

Does a language allow zero copula (restricted or widespread)?

Equations

• p.allowsZeroCopula = (p.zeroCopula == Typology.Copulas.ZeroCopulaStatus.restricted || p.zeroCopula == Typology.Copulas.ZeroCopulaStatus.widespread)

def Typology.Copulas.CopulaProfile.hasNomLocSplit (p : CopulaProfile) : Bool

Does a language split nominal and locational predication?

Equations

• p.hasNomLocSplit = (p.nomLoc == Typology.Copulas.NomLocStrategy.different)

def Typology.Copulas.CopulaProfile.alwaysRequiresCopula (p : CopulaProfile) : Bool

Does a language require a copula in all contexts?

Equations

• p.alwaysRequiresCopula = (p.zeroCopula == Typology.Copulas.ZeroCopulaStatus.impossible)

def Typology.Copulas.fromWALS118A : Data.WALS.F118A.PredicativeAdjectiveType → PredAdjStrategy

Map WALS F118A (predicative adjectives) to PredAdjStrategy.

Equations

• Typology.Copulas.fromWALS118A Data.WALS.F118A.PredicativeAdjectiveType.verbalEncoding = Typology.Copulas.PredAdjStrategy.verbal
• Typology.Copulas.fromWALS118A Data.WALS.F118A.PredicativeAdjectiveType.nonverbalEncoding = Typology.Copulas.PredAdjStrategy.nonVerbal
• Typology.Copulas.fromWALS118A Data.WALS.F118A.PredicativeAdjectiveType.mixed = Typology.Copulas.PredAdjStrategy.mixed

def Typology.Copulas.fromWALS119A : Data.WALS.F119A.NominalLocationalPredication → NomLocStrategy

Map WALS F119A (nominal and locational predication) to NomLocStrategy.

Equations

• Typology.Copulas.fromWALS119A Data.WALS.F119A.NominalLocationalPredication.different = Typology.Copulas.NomLocStrategy.different
• Typology.Copulas.fromWALS119A Data.WALS.F119A.NominalLocationalPredication.identical = Typology.Copulas.NomLocStrategy.identical

def Typology.Copulas.fromWALS120A : Data.WALS.F120A.ZeroCopulaType → Option ZeroCopulaStatus

Map WALS F120A (zero copula) to ZeroCopulaStatus.

F120A has only two values (impossible/possible), while ZeroCopulaStatus distinguishes restricted from widespread within "possible." The mapping is therefore lossy: .impossible maps exactly, but .possible is ambiguous between .restricted and .widespread. Returns Option for the ambiguous case.

Equations

• Typology.Copulas.fromWALS120A Data.WALS.F120A.ZeroCopulaType.impossible = some Typology.Copulas.ZeroCopulaStatus.impossible
• Typology.Copulas.fromWALS120A Data.WALS.F120A.ZeroCopulaType.possible = none

def Typology.Copulas.wals120A_allowsZero : Data.WALS.F120A.ZeroCopulaType → Bool

Decidable weakening of fromWALS120A: does WALS F120A say zero copula is at least possible? Suitable for cross-checking against CopulaProfile.allowsZeroCopula.

Equations

• Typology.Copulas.wals120A_allowsZero Data.WALS.F120A.ZeroCopulaType.impossible = false
• Typology.Copulas.wals120A_allowsZero Data.WALS.F120A.ZeroCopulaType.possible = true

theorem Typology.Copulas.ch118_119_120_same_sample : Typology.Copulas.ch118✝.length = Typology.Copulas.ch119✝.length ∧ Typology.Copulas.ch119✝.length = Typology.Copulas.ch120✝.length

Chs 118, 119, 120 use the same 386-language sample. Ch 117 uses a smaller 240-language sample.

theorem Typology.Copulas.ch118_verbal_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Typology.Copulas.ch118✝).length = 151

Ch 118 cell counts (from @cite{stassen-2013}'s map).

theorem Typology.Copulas.ch118_nonverbal_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.nonverbalEncoding) Typology.Copulas.ch118✝).length = 132

theorem Typology.Copulas.ch118_mixed_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.mixed) Typology.Copulas.ch118✝).length = 103

theorem Typology.Copulas.ch119_different_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F119A.NominalLocationalPredication) => x.value == Data.WALS.F119A.NominalLocationalPredication.different) Typology.Copulas.ch119✝).length = 269

Ch 119 cell counts.

theorem Typology.Copulas.ch119_identical_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F119A.NominalLocationalPredication) => x.value == Data.WALS.F119A.NominalLocationalPredication.identical) Typology.Copulas.ch119✝).length = 117

theorem Typology.Copulas.ch120_impossible_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F120A.ZeroCopulaType) => x.value == Data.WALS.F120A.ZeroCopulaType.impossible) Typology.Copulas.ch120✝).length = 211

Ch 120 cell counts.

theorem Typology.Copulas.ch120_possible_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F120A.ZeroCopulaType) => x.value == Data.WALS.F120A.ZeroCopulaType.possible) Typology.Copulas.ch120✝).length = 175

theorem Typology.Copulas.ch117_locational_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F117A.PredicativePossession) => x.value == Data.WALS.F117A.PredicativePossession.locational) Typology.Copulas.ch117✝).length = 48

Ch 117 cell counts.

theorem Typology.Copulas.ch117_genitive_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F117A.PredicativePossession) => x.value == Data.WALS.F117A.PredicativePossession.genitive) Typology.Copulas.ch117✝).length = 22

theorem Typology.Copulas.ch117_topic_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F117A.PredicativePossession) => x.value == Data.WALS.F117A.PredicativePossession.topic) Typology.Copulas.ch117✝).length = 48

theorem Typology.Copulas.ch117_conjunctional_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F117A.PredicativePossession) => x.value == Data.WALS.F117A.PredicativePossession.conjunctional) Typology.Copulas.ch117✝).length = 59

theorem Typology.Copulas.ch117_have_count : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F117A.PredicativePossession) => x.value == Data.WALS.F117A.PredicativePossession.have) Typology.Copulas.ch117✝).length = 63

theorem Typology.Copulas.verbal_adj_most_common : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Typology.Copulas.ch118✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.nonverbalEncoding) Typology.Copulas.ch118✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Typology.Copulas.ch118✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.mixed) Typology.Copulas.ch118✝).length

Ch 118: verbal encoding is the most common strategy for predicative adjectives, exceeding both mixed and nonverbal encoding.

theorem Typology.Copulas.verbal_adj_plurality : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Typology.Copulas.ch118✝).length * 3 > Typology.Copulas.ch118✝.length

Ch 118: verbal adjectives account for roughly 39% of the sample.

theorem Typology.Copulas.no_adj_strategy_majority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F118A.PredicativeAdjectiveType) => x.value == Data.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Typology.Copulas.ch118✝).length * 2 < Typology.Copulas.ch118✝.length

Ch 118: no single predicative adjective strategy is a strict majority.

theorem Typology.Copulas.nomloc_split_majority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F119A.NominalLocationalPredication) => x.value == Data.WALS.F119A.NominalLocationalPredication.different) Typology.Copulas.ch119✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F119A.NominalLocationalPredication) => x.value == Data.WALS.F119A.NominalLocationalPredication.identical) Typology.Copulas.ch119✝).length

Ch 119: using different strategies for nominal and locational predication is more common than using the same strategy. Languages typically distinguish "is a doctor" from "is in the room" with different grammatical means.

theorem Typology.Copulas.nomloc_split_supermajority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F119A.NominalLocationalPredication) => x.value == Data.WALS.F119A.NominalLocationalPredication.different) Typology.Copulas.ch119✝).length > Typology.Copulas.ch119✝.length / 2

Ch 119: the split pattern is a clear supermajority (more than half).

theorem Typology.Copulas.zero_impossible_majority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F120A.ZeroCopulaType) => x.value == Data.WALS.F120A.ZeroCopulaType.impossible) Typology.Copulas.ch120✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F120A.ZeroCopulaType) => x.value == Data.WALS.F120A.ZeroCopulaType.possible) Typology.Copulas.ch120✝).length

Ch 120: "Impossible" (copula always required) is the majority value.

theorem Typology.Copulas.zero_impossible_over_half : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F120A.ZeroCopulaType) => x.value == Data.WALS.F120A.ZeroCopulaType.impossible) Typology.Copulas.ch120✝).length > Typology.Copulas.ch120✝.length / 2

Ch 120: "Impossible" accounts for more than half the sample.