Typology.Comparison

@cite{stassen-2013} @cite{wals-2013} @cite{beck-2009} @cite{haspelmath-2001}

Per-language typological substrate for comparative-construction typology (Stassen's WALS Ch 121 framework + Beck-Crisma-Krasikova degree-word typology + superlative strategies). Fragment-importable; mirrors the Linglib/Typology/{Possession,Negation,Question}.lean pattern.

What lives here

• ComparativeType (5-way Stassen 2013 / WALS Ch 121A: locational | exceed | conjoined | particle | mixed).
• DegreeWordType (@cite{beck-2009} 3-way: hasDegreeWord | morphological | noDegreeMarking).
• SuperlativeStrategy (6-way: morphological, definiteComparative, elative, exceedAll, comparativeUniversal, none).
• ComparativeProfile — Fragment-side joint with comparative type, degree word type, superlative strategy, and optional standardMarker / degreeMarker / basicOrder / illustrative form.
• ofWALS121A converter from WALS Ch 121A.
• WALS Ch 121A aggregate sample-size + corpus-only generalisations (locational_most_common, particle_rarest, locational_and_particle_dominant).
• Helper predicates (hasType, hasDegWord, noDegree, isSOV, isSVO).

Theory-laden caveats

• ComparativeType is the WALS 2013 5-way typology. Stassen's original 1985 6-way typology (separative | allative | locative | exceed | conjoined | particle) lives in Phenomena/Comparison/Studies/Stassen1985.lean because the 3-way adverbial split is paper-distinctive — the WALS update collapses it into a single locational for cross-linguistic indexing.
• DegreeWordType is Beck et al. 2009's three-way classification. Other approaches (Kennedy 1999, Beck 2011, Bochnak 2013) refine the typology with scale-structure and degree-argument parameters; those live in Theories/Semantics/Degree/.

Out of scope

Stassen's 1985 fine-grained adverbial typology (ComparativeType1985, caseAssignment, fixedEncoding, spatialCase) and the 1985-↔-2013 consistency theorems live in Studies/Stassen1985.lean (paper-anchored). Cross-linguistic theorems consuming Fragment per-language data live in Studies/Stassen2013.lean.

inductive Typology.Comparison.ComparativeType : Type

WALS Ch 121: how a language expresses comparison of inequality.

Stassen's classification is based on how the standard of comparison (the Y in "X is more Adj than Y") is encoded. Five types are cross-cutting; a single language may use more than one productively (classified as "mixed").

• locational : ComparativeType

  Locational: the standard is marked with a locational/ablative case or adposition. Example: Japanese Y yori X tall 'Y from/than X tall'. Also Turkish (ablative), Hindi-Urdu (se), Latin (ablative).

• exceed : ComparativeType

  Exceed: a verb meaning 'exceed/surpass' encodes comparison. Example: Yoruba Ade ga ju Bola lo. Common in Niger-Congo + SE Asian.

• conjoined : ComparativeType

  Conjoined: two juxtaposed clauses, one attributing the property to X and the other denying / contrasting it for Y. Rarest type.

• particle : ComparativeType

  Particle: a dedicated comparative particle marks the standard (e.g. English than, German als). Standard Average European pattern.

• mixed : ComparativeType

  Mixed: more than one type is productive without a clear dominant.

@[implicit_reducible]

instance Typology.Comparison.instDecidableEqComparativeType : DecidableEq ComparativeType

Equations

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

@[implicit_reducible]

instance Typology.Comparison.instBEqComparativeType : BEq ComparativeType

Equations

• Typology.Comparison.instBEqComparativeType = { beq := Typology.Comparison.instBEqComparativeType.beq }

def Typology.Comparison.instBEqComparativeType.beq : ComparativeType → ComparativeType → Bool

Equations

• Typology.Comparison.instBEqComparativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Typology.Comparison.instReprComparativeType.repr : ComparativeType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Comparison.instReprComparativeType : Repr ComparativeType

Equations

• Typology.Comparison.instReprComparativeType = { reprPrec := Typology.Comparison.instReprComparativeType.repr }

inductive Typology.Comparison.DegreeWordType : Type

@cite{beck-2009}: presence of degree words in comparison constructions.

• hasDegreeWord : DegreeWordType

  Free degree word (English more, French plus, Mandarin geng).

• morphological : DegreeWordType

  Bound comparative morphology, no free degree word (English -er for short adjectives, Turkish -rak).

• noDegreeMarking : DegreeWordType

  No overt degree marking (exceed-verb, juxtaposition, pragmatic).

@[implicit_reducible]

instance Typology.Comparison.instDecidableEqDegreeWordType : DecidableEq DegreeWordType

Equations

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

@[implicit_reducible]

instance Typology.Comparison.instBEqDegreeWordType : BEq DegreeWordType

Equations

• Typology.Comparison.instBEqDegreeWordType = { beq := Typology.Comparison.instBEqDegreeWordType.beq }

def Typology.Comparison.instBEqDegreeWordType.beq : DegreeWordType → DegreeWordType → Bool

Equations

• Typology.Comparison.instBEqDegreeWordType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Comparison.instReprDegreeWordType : Repr DegreeWordType

Equations

• Typology.Comparison.instReprDegreeWordType = { reprPrec := Typology.Comparison.instReprDegreeWordType.repr }

def Typology.Comparison.instReprDegreeWordType.repr : DegreeWordType → Nat → Std.Format

Equations

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

inductive Typology.Comparison.SuperlativeStrategy : Type

How a language forms superlatives. Partially independent of comparative type; some languages lack a dedicated superlative entirely.

• morphological : SuperlativeStrategy

  Dedicated superlative morphology (English -est, Latin -issimus).

• definiteComparative : SuperlativeStrategy

  Definite article + comparative (French le plus grand).

• elative : SuperlativeStrategy

  Elative pattern without comparison class (Arabic ʔafʕal).

• exceedAll : SuperlativeStrategy

  Exceed verb + universal quantifier ("X exceeds all").

• comparativeUniversal : SuperlativeStrategy

  Comparative + universal standard (Japanese dare yori mo takai).

• none : SuperlativeStrategy

  No dedicated superlative strategy.

@[implicit_reducible]

instance Typology.Comparison.instDecidableEqSuperlativeStrategy : DecidableEq SuperlativeStrategy

Equations

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

@[implicit_reducible]

instance Typology.Comparison.instBEqSuperlativeStrategy : BEq SuperlativeStrategy

Equations

• Typology.Comparison.instBEqSuperlativeStrategy = { beq := Typology.Comparison.instBEqSuperlativeStrategy.beq }

def Typology.Comparison.instBEqSuperlativeStrategy.beq : SuperlativeStrategy → SuperlativeStrategy → Bool

Equations

• Typology.Comparison.instBEqSuperlativeStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Typology.Comparison.instReprSuperlativeStrategy.repr : SuperlativeStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Comparison.instReprSuperlativeStrategy : Repr SuperlativeStrategy

Equations

• Typology.Comparison.instReprSuperlativeStrategy = { reprPrec := Typology.Comparison.instReprSuperlativeStrategy.repr }

structure Typology.Comparison.ComparativeProfile : Type

A language's comparative construction profile. Fragment-side joint: every Fragments/{Lang}/Comparison.lean exposes def comparison : ComparativeProfile.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• comparativeType : ComparativeType

  WALS Ch 121 comparative type.

• degreeWord : DegreeWordType

  Degree word typology.

• superlative : SuperlativeStrategy

  Primary superlative strategy.

• comparativeForm : String

  Illustrative comparative form.

• standardMarker : String

  Standard marker (the "than" equivalent), if applicable.

• degreeMarker : String

  Degree marker ("more" equivalent), if applicable.

• basicOrder : String

  Dominant basic word order (for word-order correlations).

def Typology.Comparison.instReprComparativeProfile.repr : ComparativeProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Comparison.instReprComparativeProfile : Repr ComparativeProfile

Equations

• Typology.Comparison.instReprComparativeProfile = { reprPrec := Typology.Comparison.instReprComparativeProfile.repr }

def Typology.Comparison.ofWALS121A : Data.WALS.F121A.ComparativeType → ComparativeType

WALS Ch 121A → ComparativeType. The generated WALS data uses four categories; mixed is not a separate WALS value (languages are assigned to whichever single type best characterises them).

Equations

• Typology.Comparison.ofWALS121A Data.WALS.F121A.ComparativeType.locational = Typology.Comparison.ComparativeType.locational
• Typology.Comparison.ofWALS121A Data.WALS.F121A.ComparativeType.exceed = Typology.Comparison.ComparativeType.exceed
• Typology.Comparison.ofWALS121A Data.WALS.F121A.ComparativeType.conjoined = Typology.Comparison.ComparativeType.conjoined
• Typology.Comparison.ofWALS121A Data.WALS.F121A.ComparativeType.particle = Typology.Comparison.ComparativeType.particle

def Typology.Comparison.ComparativeProfile.hasType (p : ComparativeProfile) (t : ComparativeType) : Bool

Does a language have a given comparative type?

Equations

• p.hasType t = (p.comparativeType == t)

def Typology.Comparison.ComparativeProfile.hasDegWord (p : ComparativeProfile) : Bool

Does a language have a free degree word?

Equations

• p.hasDegWord = (p.degreeWord == Typology.Comparison.DegreeWordType.hasDegreeWord)

def Typology.Comparison.ComparativeProfile.hasMorphComp (p : ComparativeProfile) : Bool

Does a language have bound comparative morphology?

Equations

• p.hasMorphComp = (p.degreeWord == Typology.Comparison.DegreeWordType.morphological)

def Typology.Comparison.ComparativeProfile.noDegree (p : ComparativeProfile) : Bool

Does a language lack overt degree marking entirely?

Equations

• p.noDegree = (p.degreeWord == Typology.Comparison.DegreeWordType.noDegreeMarking)

def Typology.Comparison.ComparativeProfile.hasMorphSuperlative (p : ComparativeProfile) : Bool

Does a language have a morphological superlative?

Equations

• p.hasMorphSuperlative = (p.superlative == Typology.Comparison.SuperlativeStrategy.morphological)

def Typology.Comparison.ComparativeProfile.isSOV (p : ComparativeProfile) : Bool

Is this an SOV language?

Equations

• p.isSOV = (p.basicOrder == "SOV")

def Typology.Comparison.ComparativeProfile.isSVO (p : ComparativeProfile) : Bool

Is this an SVO language?

Equations

• p.isSVO = (p.basicOrder == "SVO" || p.basicOrder == "SVO/V2")

def Typology.Comparison.countByType (langs : List ComparativeProfile) (t : ComparativeType) : Nat

Count of languages in a sample with a given comparative type.

Equations

• Typology.Comparison.countByType langs t = (List.filter (fun (x : Typology.Comparison.ComparativeProfile) => x.hasType t) langs).length

def Typology.Comparison.countByDegree (langs : List ComparativeProfile) (d : DegreeWordType) : Nat

Count of languages in a sample by degree word type.

Equations

• Typology.Comparison.countByDegree langs d = (List.filter (fun (p : Typology.Comparison.ComparativeProfile) => p.degreeWord == d) langs).length

def Typology.Comparison.countBySuperlative (langs : List ComparativeProfile) (s : SuperlativeStrategy) : Nat

Count of languages in a sample by superlative strategy.

Equations

• Typology.Comparison.countBySuperlative langs s = (List.filter (fun (p : Typology.Comparison.ComparativeProfile) => p.superlative == s) langs).length

theorem Typology.Comparison.ch121_counts_sum : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.locational) Typology.Comparison.ch121✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.exceed) Typology.Comparison.ch121✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.conjoined) Typology.Comparison.ch121✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.particle) Typology.Comparison.ch121✝).length = Typology.Comparison.ch121✝.length

Per-type counts sum to sample total.

theorem Typology.Comparison.locational_most_common : have loc := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.locational) Typology.Comparison.ch121✝).length; have exc := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.exceed) Typology.Comparison.ch121✝).length; have con := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.conjoined) Typology.Comparison.ch121✝).length; have par := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.particle) Typology.Comparison.ch121✝).length; loc > exc ∧ loc > con ∧ loc > par

Locational comparatives are the most common single type in WALS Ch 121.

theorem Typology.Comparison.particle_rarest : have loc := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.locational) Typology.Comparison.ch121✝).length; have exc := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.exceed) Typology.Comparison.ch121✝).length; have con := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.conjoined) Typology.Comparison.ch121✝).length; have par := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.particle) Typology.Comparison.ch121✝).length; par < loc ∧ par < exc ∧ par < con

Particle comparatives are the rarest single type in the WALS data.

theorem Typology.Comparison.locational_and_particle_dominant : have loc := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.locational) Typology.Comparison.ch121✝).length; have par := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F121A.ComparativeType) => x.value == Data.WALS.F121A.ComparativeType.particle) Typology.Comparison.ch121✝).length; loc + par > Typology.Comparison.ch121✝.length / 2

Locational + particle together account for more than half the sample.