Words and their parts as comparative concepts

Haspelmath defines the parts of words for comparing languages by their distribution over a language's free forms, the forms that can be used on their own. A bound morph is not a free form. A root is a contentful morph that can occur in a free form without another contentful morph. An affix is a bound morph that is not a root, must occur on a root, and cannot occur on roots of different classes, where a morph occurs on a root when it is next to the root or next to an affix that occurs on it. A clitic is a bound morph that is neither a root nor an affix, and a word is a free morph, a clitic, or a root with its affixes.

Main definitions

• Comparative.RootClass: the classes of roots denoting actions, objects and properties.
• Comparative.IsBoundIn, Comparative.IsContentful, Comparative.IsRootIn: bound morphs, contentful morphs, and roots of an inventory.
• Comparative.OccursOn: occurrence on a root through candidate affixes.
• Comparative.AffixStep, Comparative.IsAffixIn: one step of the definition of an affix, and its greatest solution.
• Comparative.IsCliticIn, Comparative.IsRequiredAffixIn, Comparative.IsWordIn: clitics, required affixes and words.

Main results

• Comparative.isAffixIn_iff_sublists: affixhood is decided over the bound morphs of the inventory.
• Comparative.AffixStep.mono: when the roots of every free form are adjacent, the step is monotone.
• Comparative.isGreatest_setOf_isAffixIn: the affixes are then the greatest fixed point of the step.

Implementation notes

An inventory is a list of free forms, each a list of morphs, with the root class each morph denotes, if any. The definition of an affix refers to affixes, and its fixed points need not be unique; the affixes are its greatest solution. It is parametric in the roots, which are the contentful morphs in the 2021 paper and those of IsRootIn in the 2023 one. A required affix may be replaced by any other affix on its root, since replacement within one slot would need paradigm structure. Compounds are not covered.

References

• [Has21a]
• [Has23]

inductive Morphology.Comparative.RootClass : Type

The class of a root says whether it denotes an action, an object or a property.

• action : RootClass

  The root denotes an action, as a verb root does.

• object : RootClass

  The root denotes an object, as a noun root does.

• property : RootClass

  The root denotes a property, as an adjective root does.

@[instance_reducible]

instance Morphology.Comparative.instDecidableEqRootClass : DecidableEq RootClass

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instFintypeRootClass : Fintype RootClass

Equations

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

def Morphology.Comparative.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instReprRootClass : Repr RootClass

Equations

• Morphology.Comparative.instReprRootClass = { reprPrec := Morphology.Comparative.instReprRootClass.repr }

Free forms and roots

def Morphology.Comparative.IsBoundIn {M : Type u_1} (F : List (List M)) (x : M) : Prop

A morph is bound when it is not a free form, one that can be used on its own.

Equations

• Morphology.Comparative.IsBoundIn F x = ([x] ∉ F)

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsBoundInOfDecidableEq {M : Type u_1} (F : List (List M)) [DecidableEq M] (x : M) : Decidable (IsBoundIn F x)

Equations

• Morphology.Comparative.instDecidableIsBoundInOfDecidableEq F x = { decide := !decide ([x] ∈ F), reflects_decide := ⋯ }

def Morphology.Comparative.IsContentful {M : Type u_1} (rootClass : M → Option RootClass) (x : M) : Prop

A morph is contentful when it denotes an action, an object or a property.

Equations

• Morphology.Comparative.IsContentful rootClass x = (rootClass x ≠ none)

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsContentful {M : Type u_1} (rootClass : M → Option RootClass) (x : M) : Decidable (IsContentful rootClass x)

Equations

• Morphology.Comparative.instDecidableIsContentful rootClass x = { decide := !decide (rootClass x = none), reflects_decide := ⋯ }

def Morphology.Comparative.IsRootIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (x : M) : Prop

A root is a contentful morph that occurs in a free form with no other contentful morph.

Equations

• Morphology.Comparative.IsRootIn F rootClass x = (Morphology.Comparative.IsContentful rootClass x ∧ ∃ w ∈ F, x ∈ w ∧ ∀ y ∈ w, y ≠ x → ¬Morphology.Comparative.IsContentful rootClass y)

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsRootInOfDecidableEq {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) [DecidableEq M] (x : M) : Decidable (IsRootIn F rootClass x)

Equations

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

theorem Morphology.Comparative.IsRootIn.isContentful {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) {x : M} (h : IsRootIn F rootClass x) : IsContentful rootClass x

Occurrence on a root

def Morphology.Comparative.Reaches {M : Type u_1} (A : Set M) : List M → M → Prop

Read outward from a position, the morphs v reach y through the morphs of A when y is next, or the next morph is in A and the rest reach y.

Equations

• Morphology.Comparative.Reaches A [] x✝ = False
• Morphology.Comparative.Reaches A (z :: v) x✝ = (z = x✝ ∨ z ∈ A ∧ Morphology.Comparative.Reaches A v x✝)

@[instance_reducible]

instance Morphology.Comparative.decReaches {M : Type u_1} [DecidableEq M] (A : Set M) [DecidablePred fun (x : M) => x ∈ A] (v : List M) (y : M) : Decidable (Reaches A v y)

Equations

• Morphology.Comparative.decReaches A [] x✝ = isFalse ⋯
• Morphology.Comparative.decReaches A (z :: v) x✝ = { decide := decide (z = x✝) || decide (z ∈ A ∧ Morphology.Comparative.Reaches A v x✝), reflects_decide := ⋯ }

@[simp]

theorem Morphology.Comparative.reaches_nil {M : Type u_1} (A : Set M) (y : M) : ¬Reaches A [] y

@[simp]

theorem Morphology.Comparative.reaches_cons {M : Type u_1} {A : Set M} {z y : M} {v : List M} : Reaches A (z :: v) y ↔ z = y ∨ z ∈ A ∧ Reaches A v y

theorem Morphology.Comparative.Reaches.mono {M : Type u_1} {A B : Set M} (h : A ⊆ B) {v : List M} {y : M} (hv : Reaches A v y) : Reaches B v y

theorem Morphology.Comparative.Reaches.mem {M : Type u_1} {A : Set M} {v : List M} {y : M} (hv : Reaches A v y) : y ∈ v

theorem Morphology.Comparative.Reaches.find?_eq {M : Type u_1} {A : Set M} {p : M → Prop} [DecidablePred p] (hA : ∀ z ∈ A, ¬p z) {v : List M} {y : M} (hv : Reaches A v y) (hy : p y) : List.find? (fun (x : M) => decide (p x)) v = some y

Through morphs none of which satisfy p, a morph satisfying p that v reaches is the first one in v.

def Morphology.Comparative.OccursOn {M : Type u_1} (root : M → Prop) (A : Set M) (w : List M) (i : ℕ) (y : M) : Prop

In the free form w, the morph at i occurs on the root y through the morphs of A when it is next to y, or next to a morph of A that occurs on y.

Equations

• Morphology.Comparative.OccursOn root A w i y = (root y ∧ (Morphology.Comparative.Reaches A (List.drop (i + 1) w) y ∨ Morphology.Comparative.Reaches A (List.take i w).reverse y))

@[instance_reducible]

instance Morphology.Comparative.instDecidableOccursOnOfDecidableEqOfDecidablePredMemSet {M : Type u_1} (root : M → Prop) [DecidableEq M] [DecidablePred root] (A : Set M) [DecidablePred fun (x : M) => x ∈ A] (w : List M) (i : ℕ) (y : M) : Decidable (OccursOn root A w i y)

Equations

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

def Morphology.Comparative.AffixStep {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (A : Set M) (x : M) : Prop

AffixStep A x is one step of the definition of an affix. Given that the morphs of A are affixes, x is an affix when it is a bound morph that is not a root, and there is a root class such that every occurrence of x occurs on a root and every root it occurs on is of that class.

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instDecidableAffixStepOfDecidableEqOfDecidablePredMemSet {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) [DecidableEq M] [DecidablePred root] (A : Set M) [DecidablePred fun (x : M) => x ∈ A] (x : M) : Decidable (AffixStep F rootClass root A x)

Equations

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

def Morphology.Comparative.RootsContiguous {M : Type u_1} (root : M → Prop) (w : List M) : Prop

The roots of the form w are contiguous when no morph that is not a root lies between two roots, as in a compound.

Equations

• Morphology.Comparative.RootsContiguous root w = ∀ (i : ℕ) (hi : i < w.length), ¬root w[i] → (∀ y ∈ List.take i w, ¬root y) ∨ ∀ y ∈ List.drop (i + 1) w, ¬root y

@[instance_reducible]

instance Morphology.Comparative.instDecidableRootsContiguousOfDecidablePred {M : Type u_1} (root : M → Prop) [DecidablePred root] (w : List M) : Decidable (RootsContiguous root w)

Equations

• Morphology.Comparative.instDecidableRootsContiguousOfDecidablePred root w = Morphology.Comparative.instDecidableRootsContiguousOfDecidablePred._aux_1 root w

def Morphology.Comparative.IsAffixIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (x : M) : Prop

An affix is a morph in a set of morphs each of which is an affix given that the members of the set are, so the affixes are the greatest solution of the definition.

Equations

• Morphology.Comparative.IsAffixIn F rootClass root x = ∃ (A : Set M), x ∈ A ∧ ∀ y ∈ A, Morphology.Comparative.AffixStep F rootClass root A y

theorem Morphology.Comparative.AffixStep.not_root {M : Type u_1} {F : List (List M)} {rootClass : M → Option RootClass} {root : M → Prop} {A : Set M} {x : M} (h : AffixStep F rootClass root A x) : ¬root x

theorem Morphology.Comparative.AffixStep.mem_flatten {M : Type u_1} {F : List (List M)} {rootClass : M → Option RootClass} {root : M → Prop} {A : Set M} {x : M} (h : AffixStep F rootClass root A x) : x ∈ F.flatten

theorem Morphology.Comparative.isAffixIn_iff_sublists {M : Type u_1} {F : List (List M)} {rootClass : M → Option RootClass} {root : M → Prop} [DecidableEq M] [DecidablePred root] {x : M} : IsAffixIn F rootClass root x ↔ ∃ A ∈ (List.filter (fun (y : M) => decide (IsBoundIn F y ∧ ¬root y)) F.flatten.dedup).sublists, x ∈ A ∧ ∀ y ∈ A, AffixStep F rootClass root {z : M | z ∈ A} y

The candidate sets can be restricted to sublists of the bound morphs of the inventory that are not roots.

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsAffixInOfDecidableEqOfDecidablePred {M : Type u_1} {F : List (List M)} {rootClass : M → Option RootClass} {root : M → Prop} [DecidableEq M] [DecidablePred root] (x : M) : Decidable (IsAffixIn F rootClass root x)

Equations

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

The greatest solution

theorem Morphology.Comparative.AffixStep.mono {M : Type u_1} {F : List (List M)} {rootClass : M → Option RootClass} {root : M → Prop} (hF : ∀ w ∈ F, RootsContiguous root w) {A B : Set M} (hAB : A ⊆ B) (hB : ∀ z ∈ B, ¬root z) {x : M} (h : AffixStep F rootClass root A x) : AffixStep F rootClass root B x

When roots are contiguous in every free form, the step is monotone among sets of morphs that are not roots.

theorem Morphology.Comparative.isGreatest_setOf_isAffixIn {M : Type u_1} {F : List (List M)} {rootClass : M → Option RootClass} {root : M → Prop} (hF : ∀ w ∈ F, RootsContiguous root w) : IsGreatest {A : Set M | {x : M | AffixStep F rootClass root A x} = A} {x : M | IsAffixIn F rootClass root x}

When roots are contiguous in every free form, the affixes are the greatest set that the step maps to itself.

Clitics, required affixes and words

def Morphology.Comparative.IsCliticIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (x : M) : Prop

A clitic is a bound morph that is neither a root nor an affix.

Equations

• Morphology.Comparative.IsCliticIn F rootClass root x = (Morphology.Comparative.IsBoundIn F x ∧ ¬root x ∧ ¬Morphology.Comparative.IsAffixIn F rootClass root x ∧ ∃ w ∈ F, x ∈ w)

def Morphology.Comparative.IsAffixOnAt {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (w : List M) (i : ℕ) (y r : M) : Prop

In the free form w, the morph y at i is an affix that occurs on the root r.

Equations

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

def Morphology.Comparative.RequiresAffixIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (r : M) : Prop

A root requires an affix when every free form containing it has an affix on it.

Equations

• Morphology.Comparative.RequiresAffixIn F rootClass root r = ∀ w ∈ F, r ∈ w → ∃ i < w.length, ∃ y ∈ w, Morphology.Comparative.IsAffixOnAt F rootClass root w i y r

def Morphology.Comparative.IsRequiredAffixIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (x r : M) : Prop

A required affix of a root is an affix on it when the root requires an affix, so that the affix must be present unless another replaces it.

Equations

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

def Morphology.Comparative.IsWordIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) (w : List M) : Prop

A word is a form of the language that is a free morph, a clitic, or a root with affixes, among them an affix if the root requires one. Compounds are not covered.

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsCliticIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) [DecidableEq M] [DecidablePred root] (x : M) : Decidable (IsCliticIn F rootClass root x)

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsAffixOnAt {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) [DecidableEq M] [DecidablePred root] (w : List M) (i : ℕ) (y r : M) : Decidable (IsAffixOnAt F rootClass root w i y r)

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instDecidableRequiresAffixIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) [DecidableEq M] [DecidablePred root] (r : M) : Decidable (RequiresAffixIn F rootClass root r)

Equations

• Morphology.Comparative.instDecidableRequiresAffixIn F rootClass root r = Morphology.Comparative.instDecidableRequiresAffixIn._aux_1 F rootClass root r

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsRequiredAffixIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) [DecidableEq M] [DecidablePred root] (x r : M) : Decidable (IsRequiredAffixIn F rootClass root x r)

Equations

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

@[instance_reducible]

instance Morphology.Comparative.instDecidableIsWordIn {M : Type u_1} (F : List (List M)) (rootClass : M → Option RootClass) (root : M → Prop) [DecidableEq M] [DecidablePred root] (w : List M) : Decidable (IsWordIn F rootClass root w)

Equations

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