Comparison: comparative-construction typology

[Sta13b] [DH13b] [BKF+09] [Has01]

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 ([BKF+09] 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 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 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 Comparative.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 Comparative.instDecidableEqComparativeType : DecidableEq ComparativeType

Equations

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

def Comparative.instBEqComparativeType.beq : ComparativeType → ComparativeType → Bool

Equations

• Comparative.instBEqComparativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Comparative.instBEqComparativeType : BEq ComparativeType

Equations

• Comparative.instBEqComparativeType = { beq := Comparative.instBEqComparativeType.beq }

def Comparative.instReprComparativeType.repr : ComparativeType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Comparative.instReprComparativeType : Repr ComparativeType

Equations

• Comparative.instReprComparativeType = { reprPrec := Comparative.instReprComparativeType.repr }

inductive Comparative.DegreeWordType : Type

[BKF+09]: 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 Comparative.instDecidableEqDegreeWordType : DecidableEq DegreeWordType

Equations

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

def Comparative.instBEqDegreeWordType.beq : DegreeWordType → DegreeWordType → Bool

Equations

• Comparative.instBEqDegreeWordType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Comparative.instBEqDegreeWordType : BEq DegreeWordType

Equations

• Comparative.instBEqDegreeWordType = { beq := Comparative.instBEqDegreeWordType.beq }

@[implicit_reducible]

instance Comparative.instReprDegreeWordType : Repr DegreeWordType

Equations

• Comparative.instReprDegreeWordType = { reprPrec := Comparative.instReprDegreeWordType.repr }

def Comparative.instReprDegreeWordType.repr : DegreeWordType → ℕ → Std.Format

Equations

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

inductive Comparative.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 Comparative.instDecidableEqSuperlativeStrategy : DecidableEq SuperlativeStrategy

Equations

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

@[implicit_reducible]

instance Comparative.instBEqSuperlativeStrategy : BEq SuperlativeStrategy

Equations

• Comparative.instBEqSuperlativeStrategy = { beq := Comparative.instBEqSuperlativeStrategy.beq }

def Comparative.instBEqSuperlativeStrategy.beq : SuperlativeStrategy → SuperlativeStrategy → Bool

Equations

• Comparative.instBEqSuperlativeStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Comparative.instReprSuperlativeStrategy.repr : SuperlativeStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Comparative.instReprSuperlativeStrategy : Repr SuperlativeStrategy

Equations

• Comparative.instReprSuperlativeStrategy = { reprPrec := Comparative.instReprSuperlativeStrategy.repr }

structure Comparative.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 Comparative.instReprComparativeProfile.repr : ComparativeProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Comparative.instReprComparativeProfile : Repr ComparativeProfile

Equations

• Comparative.instReprComparativeProfile = { reprPrec := Comparative.instReprComparativeProfile.repr }

def Comparative.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

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

def Comparative.ComparativeProfile.hasType (p : ComparativeProfile) (t : ComparativeType) : Bool

Does a language have a given comparative type?

Equations

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

def Comparative.ComparativeProfile.hasDegWord (p : ComparativeProfile) : Bool

Does a language have a free degree word?

Equations

• p.hasDegWord = (p.degreeWord == Comparative.DegreeWordType.hasDegreeWord)

def Comparative.ComparativeProfile.hasMorphComp (p : ComparativeProfile) : Bool

Does a language have bound comparative morphology?

Equations

• p.hasMorphComp = (p.degreeWord == Comparative.DegreeWordType.morphological)

def Comparative.ComparativeProfile.noDegree (p : ComparativeProfile) : Bool

Does a language lack overt degree marking entirely?

Equations

• p.noDegree = (p.degreeWord == Comparative.DegreeWordType.noDegreeMarking)

def Comparative.ComparativeProfile.hasMorphSuperlative (p : ComparativeProfile) : Bool

Does a language have a morphological superlative?

Equations

• p.hasMorphSuperlative = (p.superlative == Comparative.SuperlativeStrategy.morphological)

def Comparative.ComparativeProfile.isSOV (p : ComparativeProfile) : Bool

Is this an SOV language?

Equations

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

def Comparative.ComparativeProfile.isSVO (p : ComparativeProfile) : Bool

Is this an SVO language?

Equations

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

def Comparative.countByType (langs : List ComparativeProfile) (t : ComparativeType) : ℕ

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

Equations

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

def Comparative.countByDegree (langs : List ComparativeProfile) (d : DegreeWordType) : ℕ

Count of languages in a sample by degree word type.

Equations

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

def Comparative.countBySuperlative (langs : List ComparativeProfile) (s : SuperlativeStrategy) : ℕ

Count of languages in a sample by superlative strategy.

Equations

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

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

Per-type counts sum to sample total.

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

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

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

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

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

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

Stassen 1985 — Comparative Entry [Sta85]

A typed record for the parameters of a comparative construction in a particular language: standard case, how that case is assigned, optional fixed-encoding role, the standard marker (e.g., than, より), and whether the construction has dedicated degree morphology.

structure Comparative.ComparativeEntry : Type

A language's comparative construction entry ([Sta85]).

• standardCase : Case
• caseAssignment : Features.CaseAssignment
• fixedEncoding : Option Features.FixedCaseEncoding
• standardMarker : String
• hasDegreeMorphology : Bool

@[implicit_reducible]

instance Comparative.instReprComparativeEntry : Repr ComparativeEntry

Equations

• Comparative.instReprComparativeEntry = { reprPrec := Comparative.instReprComparativeEntry.repr }

def Comparative.instReprComparativeEntry.repr : ComparativeEntry → ℕ → Std.Format

Equations

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

def Comparative.instBEqComparativeEntry.beq : ComparativeEntry → ComparativeEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Comparative.instBEqComparativeEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Comparative.instBEqComparativeEntry : BEq ComparativeEntry

Equations

• Comparative.instBEqComparativeEntry = { beq := Comparative.instBEqComparativeEntry.beq }