Haspelmath (2025): Roots and root classes in comparative grammar

This file formalizes the definition of the root as a comparative concept in Haspelmath's chapter. Its definition (1), a contentful form (Form, a morph with its meaning class) that occurs in a free form with no other contentful form, is the root of Morphology.Comparative, read over a fragment's free-form inventory. The qualifying clause separates roots from contentful affixes (the Japanese causative -ase) and neoclassical combining forms (geo-), which are morphological cores under the formal base definition of Morphology/Root/Basic.lean but not roots; it admits bound roots (Sorbian žon-) and excludes free forms without a lexical meaning (hello, fn. 10). Roots are concrete forms (§4), so the four Arabic forms sharing the skeleton k-t-b are four roots (arabic_four_roots) and the German ablaut pair lauf ~ lief two. upos is (10), word classes as comparative concepts, and unmarkedFunction the prototypical combinations of (9).

§6 adopts the heterosemy view: hammer (noun) and hammer (verb) are two roots with one shape (hammer_two_roots), related by the sister schemas of (21) (nounVerb, one description over shared variables read through two subscriptings, ConstructionMorphology.Schema.InstantiatesAt), which the pair instantiates (hammer_sisters) and hammer/dance does not.

Implementation notes

• Form pairs a substrate Morph, the shape side, with an Option RootClass standing in for its meaning, which is all definition (1) and the lexical meaning of (11) need. Relatedness of meaning within a heterosemous root set is carried by the schema of (21), not by the forms.
• IsStemIn is the stem definition of fn. 6, with the Latin laud-ab- case; its affixes are those of Morphology.Comparative.IsAffixIn over the roots of definition (1).
• The chapter names the combining forms geo- and socio- in prose only; the English word geology, with its -logy, is this file's illustration of geo-.

References

• [Has23]
• [Has25c]
• [JA20]

Root classes (§5)

def Haspelmath2025b.upos : Morphology.Comparative.RootClass → UD.UPOS

Word classes are comparative concepts (10): a verb is an action-denoting root, a noun an object-denoting root, an adjective a property-denoting root.

Equations

• Haspelmath2025b.upos Morphology.Comparative.RootClass.action = UD.UPOS.VERB
• Haspelmath2025b.upos Morphology.Comparative.RootClass.object = UD.UPOS.NOUN
• Haspelmath2025b.upos Morphology.Comparative.RootClass.property = UD.UPOS.ADJ

inductive Haspelmath2025b.DiscourseFunction : Type

The discourse functions of (9).

• predication : DiscourseFunction
• reference : DiscourseFunction
• modification : DiscourseFunction

@[instance_reducible]

instance Haspelmath2025b.instDecidableEqDiscourseFunction : DecidableEq DiscourseFunction

Equations

• Haspelmath2025b.instDecidableEqDiscourseFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Haspelmath2025b.instFintypeDiscourseFunction : Fintype DiscourseFunction

Equations

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

def Haspelmath2025b.instReprDiscourseFunction.repr : DiscourseFunction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025b.instReprDiscourseFunction : Repr DiscourseFunction

Equations

• Haspelmath2025b.instReprDiscourseFunction = { reprPrec := Haspelmath2025b.instReprDiscourseFunction.repr }

def Haspelmath2025b.unmarkedFunction : Morphology.Comparative.RootClass → DiscourseFunction

unmarkedFunction c is the discourse function in which the class c needs no function indicator (9): no copula or verbalizer for action roots in predication, no nominalizer for object roots in reference, no relativizer or genitive for property roots in modification.

Equations

• Haspelmath2025b.unmarkedFunction Morphology.Comparative.RootClass.action = Haspelmath2025b.DiscourseFunction.predication
• Haspelmath2025b.unmarkedFunction Morphology.Comparative.RootClass.object = Haspelmath2025b.DiscourseFunction.reference
• Haspelmath2025b.unmarkedFunction Morphology.Comparative.RootClass.property = Haspelmath2025b.DiscourseFunction.modification

Definition (1)

structure Haspelmath2025b.Form : Type

A form (§2, §4) is a morph, the pairing of a shape with a meaning, recorded with its root class when it denotes an action, an object or a property and none otherwise.

• shape : Morphology.Morph

  The morph.

• meaning : Option Morphology.Comparative.RootClass

  The root class the form denotes, if any.

@[instance_reducible]

instance Haspelmath2025b.instDecidableEqForm : DecidableEq Form

Equations

• Haspelmath2025b.instDecidableEqForm = Haspelmath2025b.instDecidableEqForm.decEq

def Haspelmath2025b.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

• Haspelmath2025b.instDecidableEqForm.decEq { shape := a, meaning := a_1 } { shape := b, meaning := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Haspelmath2025b.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025b.instReprForm : Repr Form

Equations

• Haspelmath2025b.instReprForm = { reprPrec := Haspelmath2025b.instReprForm.repr }

def Haspelmath2025b.shapes (w : List Form) : List Morphology.Morph

The shapes of the forms of a word, for the formal definitions of Morphology/Root/Basic.lean.

Equations

• Haspelmath2025b.shapes w = List.map Haspelmath2025b.Form.shape w

def Haspelmath2025b.IsStemIn (words freeForms : List (List Form)) (s : List Form) : Prop

Fn. 6: a stem is a contiguous string of at least one root and possibly some affixes that can be combined with an affix.

Equations

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

@[instance_reducible]

instance Haspelmath2025b.instDecidableIsStemIn (words freeForms : List (List Form)) (s : List Form) : Decidable (IsStemIn words freeForms s)

Equations

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

Contentful affixes and combining forms (§2)

def Haspelmath2025b.yom : Form

The Japanese action root yom 'read'.

Equations

• Haspelmath2025b.yom = { shape := Morphology.Morph.root "yom", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.ase : Form

The Japanese causative suffix -ase, which denotes an action.

Equations

• Haspelmath2025b.ase = { shape := Morphology.Morph.suff "ase", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.u : Form

The Japanese nonpast suffix -u.

Equations

• Haspelmath2025b.u = { shape := Morphology.Morph.suff "u", meaning := none }

def Haspelmath2025b.ru : Form

The Japanese nonpast suffix -ru.

Equations

• Haspelmath2025b.ru = { shape := Morphology.Morph.suff "ru", meaning := none }

def Haspelmath2025b.japanese : List (List Form)

The Japanese free forms yom-u 'read' and yom-ase-ru 'make read'.

Equations

• Haspelmath2025b.japanese = [[Haspelmath2025b.yom, Haspelmath2025b.u], [Haspelmath2025b.yom, Haspelmath2025b.ase, Haspelmath2025b.ru]]

theorem Haspelmath2025b.ase_not_root : Morphology.Comparative.IsContentful Form.meaning ase ∧ ¬Morphology.Comparative.IsRootIn japanese Form.meaning ase ∧ Morphology.Comparative.IsRootIn japanese Form.meaning yom

The causative -ase is contentful but never occurs without another contentful form, so it is not a root, while yom is (§2).

def Haspelmath2025b.geo : Form

The neoclassical combining form geo-.

Equations

• Haspelmath2025b.geo = { shape := Morphology.Morph.root "geo", meaning := some Morphology.Comparative.RootClass.object }

def Haspelmath2025b.logy : Form

The neoclassical combining form -logy.

Equations

• Haspelmath2025b.logy = { shape := Morphology.Morph.root "logy", meaning := some Morphology.Comparative.RootClass.object }

def Haspelmath2025b.hello : Form

The English interjection hello (fn. 10).

Equations

• Haspelmath2025b.hello = { shape := Morphology.Morph.free "hello", meaning := none }

def Haspelmath2025b.hammerN : Form

The English object root hammer (12a).

Equations

• Haspelmath2025b.hammerN = { shape := Morphology.Morph.root "hammer", meaning := some Morphology.Comparative.RootClass.object }

def Haspelmath2025b.hammerV : Form

The English action root hammer (12b).

Equations

• Haspelmath2025b.hammerV = { shape := Morphology.Morph.root "hammer", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.s : Form

The English plural suffix.

Equations

• Haspelmath2025b.s = { shape := Morphology.Morph.suff "s", meaning := none }

def Haspelmath2025b.ed : Form

The English past suffix.

Equations

• Haspelmath2025b.ed = { shape := Morphology.Morph.suff "ed", meaning := none }

def Haspelmath2025b.english : List (List Form)

The English free forms: geology (an illustration), hello, and the hammer forms.

Equations

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

theorem Haspelmath2025b.geo_not_root : ¬Morphology.Comparative.IsRootIn english Form.meaning geo ∧ geo.shape.IsCoreIn (List.map shapes english) (List.map shapes english)

geo- is contentful but only occurs with another contentful form, so it is not a root, although it is a morphological core under the formal base definition (§2).

theorem Haspelmath2025b.hello_not_root : ¬Morphology.Comparative.IsRootIn english Form.meaning hello ∧ hello.shape.IsCoreIn (List.map shapes english) (List.map shapes english)

hello is a free form without a lexical meaning, hence not a root, although it is a morphological core (fn. 10).

def Haspelmath2025b.žon : Form

The Sorbian object root žon- 'wife'.

Equations

• Haspelmath2025b.žon = { shape := Morphology.Morph.root "žon", meaning := some Morphology.Comparative.RootClass.object }

def Haspelmath2025b.a : Form

The Sorbian nominative suffix.

Equations

• Haspelmath2025b.a = { shape := Morphology.Morph.suff "a", meaning := none }

def Haspelmath2025b.y : Form

The Sorbian genitive suffix.

Equations

• Haspelmath2025b.y = { shape := Morphology.Morph.suff "y", meaning := none }

def Haspelmath2025b.uAcc : Form

The Sorbian accusative suffix.

Equations

• Haspelmath2025b.uAcc = { shape := Morphology.Morph.suff "u", meaning := none }

def Haspelmath2025b.sorbian : List (List Form)

The Sorbian free forms žon-a, žon-y, žon-u (§3).

Equations

• Haspelmath2025b.sorbian = [[Haspelmath2025b.žon, Haspelmath2025b.a], [Haspelmath2025b.žon, Haspelmath2025b.y], [Haspelmath2025b.žon, Haspelmath2025b.uAcc]]

theorem Haspelmath2025b.žon_bound_root : Morphology.Comparative.IsRootIn sorbian Form.meaning žon ∧ Morphology.Comparative.IsBoundIn sorbian žon

žon- always occurs with an inflectional affix, yet it is a root (§3, fn. 2).

Roots as concrete forms (§4)

def Haspelmath2025b.lauf : Form

The German action root lauf 'run'.

Equations

• Haspelmath2025b.lauf = { shape := Morphology.Morph.root "lauf", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.lief : Form

The German ablaut root lief 'ran'.

Equations

• Haspelmath2025b.lief = { shape := Morphology.Morph.root "lief", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.e : Form

The German first-singular suffix.

Equations

• Haspelmath2025b.e = { shape := Morphology.Morph.suff "e", meaning := none }

def Haspelmath2025b.en : Form

The German plural and participial suffix.

Equations

• Haspelmath2025b.en = { shape := Morphology.Morph.suff "en", meaning := none }

def Haspelmath2025b.ge : Form

The German participial prefix.

Equations

• Haspelmath2025b.ge = { shape := Morphology.Morph.pref "ge", meaning := none }

def Haspelmath2025b.german : List (List Form)

The German verb forms of (5) are lauf-e, lauf-en, lauf, ge-lauf-en, lief.

Equations

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

theorem Haspelmath2025b.lauf_lief_roots : Morphology.Comparative.IsRootIn german Form.meaning lauf ∧ Morphology.Comparative.IsRootIn german Form.meaning lief ∧ lauf ≠ lief

With no replacive morphs, lauf and lief are two roots (§4).

def Haspelmath2025b.skeleton (f : Form) : Morphology.ConsonantalRoot Char

The consonantal skeleton of a form is its shape with the vowels removed.

Equations

• Haspelmath2025b.skeleton f = { segments := List.filter (fun (x : Char) => decide (x ∉ ['a', 'i', 'u'])) f.shape.form.toList }

def Haspelmath2025b.katab : Form

The Arabic action root katab 'wrote'.

Equations

• Haspelmath2025b.katab = { shape := Morphology.Morph.root "katab", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.ktub : Form

The Arabic action root ktub 'write'.

Equations

• Haspelmath2025b.ktub = { shape := Morphology.Morph.root "ktub", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.kaatib : Form

The Arabic object root kaatib 'writer'.

Equations

• Haspelmath2025b.kaatib = { shape := Morphology.Morph.root "kaatib", meaning := some Morphology.Comparative.RootClass.object }

def Haspelmath2025b.kitaab : Form

The Arabic object root kitaab 'book'.

Equations

• Haspelmath2025b.kitaab = { shape := Morphology.Morph.root "kitaab", meaning := some Morphology.Comparative.RootClass.object }

def Haspelmath2025b.naa : Form

The Arabic first-plural suffix.

Equations

• Haspelmath2025b.naa = { shape := Morphology.Morph.suff "naa", meaning := none }

def Haspelmath2025b.na : Form

The Arabic first-plural prefix.

Equations

• Haspelmath2025b.na = { shape := Morphology.Morph.pref "na", meaning := none }

def Haspelmath2025b.arabic : List (List Form)

The Arabic forms of (6) are katab-naa, na-ktub-u, kaatib, kitaab.

Equations

• Haspelmath2025b.arabic = [[Haspelmath2025b.katab, Haspelmath2025b.naa], [Haspelmath2025b.na, Haspelmath2025b.ktub, Haspelmath2025b.u], [Haspelmath2025b.kaatib], [Haspelmath2025b.kitaab]]

theorem Haspelmath2025b.arabic_four_roots : (∀ f ∈ [katab, ktub, kaatib, kitaab], Morphology.Comparative.IsRootIn arabic Form.meaning f ∧ skeleton f = { segments := ['k', 't', 'b'] }) ∧ [katab, ktub, kaatib, kitaab].Nodup

The forms of (6) contain four distinct roots sharing the skeleton k-t-b, which is not itself a root (§4).

def Haspelmath2025b.laud : Form

The Latin action root laud 'praise'.

Equations

• Haspelmath2025b.laud = { shape := Morphology.Morph.root "laud", meaning := some Morphology.Comparative.RootClass.action }

def Haspelmath2025b.ab : Form

The Latin imperfect suffix.

Equations

• Haspelmath2025b.ab = { shape := Morphology.Morph.suff "ab", meaning := none }

def Haspelmath2025b.am : Form

The Latin first-singular imperfect suffix.

Equations

• Haspelmath2025b.am = { shape := Morphology.Morph.suff "am", meaning := none }

def Haspelmath2025b.o : Form

The Latin first-singular present suffix.

Equations

• Haspelmath2025b.o = { shape := Morphology.Morph.suff "o", meaning := none }

def Haspelmath2025b.latin : List (List Form)

The Latin forms laud-o 'I praise' and laud-ab-am 'I was praising'.

Equations

• Haspelmath2025b.latin = [[Haspelmath2025b.laud, Haspelmath2025b.o], [Haspelmath2025b.laud, Haspelmath2025b.ab, Haspelmath2025b.am]]

theorem Haspelmath2025b.laudab_stem : IsStemIn latin latin [laud, ab] ∧ IsStemIn latin latin [laud]

Fn. 6: laud-ab- is an imperfect stem, a root with a tense suffix that combines with a person suffix.

Heterosemy (§6)

theorem Haspelmath2025b.hammer_two_roots : Morphology.Comparative.IsRootIn english Form.meaning hammerN ∧ Morphology.Comparative.IsRootIn english Form.meaning hammerV ∧ hammerN ≠ hammerV ∧ hammerN.shape = hammerV.shape

hammer (noun) and hammer (verb) are two roots with one shape (§6).

inductive Haspelmath2025b.Tier : Type

The tiers of the schemas of (18)–(21).

• semantics : Tier
• morphosyntax : Tier
• phonology : Tier

@[instance_reducible]

instance Haspelmath2025b.instDecidableEqTier : DecidableEq Tier

Equations

• Haspelmath2025b.instDecidableEqTier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Haspelmath2025b.instFintypeTier : Fintype Tier

Equations

• Haspelmath2025b.instFintypeTier = { elems := { val := ↑Haspelmath2025b.Tier.enumList, nodup := Haspelmath2025b.Tier.enumList_nodup }, complete := Haspelmath2025b.instFintypeTier._proof_1 }

def Haspelmath2025b.instReprTier.repr : Tier → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025b.instReprTier : Repr Tier

Equations

• Haspelmath2025b.instReprTier = { reprPrec := Haspelmath2025b.instReprTier.repr }

inductive Haspelmath2025b.Value : Type

A tier value is a meaning, a word class, or a shape.

• meaning (m : String) : Value
• category (c : Morphology.Comparative.RootClass) : Value
• shape (s : String) : Value

def Haspelmath2025b.instDecidableEqValue.decEq (x✝ x✝¹ : Value) : Decidable (x✝ = x✝¹)

Equations

• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.meaning a) (Haspelmath2025b.Value.meaning b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.meaning m) (Haspelmath2025b.Value.category c) = isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.meaning m) (Haspelmath2025b.Value.shape s) = isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.category c) (Haspelmath2025b.Value.meaning m) = isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.category a) (Haspelmath2025b.Value.category b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.category c) (Haspelmath2025b.Value.shape s) = isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.shape s) (Haspelmath2025b.Value.meaning m) = isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.shape s) (Haspelmath2025b.Value.category c) = isFalse ⋯
• Haspelmath2025b.instDecidableEqValue.decEq (Haspelmath2025b.Value.shape a) (Haspelmath2025b.Value.shape b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Haspelmath2025b.instDecidableEqValue : DecidableEq Value

Equations

• Haspelmath2025b.instDecidableEqValue = Haspelmath2025b.instDecidableEqValue.decEq

@[instance_reducible]

instance Haspelmath2025b.instReprValue : Repr Value

Equations

• Haspelmath2025b.instReprValue = { reprPrec := Haspelmath2025b.instReprValue.repr }

def Haspelmath2025b.instReprValue.repr : Value → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025b.instPartialOrderValue : PartialOrder Value

Tier values are discrete: a constant is dominated only by itself.

Equations

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

@[instance_reducible]

instance Haspelmath2025b.instDecidableLEValue : DecidableLE Value

Equations

• Haspelmath2025b.instDecidableLEValue a b = Haspelmath2025b.instDecidableEqValue a b

@[reducible, inline]

abbrev Haspelmath2025b.Slot : Type

A tier description is a value, or ⊥ for an open variable.

Equations

• Haspelmath2025b.Slot = WithBot Haspelmath2025b.Value

inductive Haspelmath2025b.RootVar : Type

The variables of the sister schemas (21) are the meaning and the category of each root, and the shape Y they share (index 2).

• nounMeaning : RootVar
• nounCategory : RootVar
• verbMeaning : RootVar
• verbCategory : RootVar
• shape : RootVar

@[instance_reducible]

instance Haspelmath2025b.instDecidableEqRootVar : DecidableEq RootVar

Equations

• Haspelmath2025b.instDecidableEqRootVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Haspelmath2025b.nounVerb : ConstructionMorphology.Schema RootVar Slot

The sister schemas X (noun) and X (verb) of (21) form one description over their variables, with the categories pinned and the meanings and the shared shape open.

Equations

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

def Haspelmath2025b.nounSub : Tier → RootVar

The subscripting of the tiers of the noun schema by the variables of (21).

Equations

• Haspelmath2025b.nounSub Haspelmath2025b.Tier.semantics = Haspelmath2025b.RootVar.nounMeaning
• Haspelmath2025b.nounSub Haspelmath2025b.Tier.morphosyntax = Haspelmath2025b.RootVar.nounCategory
• Haspelmath2025b.nounSub Haspelmath2025b.Tier.phonology = Haspelmath2025b.RootVar.shape

def Haspelmath2025b.verbSub : Tier → RootVar

The subscripting of the tiers of the verb schema by the variables of (21).

Equations

• Haspelmath2025b.verbSub Haspelmath2025b.Tier.semantics = Haspelmath2025b.RootVar.verbMeaning
• Haspelmath2025b.verbSub Haspelmath2025b.Tier.morphosyntax = Haspelmath2025b.RootVar.verbCategory
• Haspelmath2025b.verbSub Haspelmath2025b.Tier.phonology = Haspelmath2025b.RootVar.shape

def Haspelmath2025b.nounSchema : ConstructionMorphology.Schema Tier Slot

Schema (21a), X (noun), pairs an object meaning related to X with a noun and the open shape Y.

Equations

• Haspelmath2025b.nounSchema = Haspelmath2025b.nounVerb.comap Haspelmath2025b.nounSub

def Haspelmath2025b.verbSchema : ConstructionMorphology.Schema Tier Slot

Schema (21b), X (verb), pairs doing in relation to X with a verb and the open shape Y.

Equations

• Haspelmath2025b.verbSchema = Haspelmath2025b.nounVerb.comap Haspelmath2025b.verbSub

def Haspelmath2025b.hammerNoun : Tier → Slot

hammerNoun is the noun hammer of (20a).

Equations

• Haspelmath2025b.hammerNoun Haspelmath2025b.Tier.semantics = ↑(Haspelmath2025b.Value.meaning "HAMMER")
• Haspelmath2025b.hammerNoun Haspelmath2025b.Tier.morphosyntax = ↑(Haspelmath2025b.Value.category Morphology.Comparative.RootClass.object)
• Haspelmath2025b.hammerNoun Haspelmath2025b.Tier.phonology = ↑(Haspelmath2025b.Value.shape "hæmər")

def Haspelmath2025b.hammerVerb : Tier → Slot

hammerVerb is the verb hammer of (20b).

Equations

• Haspelmath2025b.hammerVerb Haspelmath2025b.Tier.semantics = ↑(Haspelmath2025b.Value.meaning "HIT (WITH SOMETHING LIKE HAMMER)")
• Haspelmath2025b.hammerVerb Haspelmath2025b.Tier.morphosyntax = ↑(Haspelmath2025b.Value.category Morphology.Comparative.RootClass.action)
• Haspelmath2025b.hammerVerb Haspelmath2025b.Tier.phonology = ↑(Haspelmath2025b.Value.shape "hæmər")

def Haspelmath2025b.danceVerb : Tier → Slot

dance (verb), whose shape differs from hammer's.

Equations

• Haspelmath2025b.danceVerb Haspelmath2025b.Tier.semantics = ↑(Haspelmath2025b.Value.meaning "DANCE")
• Haspelmath2025b.danceVerb Haspelmath2025b.Tier.morphosyntax = ↑(Haspelmath2025b.Value.category Morphology.Comparative.RootClass.action)
• Haspelmath2025b.danceVerb Haspelmath2025b.Tier.phonology = ↑(Haspelmath2025b.Value.shape "dæns")

def Haspelmath2025b.hammerRoots : RootVar → Slot

The variables of (21) filled by the two hammer roots.

Equations

• Haspelmath2025b.hammerRoots Haspelmath2025b.RootVar.nounMeaning = Haspelmath2025b.hammerNoun Haspelmath2025b.Tier.semantics
• Haspelmath2025b.hammerRoots Haspelmath2025b.RootVar.nounCategory = Haspelmath2025b.hammerNoun Haspelmath2025b.Tier.morphosyntax
• Haspelmath2025b.hammerRoots Haspelmath2025b.RootVar.verbMeaning = Haspelmath2025b.hammerVerb Haspelmath2025b.Tier.semantics
• Haspelmath2025b.hammerRoots Haspelmath2025b.RootVar.verbCategory = Haspelmath2025b.hammerVerb Haspelmath2025b.Tier.morphosyntax
• Haspelmath2025b.hammerRoots Haspelmath2025b.RootVar.shape = Haspelmath2025b.hammerNoun Haspelmath2025b.Tier.phonology

theorem Haspelmath2025b.hammer_sisters : nounVerb.InstantiatesAt (Sum.elim nounSub verbSub) (Sum.elim hammerNoun hammerVerb)

The two hammer roots of (20) instantiate the sister schemas of (21) as a pair, their shapes filled alike; neither is derived from the other or from an abstract root.

theorem Haspelmath2025b.hammer_dance_not_sisters : ¬nounVerb.InstantiatesAt (Sum.elim nounSub verbSub) (Sum.elim hammerNoun danceVerb)

hammer (noun) and dance (verb) instantiate the schemas but not as a pair: the linked shapes differ.