Comparative Construction Typology (WALS Chapter 121)

@cite{beck-2009} @cite{haspelmath-2001} @cite{kennedy-2007} @cite{stassen-1985} @cite{stassen-2013}

Cross-linguistic data on how languages express comparison of inequality ("X is taller than Y"), based on @cite{stassen-2013} in WALS Online. Stassen identifies five major construction types attested across a sample of 167 languages, classified by how the standard of comparison (the entity being compared to) is encoded.

The WALS 2013 typology simplifies @cite{stassen-1985}'s original six-type classification. Stassen 1985 (based on 110 languages) distinguishes three subtypes within "locational": separative (standard marked 'from'/ablative), allative (standard marked 'to'/goal), and locative (standard marked 'at'/contact). This finer distinction is crucial to the book's explanatory hypothesis connecting comparative types to temporal chaining constructions (formalized in Studies/Stassen1985.lean). The WALS 2013 typology also adds the "mixed" category not present in the 1985 system.

The typology intersects with two further dimensions:

• Degree word typology: whether a language has an overt degree word like English "more" or achieves comparison morphologically or without any degree marker.
• Superlative strategies: how superlatives are formed (elative, definite article + comparative, special morphology, "exceed all" constructions, etc.).

Key typological generalizations

1. Locational comparatives are the most common type worldwide.
2. Particle comparatives concentrate in Europe (a Standard Average European feature; @cite{haspelmath-2001}).
3. Exceed comparatives concentrate in West Africa and mainland Southeast Asia.
4. Conjoined comparatives are the least common type, concentrated in Papuan and Australian languages.
5. SOV languages strongly favor locational comparatives; SVO languages split between exceed and particle types.

inductive Phenomena.Comparison.Typology.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. The 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, as if saying "X is tall from/at Y". Example: Japanese Taroo wa Hanako yori se ga takai 'Taro TOP Hanako than/from tall'. Also Turkish (ablative), Hindi-Urdu (postposition se), Latin (ablative case).

• exceed : ComparativeType

  Exceed: a verb meaning 'exceed' or 'surpass' is used to encode comparison, as if saying "X exceeds/surpasses Y in tallness". Example: Yoruba Ade ga ju Bola lo 'Ade tall exceed Bola go'. Common in Niger-Congo and mainland Southeast Asian languages.

• conjoined : ComparativeType

  Conjoined: two juxtaposed or coordinated clauses, one attributing the property to X and the other denying it of Y (or attributing its antonym), as if saying "X is tall, Y is short". Example: Amele (Papuan) uqa busak-i, ija cos-ig-a 'he big-PRED, I small-1SG-PRED'. The rarest type.

• particle : ComparativeType

  Particle: a dedicated comparative particle or morpheme marks the standard, as in English "X is taller than Y". The particle is not a case marker or adposition with independent spatial meaning. Concentrated in Standard Average European.

• mixed : ComparativeType

  Mixed: the language uses more than one of the above types productively, without a clear dominant strategy.

instance Phenomena.Comparison.Typology.instDecidableEqComparativeType : DecidableEq ComparativeType

Equations

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

instance Phenomena.Comparison.Typology.instBEqComparativeType : BEq ComparativeType

Equations

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

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

Equations

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

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

Equations

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

instance Phenomena.Comparison.Typology.instReprComparativeType : Repr ComparativeType

Equations

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

inductive Phenomena.Comparison.Typology.ComparativeType1985 : Type

The six comparative construction types of @cite{stassen-1985} Ch 2.

These are finer than the WALS 2013 types (ComparativeType): the three adverbial subtypes (separative, allative, locative) are collapsed into a single "locational" category in WALS. The six types form a hierarchy based on case assignment and syntactic encoding:

                    Comparative
                   /            \
            Derived case    Fixed case
           /        \       /        \
      Conjoined  Particle  Exceed  Adverbial
                                  /    |    \
                               Sep   All   Loc

• separative : ComparativeType1985
• allative : ComparativeType1985
• locative : ComparativeType1985
• exceed : ComparativeType1985
• conjoined : ComparativeType1985
• particle : ComparativeType1985

instance Phenomena.Comparison.Typology.instDecidableEqComparativeType1985 : DecidableEq ComparativeType1985

Equations

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

def Phenomena.Comparison.Typology.instBEqComparativeType1985.beq : ComparativeType1985 → ComparativeType1985 → Bool

Equations

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

instance Phenomena.Comparison.Typology.instBEqComparativeType1985 : BEq ComparativeType1985

Equations

• Phenomena.Comparison.Typology.instBEqComparativeType1985 = { beq := Phenomena.Comparison.Typology.instBEqComparativeType1985.beq }

def Phenomena.Comparison.Typology.instReprComparativeType1985.repr : ComparativeType1985 → Nat → Std.Format

Equations

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

instance Phenomena.Comparison.Typology.instReprComparativeType1985 : Repr ComparativeType1985

Equations

• Phenomena.Comparison.Typology.instReprComparativeType1985 = { reprPrec := Phenomena.Comparison.Typology.instReprComparativeType1985.repr }

def Phenomena.Comparison.Typology.ComparativeType1985.toWALS : ComparativeType1985 → ComparativeType

Map @cite{stassen-1985} types to the coarser WALS 2013 types.

The key coarsening: separative, allative, and locative all become "locational". This loses the spatial-relation distinction that drives Stassen's explanatory universals connecting comparison to temporal chaining.

Equations

• Phenomena.Comparison.Typology.ComparativeType1985.separative.toWALS = Phenomena.Comparison.Typology.ComparativeType.locational
• Phenomena.Comparison.Typology.ComparativeType1985.allative.toWALS = Phenomena.Comparison.Typology.ComparativeType.locational
• Phenomena.Comparison.Typology.ComparativeType1985.locative.toWALS = Phenomena.Comparison.Typology.ComparativeType.locational
• Phenomena.Comparison.Typology.ComparativeType1985.exceed.toWALS = Phenomena.Comparison.Typology.ComparativeType.exceed
• Phenomena.Comparison.Typology.ComparativeType1985.conjoined.toWALS = Phenomena.Comparison.Typology.ComparativeType.conjoined
• Phenomena.Comparison.Typology.ComparativeType1985.particle.toWALS = Phenomena.Comparison.Typology.ComparativeType.particle

def Phenomena.Comparison.Typology.ComparativeType1985.caseAssignment : ComparativeType1985 → Core.CaseAssignment

Case assignment for each 1985 type.

Equations

• Phenomena.Comparison.Typology.ComparativeType1985.conjoined.caseAssignment = Core.CaseAssignment.derived
• Phenomena.Comparison.Typology.ComparativeType1985.particle.caseAssignment = Core.CaseAssignment.derived
• x✝.caseAssignment = Core.CaseAssignment.fixed

def Phenomena.Comparison.Typology.ComparativeType1985.fixedEncoding : ComparativeType1985 → Option Core.FixedCaseEncoding

Fixed-case encoding (only meaningful for fixed-case types).

Equations

• Phenomena.Comparison.Typology.ComparativeType1985.exceed.fixedEncoding = some Core.FixedCaseEncoding.directObject
• Phenomena.Comparison.Typology.ComparativeType1985.separative.fixedEncoding = some Core.FixedCaseEncoding.adverbial
• Phenomena.Comparison.Typology.ComparativeType1985.allative.fixedEncoding = some Core.FixedCaseEncoding.adverbial
• Phenomena.Comparison.Typology.ComparativeType1985.locative.fixedEncoding = some Core.FixedCaseEncoding.adverbial
• Phenomena.Comparison.Typology.ComparativeType1985.conjoined.fixedEncoding = none
• Phenomena.Comparison.Typology.ComparativeType1985.particle.fixedEncoding = none

def Phenomena.Comparison.Typology.ComparativeType1985.spatialCase : ComparativeType1985 → Option Core.Case

Spatial case of the standard marker (only meaningful for adverbial types).

Maps to the Core.Case values that correspond to Stassen's spatial triad: ablative (separative), allative, locative.

Equations

• Phenomena.Comparison.Typology.ComparativeType1985.separative.spatialCase = some Core.Case.abl
• Phenomena.Comparison.Typology.ComparativeType1985.allative.spatialCase = some Core.Case.all
• Phenomena.Comparison.Typology.ComparativeType1985.locative.spatialCase = some Core.Case.loc
• x✝.spatialCase = none

inductive Phenomena.Comparison.Typology.DegreeWordType : Type

Whether a language has an overt degree word in comparatives.

@cite{beck-2009} classify languages into three types based on the presence and nature of degree morphology in comparison constructions:

• Languages with a dedicated degree word (English "more", German "mehr")
• Languages with comparative morphology but no free degree word (English "-er" suffix, but also Turkish, Japanese)
• Languages with no degree marking at all (the comparative meaning is derived from context, word order, or the exceed-verb semantics).

• hasDegreeWord : DegreeWordType

  Has a free degree word (e.g., English "more", French "plus", Mandarin "geng").

• morphological : DegreeWordType

  Has comparative morphology (affixal) but no free degree word (e.g., English "-er" for short adjectives, Turkish "-rak").

• noDegreeMarking : DegreeWordType

  No overt degree marking; comparison expressed via exceed verb, juxtaposition, or pragmatic inference.

instance Phenomena.Comparison.Typology.instDecidableEqDegreeWordType : DecidableEq DegreeWordType

Equations

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

instance Phenomena.Comparison.Typology.instBEqDegreeWordType : BEq DegreeWordType

Equations

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

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

Equations

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

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

Equations

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

instance Phenomena.Comparison.Typology.instReprDegreeWordType : Repr DegreeWordType

Equations

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

inductive Phenomena.Comparison.Typology.SuperlativeStrategy : Type

How a language forms superlatives ("X is the tallest").

Superlative strategies are partially independent of comparative type. Some languages lack a dedicated superlative entirely, using comparatives with a universal standard ("taller than all") or "most" constructions.

• morphological : SuperlativeStrategy

  Superlative morphology: dedicated affix or stem change (e.g., English "-est", Latin "-issimus").

• definiteComparative : SuperlativeStrategy

  Definite article + comparative: "the more Adj" = superlative (e.g., Romance languages: French "le plus grand").

• elative : SuperlativeStrategy

  Elative: special "very/extremely" form without comparison class (e.g., Arabic elative pattern ʔafʕal).

• exceedAll : SuperlativeStrategy

  Exceed-all: exceed verb + universal quantifier (e.g., "X exceeds all in height").

• comparativeUniversal : SuperlativeStrategy

  Comparative + universal standard: "X is taller than all" (e.g., Japanese dare yori mo takai 'than anyone tall').

• none : SuperlativeStrategy

  No dedicated superlative strategy; context or periphrasis used.

instance Phenomena.Comparison.Typology.instDecidableEqSuperlativeStrategy : DecidableEq SuperlativeStrategy

Equations

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

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

Equations

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

instance Phenomena.Comparison.Typology.instBEqSuperlativeStrategy : BEq SuperlativeStrategy

Equations

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

instance Phenomena.Comparison.Typology.instReprSuperlativeStrategy : Repr SuperlativeStrategy

Equations

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

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

Equations

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

theorem Phenomena.Comparison.Typology.ch121_total : Phenomena.Comparison.Typology.ch121✝.length = 167

Ch 121 total: 167 languages in the generated WALS dataset.

theorem Phenomena.Comparison.Typology.ch121_locational_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.locational) Phenomena.Comparison.Typology.ch121✝).length = 78

Ch 121A per-type counts from the generated WALS v2020.4 data.

theorem Phenomena.Comparison.Typology.ch121_exceed_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.exceed) Phenomena.Comparison.Typology.ch121✝).length = 33

theorem Phenomena.Comparison.Typology.ch121_conjoined_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.conjoined) Phenomena.Comparison.Typology.ch121✝).length = 34

theorem Phenomena.Comparison.Typology.ch121_particle_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.particle) Phenomena.Comparison.Typology.ch121✝).length = 22

theorem Phenomena.Comparison.Typology.ch121_counts_sum : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.locational) Phenomena.Comparison.Typology.ch121✝).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.exceed) Phenomena.Comparison.Typology.ch121✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.conjoined) Phenomena.Comparison.Typology.ch121✝²).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => x.value == Core.WALS.F121A.ComparativeType.particle) Phenomena.Comparison.Typology.ch121✝³).length = Phenomena.Comparison.Typology.ch121✝⁴.length

Per-type counts sum to sample total.

structure Phenomena.Comparison.Typology.ComparativeProfile : Type

A language's comparative construction profile.

• 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 construction 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).

• notes : String

  Notes on the construction.

instance Phenomena.Comparison.Typology.instReprComparativeProfile : Repr ComparativeProfile

Equations

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

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

Equations

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

def Phenomena.Comparison.Typology.english : ComparativeProfile

English: particle comparative with dedicated "than". Dual degree marking: free "more" for polysyllabic adjectives, bound "-er" for short adjectives. Superlative: "-est" or "most". Classic Standard Average European pattern.

Equations

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

def Phenomena.Comparison.Typology.german : ComparativeProfile

German: particle comparative with "als" marking the standard. Comparative formed with suffix "-er" (always synthetic, unlike English). Superlative with "-st" + strong/weak ending. Standard Average European pattern.

Equations

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

def Phenomena.Comparison.Typology.japanese : ComparativeProfile

Japanese: locational comparative with postposition "yori" ('from/than') marking the standard. No comparative morphology on the adjective; the bare adjective form is used. SOV order. Superlative via universal standard "dare yori mo" ('than anyone').

Equations

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

def Phenomena.Comparison.Typology.mandarin : ComparativeProfile

Mandarin Chinese: exceed comparative using "bi" construction. The verb-like element "bi" introduces the standard, functioning as an exceed-type marker. SVO order. Degree adverb "geng" ('more/even more') is optional.

Equations

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

def Phenomena.Comparison.Typology.korean : ComparativeProfile

Korean: locational comparative with ablative-like particle "-boda" marking the standard. Some analyses treat "-boda" as a particle (mixed classification). No comparative morphology on the adjective. SOV order.

Equations

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

def Phenomena.Comparison.Typology.turkish : ComparativeProfile

Turkish: locational comparative with ablative case "-dan"/"-den" marking the standard. Comparative morphology "-rak"/"-rek" exists but is optional. SOV order. Superlative with "en" ('most') + adjective.

Equations

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

def Phenomena.Comparison.Typology.yoruba : ComparativeProfile

Yoruba: exceed comparative using verb "ju" ('surpass/exceed'). The parameter (dimension) of comparison is expressed as a separate predicate. Example: "Ade ga ju Bola lo" 'Ade tall exceed Bola go'. SVO order.

Equations

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

def Phenomena.Comparison.Typology.hindiUrdu : ComparativeProfile

Hindi-Urdu: locational comparative with postposition "se" ('from/than') marking the standard. The comparative adjective is optionally modified by "zyaadaa" ('more'). SOV order.

Equations

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

def Phenomena.Comparison.Typology.russian : ComparativeProfile

Russian: particle comparative with "chem" ('than') or genitive case on the standard. Comparative adjective formed with "-ee"/"-ej" suffix or suppletive stem. Relatively free word order (SVO dominant).

Equations

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

def Phenomena.Comparison.Typology.finnish : ComparativeProfile

Finnish: locational comparative with partitive case marking the standard. Comparative adjective formed with "-mpi" suffix. SOV/SVO flexible order.

Equations

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

def Phenomena.Comparison.Typology.swahili : ComparativeProfile

Swahili: exceed comparative using verb "-zidi" ('exceed/surpass') or "kuliko" ('than/more than'). SVO order. No comparative morphology on adjectives. Bantu language with agglutinative verb morphology.

Equations

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

def Phenomena.Comparison.Typology.latin : ComparativeProfile

Latin: locational comparative with ablative case marking the standard, or particle "quam" ('than'). Comparative adjective formed with "-ior" suffix. Free word order (SOV tendency). Superlative with "-issimus" suffix.

Equations

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

def Phenomena.Comparison.Typology.thai : ComparativeProfile

Thai: exceed comparative using verb "kwaa" ('exceed/more'). SVO order. The adjective precedes "kwaa", which introduces the standard. No comparative morphology.

Equations

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

def Phenomena.Comparison.Typology.tagalog : ComparativeProfile

Tagalog: exceed comparative using "mas...kaysa" construction (borrowed from Spanish "mas...que") or native "higit" ('surpass'). Verb-initial (VSO) order.

Equations

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

def Phenomena.Comparison.Typology.arabic : ComparativeProfile

Arabic (Modern Standard): elative pattern "ʔafʕal" serves as both comparative and superlative. The standard is marked with "min" ('from'). The elative is a fixed morphological template, not decomposable into degree + adjective.

Equations

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

def Phenomena.Comparison.Typology.navajo : ComparativeProfile

Navajo: conjoined comparative. Comparison expressed by juxtaposing two clauses or using the comparative enclitic "-go" with a predicate meaning 'big/much'. Navajo lacks dedicated comparative morphology. SOV order. Athabaskan language.

Equations

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

def Phenomena.Comparison.Typology.martuthunira : ComparativeProfile

Martuthunira (Pama-Nyungan, Western Australia): conjoined comparative. Comparison expressed by juxtaposing two clauses, one asserting the property of the comparee and the other denying it (or asserting the antonym) of the standard. Common Australian pattern.

Equations

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

def Phenomena.Comparison.Typology.french : ComparativeProfile

French: particle comparative with "que" ('than') marking the standard. Degree word "plus" ('more') obligatory. Superlative: "le/la plus" + adjective. Standard Average European pattern.

Equations

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

def Phenomena.Comparison.Typology.allLanguages : List ComparativeProfile

All language profiles in the sample.

Equations

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

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

Does a language have a given comparative type?

Equations

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

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

Does a language have a degree word?

Equations

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

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

Does a language have comparative morphology (bound degree marking)?

Equations

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

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

Does a language lack overt degree marking entirely?

Equations

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

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

Does a language have a morphological superlative?

Equations

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

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

Is this an SOV language?

Equations

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

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

Is this an SVO language?

Equations

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

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

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

Equations

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

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

In the WALS data, locational and particle comparatives together account for more than half of the 167-language sample.

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

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

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

Particle comparatives are the rarest single type in WALS Ch 121 (in the v2020.4 data, which lacks a separate "mixed" category).

def Phenomena.Comparison.Typology.particleLanguages : List ComparativeProfile

In our sample, particle comparative languages are all Indo-European languages of Europe. This reflects @cite{haspelmath-2001}'s identification of the comparative particle as a Standard Average European feature.

Equations

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

theorem Phenomena.Comparison.Typology.particle_languages_count : particleLanguages.length = 4

theorem Phenomena.Comparison.Typology.particle_implies_svo_in_sample : (particleLanguages.all fun (x : ComparativeProfile) => x.isSVO) = true

All particle languages in our sample are SVO (or V2).

def Phenomena.Comparison.Typology.exceedLanguages : List ComparativeProfile

In our sample, exceed comparative languages include Yoruba (W Africa), Mandarin (E Asia), Swahili (E Africa), Thai (SE Asia), and Tagalog (Austronesian). This reflects the areal concentration noted by Stassen.

Equations

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

theorem Phenomena.Comparison.Typology.exceed_languages_count : exceedLanguages.length = 5

def Phenomena.Comparison.Typology.conjoinedLanguages : List ComparativeProfile

Conjoined comparatives are the rarest type in our sample (2/18).

Equations

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

theorem Phenomena.Comparison.Typology.conjoined_languages_count : conjoinedLanguages.length = 2

theorem Phenomena.Comparison.Typology.conjoined_no_degree_marking : (conjoinedLanguages.all fun (x : ComparativeProfile) => x.noDegree) = true

Languages with conjoined comparatives universally lack overt degree marking in our sample: comparison without any morphological apparatus.

def Phenomena.Comparison.Typology.sovLanguages : List ComparativeProfile

SOV languages in our sample (Japanese, Korean, Turkish, Hindi-Urdu, Navajo, Latin) tend toward locational comparatives. In our sample, all SOV languages with a single comparative type use locational (the exceptions being Navajo with conjoined, and Latin which is mixed).

Equations

• Phenomena.Comparison.Typology.sovLanguages = List.filter (fun (x : Phenomena.Comparison.Typology.ComparativeProfile) => x.isSOV) Phenomena.Comparison.Typology.allLanguages

theorem Phenomena.Comparison.Typology.sov_languages_count : sovLanguages.length = 6

theorem Phenomena.Comparison.Typology.sov_locational_dominant : have locCount := countByType sovLanguages ComparativeType.locational; have excCount := countByType sovLanguages ComparativeType.exceed; have parCount := countByType sovLanguages ComparativeType.particle; locCount > excCount ∧ locCount > parCount

Among SOV languages in our sample, locational is the dominant type: more SOV languages use locational than any other single type.

def Phenomena.Comparison.Typology.svoLanguages : List ComparativeProfile

SVO languages in our sample are split between exceed (Mandarin, Yoruba, Swahili, Thai) and particle (English, German, Russian, French) types.

Equations

• Phenomena.Comparison.Typology.svoLanguages = List.filter (fun (x : Phenomena.Comparison.Typology.ComparativeProfile) => x.isSVO) Phenomena.Comparison.Typology.allLanguages

theorem Phenomena.Comparison.Typology.svo_languages_count : svoLanguages.length = 9

theorem Phenomena.Comparison.Typology.svo_exceed_particle_split : have excCount := countByType svoLanguages ComparativeType.exceed; have parCount := countByType svoLanguages ComparativeType.particle; excCount > 0 ∧ parCount > 0

Among SVO languages, exceed and particle types are roughly balanced.

theorem Phenomena.Comparison.Typology.exceed_mostly_no_morphology : have noMorph := List.filter (fun (x : ComparativeProfile) => x.noDegree) exceedLanguages; noMorph.length ≥ 3

Exceed-comparative languages in our sample mostly lack bound comparative morphology on adjectives. Comparison is expressed via the verb.

theorem Phenomena.Comparison.Typology.conjoined_no_superlative : (conjoinedLanguages.all fun (p : ComparativeProfile) => p.superlative == SuperlativeStrategy.none) = true

Languages with conjoined comparatives also lack dedicated superlative strategies in our sample: if you can't grammaticalize "more than", you typically can't grammaticalize "most" either.

theorem Phenomena.Comparison.Typology.morph_comp_implies_morph_super : have morphComp := List.filter (fun (x : ComparativeProfile) => x.hasMorphComp) allLanguages; (morphComp.all fun (x : ComparativeProfile) => x.hasMorphSuperlative) = true

Languages with morphological comparative degree marking (suffix "-er"/"-ee" etc.) also tend to have morphological superlatives. In our sample, every language with morphological comparative degree also has a morphological superlative.

def Phenomena.Comparison.Typology.locationalLanguages : List ComparativeProfile

Every locational comparative in our sample uses a standard marker that also has spatial/ablative meaning ('from', ablative case, partitive case). This is definitional of the locational type but worth verifying: the standard marker is never semantically empty.

Equations

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

theorem Phenomena.Comparison.Typology.locational_languages_count : locationalLanguages.length = 6

theorem Phenomena.Comparison.Typology.locational_has_standard_marker : (locationalLanguages.all fun (p : ComparativeProfile) => p.standardMarker != "") = true

theorem Phenomena.Comparison.Typology.english_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "eng") = some english.comparativeType

theorem Phenomena.Comparison.Typology.japanese_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "jpn") = some japanese.comparativeType

theorem Phenomena.Comparison.Typology.mandarin_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "mnd") = some mandarin.comparativeType

theorem Phenomena.Comparison.Typology.korean_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "kor") = some korean.comparativeType

theorem Phenomena.Comparison.Typology.turkish_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "tur") = some turkish.comparativeType

theorem Phenomena.Comparison.Typology.yoruba_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "yor") = some yoruba.comparativeType

theorem Phenomena.Comparison.Typology.hindiUrdu_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "hin") = some hindiUrdu.comparativeType

theorem Phenomena.Comparison.Typology.russian_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "rus") = some russian.comparativeType

theorem Phenomena.Comparison.Typology.swahili_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "swa") = some swahili.comparativeType

theorem Phenomena.Comparison.Typology.thai_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "tha") = some thai.comparativeType

theorem Phenomena.Comparison.Typology.arabic_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "ams") = some arabic.comparativeType

theorem Phenomena.Comparison.Typology.french_ch121 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F121A.ComparativeType) => Phenomena.Comparison.Typology.fromWALS121A✝ x.value) (Core.WALS.F121A.lookup "fre") = some french.comparativeType

theorem Phenomena.Comparison.Typology.english_is_particle : (english.comparativeType == ComparativeType.particle) = true

theorem Phenomena.Comparison.Typology.german_is_particle : (german.comparativeType == ComparativeType.particle) = true

theorem Phenomena.Comparison.Typology.japanese_is_locational : (japanese.comparativeType == ComparativeType.locational) = true

theorem Phenomena.Comparison.Typology.mandarin_is_exceed : (mandarin.comparativeType == ComparativeType.exceed) = true

theorem Phenomena.Comparison.Typology.korean_is_locational : (korean.comparativeType == ComparativeType.locational) = true

theorem Phenomena.Comparison.Typology.turkish_is_locational : (turkish.comparativeType == ComparativeType.locational) = true

theorem Phenomena.Comparison.Typology.yoruba_is_exceed : (yoruba.comparativeType == ComparativeType.exceed) = true

theorem Phenomena.Comparison.Typology.hindiUrdu_is_locational : (hindiUrdu.comparativeType == ComparativeType.locational) = true

theorem Phenomena.Comparison.Typology.russian_is_particle : (russian.comparativeType == ComparativeType.particle) = true

theorem Phenomena.Comparison.Typology.finnish_is_locational : (finnish.comparativeType == ComparativeType.locational) = true

theorem Phenomena.Comparison.Typology.swahili_is_exceed : (swahili.comparativeType == ComparativeType.exceed) = true

theorem Phenomena.Comparison.Typology.latin_is_mixed : (latin.comparativeType == ComparativeType.mixed) = true

theorem Phenomena.Comparison.Typology.thai_is_exceed : (thai.comparativeType == ComparativeType.exceed) = true

theorem Phenomena.Comparison.Typology.tagalog_is_exceed : (tagalog.comparativeType == ComparativeType.exceed) = true

theorem Phenomena.Comparison.Typology.arabic_is_locational : (arabic.comparativeType == ComparativeType.locational) = true

theorem Phenomena.Comparison.Typology.navajo_is_conjoined : (navajo.comparativeType == ComparativeType.conjoined) = true

theorem Phenomena.Comparison.Typology.martuthunira_is_conjoined : (martuthunira.comparativeType == ComparativeType.conjoined) = true

theorem Phenomena.Comparison.Typology.french_is_particle : (french.comparativeType == ComparativeType.particle) = true

theorem Phenomena.Comparison.Typology.english_has_degree_word : english.hasDegWord = true

theorem Phenomena.Comparison.Typology.japanese_no_degree : japanese.noDegree = true

theorem Phenomena.Comparison.Typology.german_morph_comp : german.hasMorphComp = true

theorem Phenomena.Comparison.Typology.yoruba_no_degree : yoruba.noDegree = true

theorem Phenomena.Comparison.Typology.english_morph_super : english.hasMorphSuperlative = true

theorem Phenomena.Comparison.Typology.french_def_comp_super : (french.superlative == SuperlativeStrategy.definiteComparative) = true

theorem Phenomena.Comparison.Typology.arabic_elative_super : (arabic.superlative == SuperlativeStrategy.elative) = true

theorem Phenomena.Comparison.Typology.navajo_no_super : (navajo.superlative == SuperlativeStrategy.none) = true

theorem Phenomena.Comparison.Typology.particle_has_degree : (particleLanguages.all fun (p : ComparativeProfile) => p.hasDegWord || p.hasMorphComp) = true

Particle comparatives in our sample all have overt degree marking (either a free degree word or comparative morphology): the comparative particle co-occurs with explicit degree semantics.

theorem Phenomena.Comparison.Typology.conjoined_lacks_degree : (conjoinedLanguages.all fun (x : ComparativeProfile) => x.noDegree) = true

Conjoined comparatives in our sample never have degree marking: the absence of a dedicated comparative construction correlates with the absence of dedicated degree morphology.

theorem Phenomena.Comparison.Typology.exceed_degree_split : have withDeg := List.filter (fun (x : ComparativeProfile) => x.hasDegWord) exceedLanguages; have withoutDeg := List.filter (fun (x : ComparativeProfile) => x.noDegree) exceedLanguages; withDeg.length > 0 ∧ withoutDeg.length > 0

Exceed comparatives show a split on degree words: some have overt degree words (Mandarin "geng", Tagalog "mas"), others do not (Yoruba, Swahili, Thai).

theorem Phenomena.Comparison.Typology.sample_locational_count : countByType allLanguages ComparativeType.locational = 6

Sample type distribution: how many languages per comparative type.

theorem Phenomena.Comparison.Typology.sample_exceed_count : countByType allLanguages ComparativeType.exceed = 5

theorem Phenomena.Comparison.Typology.sample_conjoined_count : countByType allLanguages ComparativeType.conjoined = 2

theorem Phenomena.Comparison.Typology.sample_particle_count : countByType allLanguages ComparativeType.particle = 4

theorem Phenomena.Comparison.Typology.sample_mixed_count : countByType allLanguages ComparativeType.mixed = 1

theorem Phenomena.Comparison.Typology.sample_size : allLanguages.length = 18

Number of languages in our sample.

theorem Phenomena.Comparison.Typology.all_types_represented : countByType allLanguages ComparativeType.locational > 0 ∧ countByType allLanguages ComparativeType.exceed > 0 ∧ countByType allLanguages ComparativeType.conjoined > 0 ∧ countByType allLanguages ComparativeType.particle > 0 ∧ countByType allLanguages ComparativeType.mixed > 0

All five comparative types are represented in our sample.

theorem Phenomena.Comparison.Typology.word_order_diversity : have sov := (List.filter (fun (x : ComparativeProfile) => x.isSOV) allLanguages).length; have svo := (List.filter (fun (x : ComparativeProfile) => x.isSVO) allLanguages).length; have vso := (List.filter (fun (p : ComparativeProfile) => p.basicOrder == "VSO" || p.basicOrder == "VSO/SVO") allLanguages).length; sov > 0 ∧ svo > 0 ∧ vso > 0

The sample covers at least 3 word-order types: SOV, SVO, and VSO.

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

Count of languages by degree word type.

Equations

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

theorem Phenomena.Comparison.Typology.sample_degree_word_count : countByDegree allLanguages DegreeWordType.hasDegreeWord = 5

theorem Phenomena.Comparison.Typology.sample_morph_count : countByDegree allLanguages DegreeWordType.morphological = 5

theorem Phenomena.Comparison.Typology.sample_no_degree_count : countByDegree allLanguages DegreeWordType.noDegreeMarking = 8

theorem Phenomena.Comparison.Typology.degree_counts_sum : countByDegree allLanguages DegreeWordType.hasDegreeWord + countByDegree allLanguages DegreeWordType.morphological + countByDegree allLanguages DegreeWordType.noDegreeMarking = allLanguages.length

Degree word presence totals match sample size.

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

Count of languages by superlative strategy.

Equations

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

theorem Phenomena.Comparison.Typology.sample_morph_superlative : countBySuperlative allLanguages SuperlativeStrategy.morphological = 6

theorem Phenomena.Comparison.Typology.sample_def_comp_superlative : countBySuperlative allLanguages SuperlativeStrategy.definiteComparative = 3

theorem Phenomena.Comparison.Typology.sample_exceed_all_superlative : countBySuperlative allLanguages SuperlativeStrategy.exceedAll = 3

theorem Phenomena.Comparison.Typology.sample_comp_univ_superlative : countBySuperlative allLanguages SuperlativeStrategy.comparativeUniversal = 3

theorem Phenomena.Comparison.Typology.sample_elative_superlative : countBySuperlative allLanguages SuperlativeStrategy.elative = 1

theorem Phenomena.Comparison.Typology.sample_no_superlative : countBySuperlative allLanguages SuperlativeStrategy.none = 2

theorem Phenomena.Comparison.Typology.no_comparative_no_superlative : have noDedicated := List.filter (fun (x : ComparativeProfile) => x.hasType ComparativeType.conjoined) allLanguages; (noDedicated.all fun (p : ComparativeProfile) => p.superlative == SuperlativeStrategy.none) = true

Languages that lack a dedicated comparative construction (conjoined type, which is "comparison without comparison" in Stassen's terms) also lack dedicated superlative strategies. This is an implicational universal: SUPERLATIVE → COMPARATIVE (contrapositive: no comparative → no superlative). Our sample data is consistent with this universal.

def Phenomena.Comparison.Typology.japanese1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.japanese1985 = Phenomena.Comparison.Typology.ComparativeType1985.separative

def Phenomena.Comparison.Typology.korean1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.korean1985 = Phenomena.Comparison.Typology.ComparativeType1985.separative

def Phenomena.Comparison.Typology.turkish1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.turkish1985 = Phenomena.Comparison.Typology.ComparativeType1985.separative

def Phenomena.Comparison.Typology.hindiUrdu1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.hindiUrdu1985 = Phenomena.Comparison.Typology.ComparativeType1985.separative

def Phenomena.Comparison.Typology.arabic1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.arabic1985 = Phenomena.Comparison.Typology.ComparativeType1985.separative

def Phenomena.Comparison.Typology.navajo1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.navajo1985 = Phenomena.Comparison.Typology.ComparativeType1985.locative

def Phenomena.Comparison.Typology.mandarin1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.mandarin1985 = Phenomena.Comparison.Typology.ComparativeType1985.exceed

def Phenomena.Comparison.Typology.yoruba1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.yoruba1985 = Phenomena.Comparison.Typology.ComparativeType1985.exceed

def Phenomena.Comparison.Typology.swahili1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.swahili1985 = Phenomena.Comparison.Typology.ComparativeType1985.exceed

def Phenomena.Comparison.Typology.thai1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.thai1985 = Phenomena.Comparison.Typology.ComparativeType1985.exceed

def Phenomena.Comparison.Typology.english1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.english1985 = Phenomena.Comparison.Typology.ComparativeType1985.particle

def Phenomena.Comparison.Typology.russian1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.russian1985 = Phenomena.Comparison.Typology.ComparativeType1985.particle

def Phenomena.Comparison.Typology.finnish1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.finnish1985 = Phenomena.Comparison.Typology.ComparativeType1985.particle

def Phenomena.Comparison.Typology.latin1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.latin1985 = Phenomena.Comparison.Typology.ComparativeType1985.particle

def Phenomena.Comparison.Typology.french1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Typology.french1985 = Phenomena.Comparison.Typology.ComparativeType1985.particle

theorem Phenomena.Comparison.Typology.adverbial_collapse : ComparativeType1985.separative.toWALS = ComparativeType.locational ∧ ComparativeType1985.allative.toWALS = ComparativeType.locational ∧ ComparativeType1985.locative.toWALS = ComparativeType.locational

The three adverbial types all collapse to locational under WALS.

theorem Phenomena.Comparison.Typology.derived_case_not_locational (t : ComparativeType1985) (h : t.caseAssignment = Core.CaseAssignment.derived) : t.toWALS ≠ ComparativeType.locational

Derived-case types never map to locational.

theorem Phenomena.Comparison.Typology.fixed_case_not_particle (t : ComparativeType1985) (h : t.caseAssignment = Core.CaseAssignment.fixed) : t.toWALS ≠ ComparativeType.particle

Fixed-case types never map to particle.

theorem Phenomena.Comparison.Typology.adverbial_is_fixed (t : ComparativeType1985) (h : t.fixedEncoding = some Core.FixedCaseEncoding.adverbial) : t.caseAssignment = Core.CaseAssignment.fixed

Every adverbial type is fixed-case (by construction).

theorem Phenomena.Comparison.Typology.japanese_consistent : japanese1985.toWALS = japanese.comparativeType

theorem Phenomena.Comparison.Typology.korean_consistent : korean1985.toWALS = korean.comparativeType

theorem Phenomena.Comparison.Typology.turkish_consistent : turkish1985.toWALS = turkish.comparativeType

theorem Phenomena.Comparison.Typology.hindiUrdu_consistent : hindiUrdu1985.toWALS = hindiUrdu.comparativeType

theorem Phenomena.Comparison.Typology.arabic_consistent : arabic1985.toWALS = arabic.comparativeType

theorem Phenomena.Comparison.Typology.mandarin_consistent : mandarin1985.toWALS = mandarin.comparativeType

theorem Phenomena.Comparison.Typology.yoruba_consistent : yoruba1985.toWALS = yoruba.comparativeType

theorem Phenomena.Comparison.Typology.swahili_consistent : swahili1985.toWALS = swahili.comparativeType

theorem Phenomena.Comparison.Typology.thai_consistent : thai1985.toWALS = thai.comparativeType

theorem Phenomena.Comparison.Typology.english_consistent : english1985.toWALS = english.comparativeType

theorem Phenomena.Comparison.Typology.russian_consistent : russian1985.toWALS = russian.comparativeType

theorem Phenomena.Comparison.Typology.french_consistent : french1985.toWALS = french.comparativeType

inductive Phenomena.Comparison.Typology.ComparisonConstruction : Type

The major comparison construction types found cross-linguistically.

• comparative : ComparisonConstruction
• equative : ComparisonConstruction
• superlative : ComparisonConstruction
• excessive : ComparisonConstruction
• sufficiency : ComparisonConstruction
• degreeQuestion : ComparisonConstruction

instance Phenomena.Comparison.Typology.instDecidableEqComparisonConstruction : DecidableEq ComparisonConstruction

Equations

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

instance Phenomena.Comparison.Typology.instBEqComparisonConstruction : BEq ComparisonConstruction

Equations

• Phenomena.Comparison.Typology.instBEqComparisonConstruction = { beq := Phenomena.Comparison.Typology.instBEqComparisonConstruction.beq }

def Phenomena.Comparison.Typology.instBEqComparisonConstruction.beq : ComparisonConstruction → ComparisonConstruction → Bool

Equations

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

def Phenomena.Comparison.Typology.instReprComparisonConstruction.repr : ComparisonConstruction → Nat → Std.Format

Equations

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

instance Phenomena.Comparison.Typology.instReprComparisonConstruction : Repr ComparisonConstruction

Equations

• Phenomena.Comparison.Typology.instReprComparisonConstruction = { reprPrec := Phenomena.Comparison.Typology.instReprComparisonConstruction.repr }

inductive Phenomena.Comparison.Typology.ComparisonDomain : Type

What is being compared — the syntactic category of the gradable expression, following @cite{wellwood-2015}.

The key insight: comparison constructions apply uniformly across categories; what varies is the measured domain (entity, event, state).

• adjectival : ComparisonDomain
• nominal : ComparisonDomain
• verbal : ComparisonDomain
• adverbial : ComparisonDomain

instance Phenomena.Comparison.Typology.instDecidableEqComparisonDomain : DecidableEq ComparisonDomain

Equations

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

instance Phenomena.Comparison.Typology.instBEqComparisonDomain : BEq ComparisonDomain

Equations

• Phenomena.Comparison.Typology.instBEqComparisonDomain = { beq := Phenomena.Comparison.Typology.instBEqComparisonDomain.beq }

def Phenomena.Comparison.Typology.instBEqComparisonDomain.beq : ComparisonDomain → ComparisonDomain → Bool

Equations

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

def Phenomena.Comparison.Typology.instReprComparisonDomain.repr : ComparisonDomain → Nat → Std.Format

Equations

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

instance Phenomena.Comparison.Typology.instReprComparisonDomain : Repr ComparisonDomain

Equations

• Phenomena.Comparison.Typology.instReprComparisonDomain = { reprPrec := Phenomena.Comparison.Typology.instReprComparisonDomain.repr }

inductive Phenomena.Comparison.Typology.DegreeMorphology : Type

How degree comparison is morphologically realized in a given form.

This is orthogonal to DegreeWordType (above), which classifies whether a language has degree marking at all. DegreeMorphology classifies a specific form: English "taller" is synthetic, "more tall" is analytic, "better" is suppletive — all in a language that DegreeWordType classifies as .hasDegreeWord.

• synthetic : DegreeMorphology
• analytic : DegreeMorphology
• suppletive : DegreeMorphology
• mixed : DegreeMorphology

instance Phenomena.Comparison.Typology.instDecidableEqDegreeMorphology : DecidableEq DegreeMorphology

Equations

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

def Phenomena.Comparison.Typology.instBEqDegreeMorphology.beq : DegreeMorphology → DegreeMorphology → Bool

Equations

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

instance Phenomena.Comparison.Typology.instBEqDegreeMorphology : BEq DegreeMorphology

Equations

• Phenomena.Comparison.Typology.instBEqDegreeMorphology = { beq := Phenomena.Comparison.Typology.instBEqDegreeMorphology.beq }

instance Phenomena.Comparison.Typology.instReprDegreeMorphology : Repr DegreeMorphology

Equations

• Phenomena.Comparison.Typology.instReprDegreeMorphology = { reprPrec := Phenomena.Comparison.Typology.instReprDegreeMorphology.repr }

def Phenomena.Comparison.Typology.instReprDegreeMorphology.repr : DegreeMorphology → Nat → Std.Format

Equations

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