Comparison: comparative-construction typology

The Comparative object — a comparative construction's anatomy in [Sta85]'s parameters, with its WALS Ch 121 type ([Sta13b], [DH13b]) derived from that anatomy — plus the [BKF+09] degree-word typology, superlative strategies, and the WALS Ch 121A lookup and aggregates.

Main definitions

• Comparative : the construction object (standard marker, case assignment, encoding role, spatial case, degree slot). Fragments instantiate one def per construction (German.Comparison.als; Latin has quam and ablative).
• Comparative.type : the WALS Ch 121 type, derived from the anatomy — derived-case constructions split on marker presence (particle vs conjoined), fixed-case constructions on encoding role (exceed vs locational).
• DegreeWordType ([BKF+09] 3-way), SuperlativeStrategy (6-way).
• ComparativeType.ofWALS : WALS Ch 121A comparative type by ISO 639-3 lookup; none for languages the chapter leaves uncoded.
• WALS Ch 121A aggregate generalisations (locational_most_common, particle_rarest, locational_and_particle_dominant).

Stassen's 1985 fine-grained adverbial typology (ComparativeType1985, the chaining universals) lives in Studies/Stassen1985.lean (paper-anchored).

structure Comparative : Type

A comparative construction: how it encodes the standard of comparison in "X is more Adj than Y" — [Sta85]'s construction parameters. A language may have more than one (Latin quam and the bare ablative). Coexists with namespace Comparative (a type and a namespace may share a name, cf. Pronoun).

• standardMarker : Option String

  Surface form of the standard marker (than, als, yori, bǐ); none when no segmental marker flags the standard (conjoined constructions, bare case-marked standards like the Latin ablative).

• caseAssignment : Features.CaseAssignment

  Case assignment to the standard NP: derived from the comparee's case vs fixed by the construction ([Sta85]).

• fixedEncoding : Option Features.FixedCaseEncoding

  For fixed-case constructions: the standard's syntactic role — direct object of an exceed verb, or adverbial.

• standardCase : Option Case

  Case on an adverbially encoded standard (ablative for separatives, partitive for the Finnish secondary option). Adpositions with the corresponding semantics count (Japanese yori, Arabic min → abl).

• degreeMarker : Option String

  The construction's degree-slot filler (more, -er, daha), if any.

• degreeMorphology : Bool

  Dedicated bound degree morphology on the parameter (English -er, Latin -ior) — [Sta85]'s binary parameter.

def instReprComparative.repr : Comparative → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprComparative : Repr Comparative

Equations

• instReprComparative = { reprPrec := instReprComparative.repr }

def instBEqComparative.beq : Comparative → Comparative → Bool

Equations

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

@[instance_reducible]

instance instBEqComparative : BEq Comparative

Equations

• instBEqComparative = { beq := instBEqComparative.beq }

@[instance_reducible]

instance instDecidableEqComparative : DecidableEq Comparative

Equations

• instDecidableEqComparative = instDecidableEqComparative.decEq

def instDecidableEqComparative.decEq (x✝ x✝¹ : Comparative) : Decidable (x✝ = x✝¹)

Equations

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

Classifications

inductive Comparative.ComparativeType : Type

WALS Ch 121: how a comparative construction encodes the standard of comparison (the Y in "X is more Adj than Y"). A language with more than one productive construction has one Comparative object per construction, each with its own type.

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

@[instance_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)

@[instance_reducible]

instance Comparative.instBEqComparativeType : BEq ComparativeType

Equations

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

@[instance_reducible]

instance Comparative.instReprComparativeType : Repr ComparativeType

Equations

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

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

Equations

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

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

@[instance_reducible]

instance Comparative.instDecidableEqDegreeWordType : DecidableEq DegreeWordType

Equations

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

@[instance_reducible]

instance Comparative.instBEqDegreeWordType : BEq DegreeWordType

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Comparative.instReprDegreeWordType : Repr DegreeWordType

Equations

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

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.

@[instance_reducible]

instance Comparative.instDecidableEqSuperlativeStrategy : DecidableEq SuperlativeStrategy

Equations

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

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

Equations

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

@[instance_reducible]

instance Comparative.instBEqSuperlativeStrategy : BEq SuperlativeStrategy

Equations

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

@[instance_reducible]

instance Comparative.instReprSuperlativeStrategy : Repr SuperlativeStrategy

Equations

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

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

Equations

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

The derived type

def Comparative.type (c : Comparative) : ComparativeType

The WALS Ch 121 type of a construction, derived from its anatomy: derived-case constructions split on marker presence (particle vs conjoined); fixed-case constructions on encoding role (exceed vs locational, with adverbial the default).

Equations

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

WALS lookups

def Comparative.ofWALS121A : Data.WALS.F121A.ComparativeType → ComparativeType

WALS Ch 121A → ComparativeType.

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.ComparativeType.ofWALS (iso : String) : Option ComparativeType

WALS Ch 121A comparative type for an ISO 639-3 code; none when the language is uncoded in the chapter.

Equations

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

WALS Ch 121A aggregate generalisations

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.