Haspelmath (2025): Nonverbal Clause Constructions

Haspelmath surveys the clauses that lack a typical verb and fixes a term for each of eight types, defined by meaning. A duonominal clause puts two nominals in correspondence: it is classificational when the second nominal is indefinite and equational when it is definite. An attributional clause ascribes a property. A locopossessional clause is about location or possession: it is predlocative or appertentive when the nominal that is located or possessed is definite, and existential or predpossessive when it is indefinite. A hyparctic clause expresses existence regardless of location. Four of the eight types divide into a subject and a predicate.

Forms are classified by the types they occur in. A copula links the two argument positions of an equational, ascriptive or locational clause, and an existive is a copula found only in existential and predpossessive clauses. A strategy is a way of building one type that is defined by form.

Main statements

• Construction.predicational_iff: the types with a subject and a predicate are the classificational, attributional, predlocative and appertentive ones.
• isExistive_iff: a form is an existive exactly when it occurs in existential clauses and in no clauses but existential and predpossessive ones.
• existive_gloss_hyparctic: the Hamar form the paper glosses as an existive occurs in a hyparctic clause, which the definition of an existive excludes.
• finnish_adessive: the possessor and the location of the Finnish examples are adessives of the Finnish fragment, and the adessive is a place case.

Implementation notes

• The definiteness of the second nominal, and of the located or possessed nominal, is an argument of the constructor. The grid of the four locopossessional types then holds by construction, and the cover terms are conditions on the arguments.
• A form is represented by the set of constructions it occurs in, so IsCopula and IsExistive are conditions on such a set. That a copula is an overt form is not represented.
• The construction of a row is the type the paper prints with the example, or the type its strategy builds.

TODO

• The rows hold the examples that introduce the types, the duonominal pairs, the strategy examples, the Turkish and Spanish examples of the section on copulas, the Mandinka example and the hyparctic ones. The paper's other examples are not entered, nor are the subtypes of the equational and existential types or the minor predicate types.
• The conditions that define the strategies are not stated over rows. Only the locative flag of the Finnish examples is checked, against the fragment.

References

• [Has25b]
• [Cla78]

The eight constructions

inductive Haspelmath2025a.Domain : Type

The two domains of a locopossessional clause.

• locational : Domain
• possessional : Domain

@[instance_reducible]

instance Haspelmath2025a.instDecidableEqDomain : DecidableEq Domain

Equations

• Haspelmath2025a.instDecidableEqDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Haspelmath2025a.instReprDomain.repr : Domain → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025a.instReprDomain : Repr Domain

Equations

• Haspelmath2025a.instReprDomain = { reprPrec := Haspelmath2025a.instReprDomain.repr }

@[instance_reducible]

instance Haspelmath2025a.instFintypeDomain : Fintype Domain

Equations

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

inductive Haspelmath2025a.Construction : Type

The nonverbal clause constructions. A duonominal clause carries the definiteness of its second nominal, and a locopossessional clause its domain and the definiteness of the nominal that is located or possessed.

• duonominal (second : Reference.Definiteness) : Construction

  Two nominals in correspondence.

• attributional : Construction

  A property ascribed to the subject, The bird is small.

• locopossessional (domain : Domain) (d : Reference.Definiteness) : Construction

  A clause about location or possession, [Cla78]'s locationals.

• hyparctic : Construction

  Existence regardless of location, God exists.

def Haspelmath2025a.instDecidableEqConstruction.decEq (x✝ x✝¹ : Construction) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.duonominal a) (Haspelmath2025a.Construction.duonominal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.duonominal second) Haspelmath2025a.Construction.attributional = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.duonominal second) (Haspelmath2025a.Construction.locopossessional domain d) = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.duonominal second) Haspelmath2025a.Construction.hyparctic = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq Haspelmath2025a.Construction.attributional (Haspelmath2025a.Construction.duonominal second) = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq Haspelmath2025a.Construction.attributional Haspelmath2025a.Construction.attributional = isTrue ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq Haspelmath2025a.Construction.attributional (Haspelmath2025a.Construction.locopossessional domain d) = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.locopossessional domain d) (Haspelmath2025a.Construction.duonominal second) = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.locopossessional domain d) Haspelmath2025a.Construction.attributional = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq (Haspelmath2025a.Construction.locopossessional domain d) Haspelmath2025a.Construction.hyparctic = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq Haspelmath2025a.Construction.hyparctic (Haspelmath2025a.Construction.duonominal second) = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq Haspelmath2025a.Construction.hyparctic (Haspelmath2025a.Construction.locopossessional domain d) = isFalse ⋯
• Haspelmath2025a.instDecidableEqConstruction.decEq Haspelmath2025a.Construction.hyparctic Haspelmath2025a.Construction.hyparctic = isTrue ⋯

@[instance_reducible]

instance Haspelmath2025a.instDecidableEqConstruction : DecidableEq Construction

Equations

• Haspelmath2025a.instDecidableEqConstruction = Haspelmath2025a.instDecidableEqConstruction.decEq

@[instance_reducible]

instance Haspelmath2025a.instReprConstruction : Repr Construction

Equations

• Haspelmath2025a.instReprConstruction = { reprPrec := Haspelmath2025a.instReprConstruction.repr }

def Haspelmath2025a.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025a.instFintypeConstruction : Fintype Construction

Equations

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

@[reducible, inline]

abbrev Haspelmath2025a.Construction.classificational : Construction

A definite subject and an indefinite classificatory nominal, Lee is a baker.

Equations

• Haspelmath2025a.Construction.classificational = Haspelmath2025a.Construction.duonominal Reference.Definiteness.indefinite

@[reducible, inline]

abbrev Haspelmath2025a.Construction.equational : Construction

Two definite nominals, Kim is my mother.

Equations

• Haspelmath2025a.Construction.equational = Haspelmath2025a.Construction.duonominal Reference.Definiteness.definite

@[reducible, inline]

abbrev Haspelmath2025a.Construction.predlocative : Construction

A definite nominal located by a locative phrase, The bird is on the roof.

Equations

• Haspelmath2025a.Construction.predlocative = Haspelmath2025a.Construction.locopossessional Haspelmath2025a.Domain.locational Reference.Definiteness.definite

@[reducible, inline]

abbrev Haspelmath2025a.Construction.existential : Construction

An indefinite nominal said to be in a location, There is a bird on the roof.

Equations

• Haspelmath2025a.Construction.existential = Haspelmath2025a.Construction.locopossessional Haspelmath2025a.Domain.locational Reference.Definiteness.indefinite

@[reducible, inline]

abbrev Haspelmath2025a.Construction.appertentive : Construction

A definite nominal said to belong to a possessor, The boat belongs to me.

Equations

• Haspelmath2025a.Construction.appertentive = Haspelmath2025a.Construction.locopossessional Haspelmath2025a.Domain.possessional Reference.Definiteness.definite

@[reducible, inline]

abbrev Haspelmath2025a.Construction.predpossessive : Construction

An indefinite nominal said to be possessed, I have a boat.

Equations

• Haspelmath2025a.Construction.predpossessive = Haspelmath2025a.Construction.locopossessional Haspelmath2025a.Domain.possessional Reference.Definiteness.indefinite

Cover terms

def Haspelmath2025a.Construction.Ascriptive (t : Construction) : Prop

An ascriptive clause ascribes a concept to its subject.

Equations

• t.Ascriptive = (t = Haspelmath2025a.Construction.classificational ∨ t = Haspelmath2025a.Construction.attributional)

def Haspelmath2025a.Construction.Locational (t : Construction) : Prop

A locational clause is about location.

Equations

• t.Locational = ∃ (d : Reference.Definiteness), t = Haspelmath2025a.Construction.locopossessional Haspelmath2025a.Domain.locational d

def Haspelmath2025a.Construction.Possessional (t : Construction) : Prop

A possessional clause is about possession.

Equations

• t.Possessional = ∃ (d : Reference.Definiteness), t = Haspelmath2025a.Construction.locopossessional Haspelmath2025a.Domain.possessional d

@[instance_reducible]

instance Haspelmath2025a.Construction.instDecidablePredAscriptive : DecidablePred Ascriptive

Equations

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

@[instance_reducible]

instance Haspelmath2025a.Construction.instDecidablePredLocational : DecidablePred Locational

Equations

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

@[instance_reducible]

instance Haspelmath2025a.Construction.instDecidablePredPossessional : DecidablePred Possessional

Equations

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

theorem Haspelmath2025a.Construction.locational_iff (t : Construction) : t.Locational ↔ t = predlocative ∨ t = existential

theorem Haspelmath2025a.Construction.possessional_iff (t : Construction) : t.Possessional ↔ t = appertentive ∨ t = predpossessive

Predicational clauses

def Haspelmath2025a.Construction.Predicational : Construction → Prop

A predicational clause divides into a subject and a predicate. A duonominal clause does when its second nominal is indefinite, and a locopossessional clause when the located or possessed nominal is definite, the locative phrase or the possessor then being the predicate.

Equations

• (Haspelmath2025a.Construction.duonominal a).Predicational = (a = Reference.Definiteness.indefinite)
• Haspelmath2025a.Construction.attributional.Predicational = True
• (Haspelmath2025a.Construction.locopossessional a a_1).Predicational = (a_1 = Reference.Definiteness.definite)
• Haspelmath2025a.Construction.hyparctic.Predicational = False

@[instance_reducible]

instance Haspelmath2025a.Construction.instDecidablePredPredicational : DecidablePred Predicational

Equations

• (Haspelmath2025a.Construction.duonominal second).instDecidablePredPredicational = Haspelmath2025a.Construction.instDecidablePredPredicational._aux_1 second
• (Haspelmath2025a.Construction.locopossessional domain d).instDecidablePredPredicational = Haspelmath2025a.Construction.instDecidablePredPredicational._aux_3 domain d
• Haspelmath2025a.Construction.attributional.instDecidablePredPredicational = isTrue trivial
• Haspelmath2025a.Construction.hyparctic.instDecidablePredPredicational = isFalse Haspelmath2025a.Construction.instDecidablePredPredicational._proof_1

theorem Haspelmath2025a.Construction.predicational_iff (t : Construction) : t.Predicational ↔ t = classificational ∨ t = attributional ∨ t = predlocative ∨ t = appertentive

The predicational types are the classificational, attributional, predlocative and appertentive ones; the equational, existential, predpossessive and hyparctic types are not.

The types that define a copula

def Haspelmath2025a.Construction.Copular (t : Construction) : Prop

A clause is copular when its type is one of those that define a copula, the equational, the ascriptive and the locational types.

Equations

• t.Copular = (t = Haspelmath2025a.Construction.equational ∨ t.Ascriptive ∨ t.Locational)

@[instance_reducible]

instance Haspelmath2025a.Construction.instDecidablePredCopular : DecidablePred Copular

Equations

• x✝.instDecidablePredCopular = { decide := decide (x✝ = Haspelmath2025a.Construction.equational) || decide (x✝.Ascriptive ∨ x✝.Locational), reflects_decide := ⋯ }

theorem Haspelmath2025a.Construction.copular_iff (t : Construction) : t.Copular ↔ t = equational ∨ t = classificational ∨ t = attributional ∨ t = predlocative ∨ t = existential

theorem Haspelmath2025a.Construction.Possessional.not_copular {t : Construction} (h : t.Possessional) : ¬t.Copular

Copulas and existives

def Haspelmath2025a.IsCopula (S : Set Construction) : Prop

A copula links the two argument positions of an equational, ascriptive or locational clause, S being the set of constructions the form occurs in.

Equations

• Haspelmath2025a.IsCopula S = ∃ t ∈ S, t.Copular

def Haspelmath2025a.IsExistive (S : Set Construction) : Prop

An existive is a copula that occurs in no clauses but existential and predpossessive ones.

Equations

• Haspelmath2025a.IsExistive S = (Haspelmath2025a.IsCopula S ∧ S ⊆ {Haspelmath2025a.Construction.existential, Haspelmath2025a.Construction.predpossessive})

theorem Haspelmath2025a.IsCopula.mono {S T : Set Construction} (h : S ⊆ T) : IsCopula S → IsCopula T

theorem Haspelmath2025a.not_isCopula_of_possessional {S : Set Construction} (h : ∀ t ∈ S, t.Possessional) : ¬IsCopula S

A form that occurs in possessional clauses only, as 'have' and 'belong' do, is not a copula.

theorem Haspelmath2025a.isExistive_iff {S : Set Construction} : IsExistive S ↔ Construction.existential ∈ S ∧ S ⊆ {Construction.existential, Construction.predpossessive}

A form is an existive exactly when it occurs in existential clauses and in no clauses but existential and predpossessive ones, since of the two types only the existential defines a copula.

theorem Haspelmath2025a.IsExistive.hyparctic_notMem {S : Set Construction} (h : IsExistive S) : Construction.hyparctic ∉ S

theorem Haspelmath2025a.isExistive_pair : IsExistive {Construction.existential, Construction.predpossessive}

A form that occurs in existential and predpossessive clauses and in no others is an existive, and so a copula, also when it is a transitive verb 'have'.

Strategies

inductive Haspelmath2025a.Strategy : Type

The strategies the paper names, each a way of building one construction that is defined by form.

• transpossessive : Strategy

  A transitive verb 'have' with the possessor as its subject.

• compossessive : Strategy

  A comitative flag on the possessum.

• locpossessive : Strategy

  A locative flag on the possessor.

• obliquePossessor : Strategy

  An oblique flag on the possessor.

• independentPossessor : Strategy

  A special independent-possessor form.

• existiveCopula : Strategy

  An existive.

• transpossessiveExistential : Strategy

  The verb of a transpossessive clause.

• prolocative : Strategy

  A prolocative form, a short form whose meaning elsewhere is 'here' or 'there'.

• existentPostposing : Strategy

  The existent placed after the locative phrase.

@[instance_reducible]

instance Haspelmath2025a.instDecidableEqStrategy : DecidableEq Strategy

Equations

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

@[instance_reducible]

instance Haspelmath2025a.instReprStrategy : Repr Strategy

Equations

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

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

Equations

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

def Haspelmath2025a.Strategy.construction : Strategy → Construction

The construction a strategy builds.

Equations

• Haspelmath2025a.Strategy.transpossessive.construction = Haspelmath2025a.Construction.predpossessive
• Haspelmath2025a.Strategy.compossessive.construction = Haspelmath2025a.Construction.predpossessive
• Haspelmath2025a.Strategy.locpossessive.construction = Haspelmath2025a.Construction.predpossessive
• Haspelmath2025a.Strategy.obliquePossessor.construction = Haspelmath2025a.Construction.appertentive
• Haspelmath2025a.Strategy.independentPossessor.construction = Haspelmath2025a.Construction.appertentive
• Haspelmath2025a.Strategy.existiveCopula.construction = Haspelmath2025a.Construction.existential
• Haspelmath2025a.Strategy.transpossessiveExistential.construction = Haspelmath2025a.Construction.existential
• Haspelmath2025a.Strategy.prolocative.construction = Haspelmath2025a.Construction.existential
• Haspelmath2025a.Strategy.existentPostposing.construction = Haspelmath2025a.Construction.existential

The examples

def Haspelmath2025a.constructionNames : List (String × Construction)

The names of the constructions in the rows.

Equations

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

def Haspelmath2025a.strategyNames : List (String × Strategy)

The names of the strategies in the rows.

Equations

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

def Haspelmath2025a.constructions (row : Datum) : List Construction

The constructions of an example are the types the paper prints with it and the type its strategy builds.

Equations

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

theorem Haspelmath2025a.labels_parse (row : Datum) : row ∈ Examples.all → (∀ v ∈ row.features "construction", (List.lookup v constructionNames).isSome = true) ∧ ((row.feature? "strategy").isSome = true → (row.parse? "strategy" strategyNames).isSome = true)

theorem Haspelmath2025a.english_predicational : List.filter (fun (x : Datum) => decide (∃ t ∈ constructions x, t.Predicational)) [Examples.ex1, Examples.ex2, Examples.ex3, Examples.ex4, Examples.ex5, Examples.ex6, Examples.ex7] = [Examples.ex1, Examples.ex3, Examples.ex4, Examples.ex7]

Of the seven English examples that introduce the types, the classificational, attributional, predlocative and appertentive ones are predicational.

theorem Haspelmath2025a.duonominal_coding : Examples.ex8a.features "bold" = Examples.ex8b.features "bold" ∧ Examples.ex9a.features "bold" ≠ Examples.ex9b.features "bold" ∧ Examples.ex10a.features "bold" = [] ∧ Examples.ex10b.features "bold" ≠ []

Lezgian has one copula in its classificational and its equational clause, Welsh a different form of 'be' in each, and Egyptian Arabic a copula in the equational clause alone.

theorem Haspelmath2025a.copula_gloss_copular (row : Datum) : row ∈ Examples.all → (∃ g ∈ row.features "boldGloss", g = "COP" ∨ g = "LCOP") → ∀ t ∈ constructions row, t.Copular

Every example with a form glossed as a copula or a locative copula is of a type that defines a copula.

theorem Haspelmath2025a.mandinka_general_location : constructions Examples.ex57 = [Construction.predlocative, Construction.existential]

The Mandinka example is predlocative on one of its readings and existential on the other.

theorem Haspelmath2025a.seychelles_have : "have" ∈ Examples.ex51.features "boldGloss" ∧ constructions Examples.ex51 = [Construction.existential]

In the Seychelles Creole example a verb glossed 'have' occurs in an existential clause, so by isExistive_pair it is an existive if its other clauses are predpossessive.

theorem Haspelmath2025a.existive_gloss (row : Datum) : row ∈ Examples.all → "EXV" ∈ row.features "boldGloss" → constructions row = [Construction.existential] ∨ row = Examples.ex66 ∧ constructions row = [Construction.hyparctic]

The forms glossed as existives occur in existential clauses, except in the Hamar example, which is hyparctic.

theorem Haspelmath2025a.existive_gloss_hyparctic {S : Set Construction} (h : ∀ t ∈ constructions Examples.ex66, t ∈ S) : "EXV" ∈ Examples.ex66.features "boldGloss" ∧ ¬IsExistive S

The Hamar form glossed as an existive occurs in a hyparctic clause, so whatever other clauses it occurs in, it is not an existive as defined.

The fragments

theorem Haspelmath2025a.finnish_adessive : List.map (Subregular.LocalRewrite.derive Finnish.consonantGradation) (Finnish.Nominal.realize [Finnish.p, Finnish.e, Finnish.k, Finnish.k, Finnish.a] [⟨Finnish.Nominal.Slot.case, Finnish.Nominal.Exponent.case Finnish.Case.ade⟩]) = (Finnish.ofString? "pekalla").toList ∧ List.map (Subregular.LocalRewrite.derive Finnish.consonantGradation) (Finnish.Nominal.realize [Finnish.k, Finnish.a, Finnish.t, Finnish.t, Finnish.o] [⟨Finnish.Nominal.Slot.case, Finnish.Nominal.Exponent.case Finnish.Case.ade⟩]) = (Finnish.ofString? "katolla").toList ∧ Finnish.Case.ade.label.dirOf = some Spatial.Path.Direction.place

The possessor of the locpossessive example and the location of the existent-postposing one are the adessives of Pekka and katto in the Finnish fragment, after consonant gradation, and the adessive is a place case: the locative flag of the locpossessive strategy.

theorem Haspelmath2025a.turkish_affixal_copula : Turkish.Phonology.ofSegmented? "satıcı-y-dı-m" = some (Turkish.realize [Turkish.Phonology.s, Turkish.Phonology.a, Turkish.Phonology.t, Turkish.Phonology.ı, Turkish.Phonology.c, Turkish.Phonology.ı] [Turkish.Verb.Exponent.pastCopula.form, (Turkish.Verb.Exponent.person Turkish.Verb.PersonGroup.one (Agreement.Bundle.personNumber Person.first Number.singular)).form])

The word of the Turkish example is satıcı 'seller' with the past copula and the first person singular marker of the Turkish fragment. The affix the paper glosses as the copula is the initial consonant of the fragment's past copula.