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

This file formalizes the definition of the root as a comparative concept in [haspelmath-2025-root]. IsRootIn is definition (1): a contentful form (Form, a morph with its meaning class) that occurs in a free form with no other contentful form, relative to 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. RootClass.upos is (10), word classes as comparative concepts, and RootClass.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.

References

• [haspelmath-2025-root]
• [jackendoff-audring-2020]

Root classes (§5)

inductive Haspelmath2025Root.RootClass : Type

The three root classes (§5): roots denoting actions, objects and properties, the lexical meanings of (11).

• action : RootClass
• object : RootClass
• property : RootClass

@[instance_reducible]

instance Haspelmath2025Root.instDecidableEqRootClass : DecidableEq RootClass

Equations

• Haspelmath2025Root.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Haspelmath2025Root.instFintypeRootClass : Fintype RootClass

Equations

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

def Haspelmath2025Root.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instReprRootClass : Repr RootClass

Equations

• Haspelmath2025Root.instReprRootClass = { reprPrec := Haspelmath2025Root.instReprRootClass.repr }

def Haspelmath2025Root.RootClass.upos : RootClass → UD.UPOS

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

Equations

• Haspelmath2025Root.RootClass.action.upos = UD.UPOS.VERB
• Haspelmath2025Root.RootClass.object.upos = UD.UPOS.NOUN
• Haspelmath2025Root.RootClass.property.upos = UD.UPOS.ADJ

inductive Haspelmath2025Root.DiscourseFunction : Type

The discourse functions of (9).

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

@[instance_reducible]

instance Haspelmath2025Root.instDecidableEqDiscourseFunction : DecidableEq DiscourseFunction

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instFintypeDiscourseFunction : Fintype DiscourseFunction

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instReprDiscourseFunction : Repr DiscourseFunction

Equations

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

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

Equations

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

def Haspelmath2025Root.RootClass.unmarkedFunction : RootClass → DiscourseFunction

(9): the discourse function in which a root class needs no function indicator: 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

• Haspelmath2025Root.RootClass.action.unmarkedFunction = Haspelmath2025Root.DiscourseFunction.predication
• Haspelmath2025Root.RootClass.object.unmarkedFunction = Haspelmath2025Root.DiscourseFunction.reference
• Haspelmath2025Root.RootClass.property.unmarkedFunction = Haspelmath2025Root.DiscourseFunction.modification

Definition (1)

structure Haspelmath2025Root.Form : Type

A form (§2, §4): 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 RootClass

  The root class the form denotes, if any.

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

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instDecidableEqForm : DecidableEq Form

Equations

• Haspelmath2025Root.instDecidableEqForm = Haspelmath2025Root.instDecidableEqForm.decEq

@[instance_reducible]

instance Haspelmath2025Root.instReprForm : Repr Form

Equations

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

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

Equations

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

def Haspelmath2025Root.Form.IsContentful (f : Form) : Prop

A form is contentful when it denotes an action, an object or a property (§2).

Equations

• f.IsContentful = (f.meaning ≠ none)

@[instance_reducible]

instance Haspelmath2025Root.instDecidableIsContentful (f : Form) : Decidable f.IsContentful

Equations

• Haspelmath2025Root.instDecidableIsContentful f = Haspelmath2025Root.instDecidableIsContentful._aux_1 f

def Haspelmath2025Root.IsRootIn (freeForms : List (List Form)) (f : Form) : Prop

Definition (1): a root is a contentful form that can occur as part of a free form without another contentful form.

Equations

• Haspelmath2025Root.IsRootIn freeForms f = (f.IsContentful ∧ ∃ w ∈ freeForms, f ∈ w ∧ ∀ g ∈ w, g ≠ f → ¬g.IsContentful)

@[instance_reducible]

instance Haspelmath2025Root.instDecidableIsRootIn (freeForms : List (List Form)) (f : Form) : Decidable (IsRootIn freeForms f)

Equations

• Haspelmath2025Root.instDecidableIsRootIn freeForms f = Haspelmath2025Root.instDecidableIsRootIn._aux_1 freeForms f

def Haspelmath2025Root.IsBoundIn (freeForms : List (List Form)) (f : Form) : Prop

A form is bound when it is not itself a free form (fn. 2).

Equations

• Haspelmath2025Root.IsBoundIn freeForms f = ([f] ∉ freeForms)

@[instance_reducible]

instance Haspelmath2025Root.instDecidableIsBoundIn (freeForms : List (List Form)) (f : Form) : Decidable (IsBoundIn freeForms f)

Equations

• Haspelmath2025Root.instDecidableIsBoundIn freeForms f = Haspelmath2025Root.instDecidableIsBoundIn._aux_1 freeForms f

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

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

def Haspelmath2025Root.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 Haspelmath2025Root.instDecidableIsStemIn (words freeForms : List (List Form)) (s : List Form) : Decidable (IsStemIn words freeForms s)

Equations

• Haspelmath2025Root.instDecidableIsStemIn words freeForms s = Haspelmath2025Root.instDecidableIsStemIn._aux_1 words freeForms s

Contentful affixes and combining forms (§2)

def Haspelmath2025Root.yom : Form

The Japanese action root yom 'read'.

Equations

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

def Haspelmath2025Root.ase : Form

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

Equations

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

def Haspelmath2025Root.u : Form

The Japanese nonpast suffix -u.

Equations

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

def Haspelmath2025Root.ru : Form

The Japanese nonpast suffix -ru.

Equations

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

def Haspelmath2025Root.japanese : List (List Form)

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

Equations

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

theorem Haspelmath2025Root.ase_not_root : ase.IsContentful ∧ ¬IsRootIn japanese ase ∧ IsRootIn japanese yom

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

def Haspelmath2025Root.geo : Form

The neoclassical combining form geo-.

Equations

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

def Haspelmath2025Root.logy : Form

The neoclassical combining form -logy.

Equations

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

def Haspelmath2025Root.hello : Form

The English interjection hello (fn. 10).

Equations

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

def Haspelmath2025Root.hammerN : Form

The English object root hammer (12a).

Equations

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

def Haspelmath2025Root.hammerV : Form

The English action root hammer (12b).

Equations

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

def Haspelmath2025Root.s : Form

The English plural suffix.

Equations

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

def Haspelmath2025Root.ed : Form

The English past suffix.

Equations

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

def Haspelmath2025Root.english : List (List Form)

English free forms: geology, hello, and the hammer forms.

Equations

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

theorem Haspelmath2025Root.geo_not_root : ¬IsRootIn english geo ∧ geo.shape.IsCoreIn (List.map shapes english) (List.map shapes english)

§2: 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.

theorem Haspelmath2025Root.hello_not_root : ¬IsRootIn english hello ∧ hello.shape.IsCoreIn (List.map shapes english) (List.map shapes english)

Fn. 10: hello is a free form without a lexical meaning, hence not a root, although it is a morphological core.

def Haspelmath2025Root.žon : Form

The Sorbian object root žon- 'wife'.

Equations

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

def Haspelmath2025Root.a : Form

The Sorbian nominative suffix.

Equations

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

def Haspelmath2025Root.y : Form

The Sorbian genitive suffix.

Equations

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

def Haspelmath2025Root.uAcc : Form

The Sorbian accusative suffix.

Equations

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

def Haspelmath2025Root.sorbian : List (List Form)

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

Equations

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

theorem Haspelmath2025Root.žon_bound_root : IsRootIn sorbian žon ∧ IsBoundIn sorbian žon

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

Roots as concrete forms (§4)

def Haspelmath2025Root.lauf : Form

The German action root lauf 'run'.

Equations

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

def Haspelmath2025Root.lief : Form

The German ablaut root lief 'ran'.

Equations

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

def Haspelmath2025Root.e : Form

The German first-singular suffix.

Equations

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

def Haspelmath2025Root.en : Form

The German plural and participial suffix.

Equations

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

def Haspelmath2025Root.ge : Form

The German participial prefix.

Equations

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

def Haspelmath2025Root.german : List (List Form)

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

Equations

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

theorem Haspelmath2025Root.lauf_lief_roots : IsRootIn german lauf ∧ IsRootIn german lief ∧ lauf ≠ lief

§4: with no replacive morphs, lauf and lief are two roots.

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

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

Equations

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

def Haspelmath2025Root.katab : Form

The Arabic action root katab 'wrote'.

Equations

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

def Haspelmath2025Root.ktub : Form

The Arabic action root ktub 'write'.

Equations

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

def Haspelmath2025Root.kaatib : Form

The Arabic object root kaatib 'writer'.

Equations

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

def Haspelmath2025Root.kitaab : Form

The Arabic object root kitaab 'book'.

Equations

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

def Haspelmath2025Root.naa : Form

The Arabic first-plural suffix.

Equations

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

def Haspelmath2025Root.na : Form

The Arabic first-plural prefix.

Equations

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

def Haspelmath2025Root.arabic : List (List Form)

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

Equations

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

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

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

def Haspelmath2025Root.laud : Form

The Latin action root laud 'praise'.

Equations

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

def Haspelmath2025Root.ab : Form

The Latin imperfect suffix.

Equations

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

def Haspelmath2025Root.am : Form

The Latin first-singular imperfect suffix.

Equations

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

def Haspelmath2025Root.o : Form

The Latin first-singular present suffix.

Equations

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

def Haspelmath2025Root.latin : List (List Form)

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

Equations

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

theorem Haspelmath2025Root.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 Haspelmath2025Root.hammer_two_roots : IsRootIn english hammerN ∧ IsRootIn english hammerV ∧ hammerN ≠ hammerV ∧ hammerN.shape = hammerV.shape

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

inductive Haspelmath2025Root.Tier : Type

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

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

@[instance_reducible]

instance Haspelmath2025Root.instDecidableEqTier : DecidableEq Tier

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instFintypeTier : Fintype Tier

Equations

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

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

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instReprTier : Repr Tier

Equations

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

inductive Haspelmath2025Root.Value : Type

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

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

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

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.instDecidableEqValue : DecidableEq Value

Equations

• Haspelmath2025Root.instDecidableEqValue = Haspelmath2025Root.instDecidableEqValue.decEq

@[instance_reducible]

instance Haspelmath2025Root.instReprValue : Repr Value

Equations

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

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

Equations

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

@[instance_reducible]

instance Haspelmath2025Root.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 Haspelmath2025Root.instDecidableLEValue : DecidableLE Value

Equations

• Haspelmath2025Root.instDecidableLEValue a b = Haspelmath2025Root.instDecidableEqValue a b

@[reducible, inline]

abbrev Haspelmath2025Root.Slot : Type

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

Equations

• Haspelmath2025Root.Slot = WithBot Haspelmath2025Root.Value

inductive Haspelmath2025Root.RootVar : Type

The variables of the sister schemas (21): 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 Haspelmath2025Root.instDecidableEqRootVar : DecidableEq RootVar

Equations

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

def Haspelmath2025Root.nounVerb : ConstructionMorphology.Schema RootVar Slot

(21): the sister schemas X (noun) and X (verb) as one description over their variables, the categories pinned, the meanings and the shared shape open.

Equations

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

def Haspelmath2025Root.nounSub : Tier → RootVar

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

Equations

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

def Haspelmath2025Root.verbSub : Tier → RootVar

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

Equations

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

def Haspelmath2025Root.nounSchema : ConstructionMorphology.Schema Tier Slot

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

Equations

• Haspelmath2025Root.nounSchema = Haspelmath2025Root.nounVerb.comap Haspelmath2025Root.nounSub

def Haspelmath2025Root.verbSchema : ConstructionMorphology.Schema Tier Slot

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

Equations

• Haspelmath2025Root.verbSchema = Haspelmath2025Root.nounVerb.comap Haspelmath2025Root.verbSub

def Haspelmath2025Root.hammerNoun : Tier → Slot

(20a): hammer (noun).

Equations

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

def Haspelmath2025Root.hammerVerb : Tier → Slot

(20b): hammer (verb).

Equations

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

def Haspelmath2025Root.danceVerb : Tier → Slot

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

Equations

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

def Haspelmath2025Root.hammerRoots : RootVar → Slot

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

Equations

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

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

(20): the two hammer roots 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 Haspelmath2025Root.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.