Comparative constructions

A comparative construction, X is taller than Y, marks the standard of comparison Y and may mark the degree on the predicate. Stassen classifies constructions by the case of the standard, which is derived from the case of the comparee or fixed by the construction, and by the role of a fixed-case standard, the object of a verb of exceeding or an adverbial. This file defines the construction by these parameters and derives from them its type in Stassen's chapter of the World Atlas of Language Structures, whose sample it also counts.

Main definitions

• Comparative: a construction, with the marker of its standard and its markers of degree as morphs.
• Comparative.type: the type of a construction in the atlas.
• Comparative.SuperlativeStrategy: the ways a language forms superlatives.

References

• [Sta85]
• [Sta13b]
• [DH13b]

inductive Comparative.CaseAssignment : Type

The standard of a comparative takes its case from the comparee or has one case that the construction fixes ([Sta85] §2.2.1).

• derived : CaseAssignment
• fixed : CaseAssignment

@[instance_reducible]

instance Comparative.instDecidableEqCaseAssignment : DecidableEq CaseAssignment

Equations

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

def Comparative.instReprCaseAssignment.repr : CaseAssignment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Comparative.instReprCaseAssignment : Repr CaseAssignment

Equations

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

inductive Comparative.FixedCaseEncoding : Type

A fixed-case standard is the direct object of a transitive verb of exceeding or an adverbial ([Sta85] §2.2.2).

• directObject : FixedCaseEncoding
• adverbial : FixedCaseEncoding

@[instance_reducible]

instance Comparative.instDecidableEqFixedCaseEncoding : DecidableEq FixedCaseEncoding

Equations

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

def Comparative.instReprFixedCaseEncoding.repr : FixedCaseEncoding → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Comparative.instReprFixedCaseEncoding : Repr FixedCaseEncoding

Equations

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

structure Comparative : Type

A comparative construction, by the way it encodes the standard of comparison in X is more Adj than Y, in the parameters of [Sta85]. A language may have more than one, as Latin has quam and the bare ablative.

• standardMarker : List Morphology.Morph

  The marker of the standard as the morphs of its form in order, than or the two pieces of Yoruba ju … lọ. It is empty where no segmental marker flags the standard, as in a conjoined construction and with a bare case-marked standard like the Latin ablative.

• caseAssignment : CaseAssignment

  The standard takes its case from the comparee or has a case the construction fixes.

• fixedEncoding : Option FixedCaseEncoding

  The role of a fixed-case standard, the object of a verb of exceeding or an adverbial.

• standardCase : Option Case

  The case of an adverbially encoded standard, the ablative of a separative and the partitive of the Finnish secondary construction. An adposition with the meaning of the case counts, as Japanese yori and Arabic min do for the ablative.

• degreeMarkers : List Morphology.Morph

  The markers of degree on the predicate, each an alternative, as English more and -er. A bound marker is degree morphology and a free one a degree word, and the list is empty where the construction marks no degree.

@[instance_reducible]

instance instReprComparative : Repr Comparative

Equations

• instReprComparative = { reprPrec := instReprComparative.repr }

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

Equations

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

@[instance_reducible]

instance instBEqComparative : BEq Comparative

Equations

• instBEqComparative = { beq := instBEqComparative.beq }

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

@[reducible, inline]

abbrev Comparative.ch121 : List (String × Data.WALS.F121A.ComparativeType)

Equations

• Comparative.ch121 = Data.WALS.F121A.allData

Classifications

inductive Comparative.ComparativeType : Type

The type of a comparative construction in the atlas, by how it encodes the standard of comparison. A language with more than one productive construction has one Comparative for each, with its own type.

• locational : ComparativeType

  The standard is marked with a locational or ablative case or adposition, as in Japanese Y yori X tall, Turkish, Hindi-Urdu and the Latin ablative.

• exceed : ComparativeType

  A verb meaning 'exceed' or 'surpass' encodes the comparison, as in Yoruba Ade ga ju Bola lo.

• conjoined : ComparativeType

  Two juxtaposed clauses, one attributing the property to X and the other denying it of Y or contrasting it.

• particle : ComparativeType

  A dedicated comparative particle marks the standard, as English than and German als do.

@[instance_reducible]

instance Comparative.instDecidableEqComparativeType : DecidableEq ComparativeType

Equations

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

@[instance_reducible]

instance Comparative.instBEqComparativeType : BEq ComparativeType

Equations

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

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

Equations

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

@[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.SuperlativeStrategy : Type

The ways a language forms superlatives, which are partly independent of its comparative type.

• morphological : SuperlativeStrategy

  Dedicated superlative morphology, as English -est and Latin -issimus.

• definiteComparative : SuperlativeStrategy

  The definite article with the comparative, as French le plus grand.

• elative : SuperlativeStrategy

  The elative pattern without a comparison class, as Arabic ʔafʕal.

• exceedAll : SuperlativeStrategy

  A verb of exceeding with a universal quantifier, 'X exceeds all'.

• comparativeUniversal : SuperlativeStrategy

  The comparative with a universal standard, as 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 type of a construction in the atlas, derived from its anatomy. A derived-case construction is a particle comparative when it has a standard marker and a conjoined one otherwise, and a fixed-case construction is an exceed comparative when the standard is a direct object and a locational one otherwise.

Equations

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

Counts over the sample of the atlas

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

The four types exhaust the sample.

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

Locational comparatives are the most common type in the sample.

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

Particle comparatives are the rarest type in the sample.

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

Locational and particle comparatives together are more than half the sample.