Rett 2020: Separate but Equal — A Typology of Equative Constructions

[rett-2020-equatives] replicates the descriptive and theoretical typologies of comparatives for equatives. Descriptively (§3, after Henkelmann 2006 and Haspelmath & Buchholz 1998), languages mark equatives by relative strategies (a degree-relativizer standard marker, with or without a parameter marker), predicate strategies (a main predicate 'equal' or an adverbial 'equally'), conjoined clauses, case-marked standards, or dedicated morphemes. Theoretically (Figure 3), predicative equatives lack weak "at least" readings; non-predicative equatives split into explicit (parameter-marked) and implicit (unmarked, evaluative) — and explicit equatives split again (§4.3) into sufficientive parameter markers (English as, degree quantifiers, modifiable by twice) and degree-demonstrative parameter markers (Italian tanto, unmodifiable).

Only the sufficientive strategy involves degree quantification (§5); its set-based ⟦as⟧ ((5-b)) relates degree sets by inclusion, which at extent sets is exactly the point-standard equative (setBasedAs_iff_equativeSem).

Descriptive strategies (§3)

inductive Rett2020Equatives.Strategy : Type

An equative-marking strategy: the descriptive classes of §3, with parameter-marked relatives split per §4.3 and the Appendix.

• relativeSMOnly : Strategy

  Relativizer standard marker only ("Jane is tall like Bill"; Italian come, Serbo-Croatian kao).

• relativeDemonstrative : Strategy

  Degree-demonstrative parameter marker plus relativizer standard marker (Italian tanto...quanto, Spanish tan...como).

• relativeSufficientive : Strategy

  Sufficientive parameter marker plus relativizer standard marker (English as...as, German so...wie).

• predicateMain : Strategy

  Main predicate meaning 'equal' (Nkore-Kiga -ingana).

• predicateAdverbial : Strategy

  Adverbial meaning 'equally, to the same extent' (Mandarin yíyàng).

• conjoined : Strategy

  Conjoined parallel clauses, often with an additive particle (Mangarayi).

• caseMarkedStandard : Strategy

  Case marker or preposition as standard marker (Japanese, Greenlandic).

• dedicated : Strategy

  Construction-specific markers with no transparent etymology (Welsh).

@[instance_reducible]

instance Rett2020Equatives.instDecidableEqStrategy : DecidableEq Strategy

Equations

• Rett2020Equatives.instDecidableEqStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2020Equatives.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rett2020Equatives.instReprStrategy : Repr Strategy

Equations

• Rett2020Equatives.instReprStrategy = { reprPrec := Rett2020Equatives.instReprStrategy.repr }

inductive Rett2020Equatives.TheoreticalClass : Type

Theoretical classes (Figure 3).

• predicative : TheoreticalClass
• explicitSufficientive : TheoreticalClass
• explicitDemonstrative : TheoreticalClass
• implicit : TheoreticalClass

@[instance_reducible]

instance Rett2020Equatives.instDecidableEqTheoreticalClass : DecidableEq TheoreticalClass

Equations

• Rett2020Equatives.instDecidableEqTheoreticalClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2020Equatives.instReprTheoreticalClass.repr : TheoreticalClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rett2020Equatives.instReprTheoreticalClass : Repr TheoreticalClass

Equations

• Rett2020Equatives.instReprTheoreticalClass = { reprPrec := Rett2020Equatives.instReprTheoreticalClass.repr }

def Rett2020Equatives.Strategy.theoretical : Strategy → Option TheoreticalClass

Figure 3's classification. Predicate subtypes pattern together (fn. 11); SM-only relatives and conjoined equatives are implicit by the §4.1 diagnostics; case-marked and dedicated strategies are left for future research (§5).

Equations

• Rett2020Equatives.Strategy.relativeSMOnly.theoretical = some Rett2020Equatives.TheoreticalClass.implicit
• Rett2020Equatives.Strategy.relativeDemonstrative.theoretical = some Rett2020Equatives.TheoreticalClass.explicitDemonstrative
• Rett2020Equatives.Strategy.relativeSufficientive.theoretical = some Rett2020Equatives.TheoreticalClass.explicitSufficientive
• Rett2020Equatives.Strategy.predicateMain.theoretical = some Rett2020Equatives.TheoreticalClass.predicative
• Rett2020Equatives.Strategy.predicateAdverbial.theoretical = some Rett2020Equatives.TheoreticalClass.predicative
• Rett2020Equatives.Strategy.conjoined.theoretical = some Rett2020Equatives.TheoreticalClass.implicit
• Rett2020Equatives.Strategy.caseMarkedStandard.theoretical = none
• Rett2020Equatives.Strategy.dedicated.theoretical = none

structure Rett2020Equatives.TypologyDatum : Type

A language's equative strategy with the paper's example form and location.

• language : String
• strategy : Strategy
• form : String
• source : String

  Example number or Appendix row.

def Rett2020Equatives.instReprTypologyDatum.repr : TypologyDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rett2020Equatives.instReprTypologyDatum : Repr TypologyDatum

Equations

• Rett2020Equatives.instReprTypologyDatum = { reprPrec := Rett2020Equatives.instReprTypologyDatum.repr }

def Rett2020Equatives.typology : List TypologyDatum

Per-language strategies; a language may use several (English (50)).

Equations

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

Diagnostics for explicit equatives (Figure 2)

structure Rett2020Equatives.ExplicitDiagnostics : Type

A row of Figure 2: a parameter-marked relative equative with its subtype and diagnostic values. none records the paper's uncertain cells.

• language : String
• pm : String
• subtype : Strategy
• modifiable : Option Bool
• evaluative : Option Bool
• weakReading : Option Bool

def Rett2020Equatives.instReprExplicitDiagnostics.repr : ExplicitDiagnostics → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rett2020Equatives.instReprExplicitDiagnostics : Repr ExplicitDiagnostics

Equations

• Rett2020Equatives.instReprExplicitDiagnostics = { reprPrec := Rett2020Equatives.instReprExplicitDiagnostics.repr }

def Rett2020Equatives.figure2 : List ExplicitDiagnostics

Figure 2's table. Slovenian's uncertain cells and Spanish's uncertain modifiability (the consultants' "unnatural" vs Italian's ungrammatical, fn. 15 and surrounding text) are none.

Equations

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

theorem Rett2020Equatives.sufficientive_iff_modifiable (r : ExplicitDiagnostics) : r ∈ figure2 → (r.modifiable = some true ↔ r.subtype = Strategy.relativeSufficientive)

Figure 2's generalization: among explicit equatives, factor-modifiability holds exactly of the sufficientive parameter markers — the diagnostic that splits explicit equatives into two subtypes.

theorem Rett2020Equatives.explicit_not_evaluative (r : ExplicitDiagnostics) : r ∈ figure2 → r.evaluative = some true → False

Explicit equatives of both subtypes are non-evaluative wherever Figure 2 records a value.

The sufficientive equative as a degree quantifier

def Rett2020Equatives.setBasedAs {D : Type u_1} (std tgt : Set D) : Prop

The set-based sufficientive ⟦as⟧ ((5-b)): the standard's degree set is included in the target's.

Equations

• Rett2020Equatives.setBasedAs std tgt = (std ⊆ tgt)

theorem Rett2020Equatives.setBasedAs_iff_equativeSem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : setBasedAs (Set.Iic (μ b)) (Set.Iic (μ a)) ↔ Degree.equativeSem μ a b Core.Order.ScalePolarity.positive

At extent sets, the set-based ⟦as⟧ is the point-standard equative: the degree-quantificational sufficientive strategy coincides with Degree.equativeSem over a measure function.