Word-internal structure

import Linglib.Morphology.Word.Tree · namespace Morphology.Word

A Word.Tree M records how a word is built from material in M, with one constructor for each of Booij's morphological operations: affixation on either side, infixation, circumfixation, compounding, reduplication and conversion. Linearization forgets the structure; attaching affixes to a root in order records the affixes and their order.

Main definitions

Morphology.Word.Tree: the tree of a word's formation.
Morphology.Word.Tree.toList: the material of a tree in surface order.
Morphology.Word.Tree.IsConcatenative: the tree is built by concatenation alone, so toList is the word's segmentation.
Morphology.Word.Tree.attachAll, Morphology.Word.Tree.attachMorphs: attachment of affixes to a root, and of morphs on the sides their kinds give.

Main results

Morphology.Word.Tree.toList_attachAll: the affixes of each side surface outward from the root in the order they were attached.
Morphology.Word.Tree.attachAll_injective: attachment records the affixes and their order.

References

Booij 2012, The Grammar of Words: An Introduction to Linguistic Morphology

The reduplication index

L44–51

The tree

A tree of word-formation operations over material in M.

inductive Tree L55–73

(M : Type u_1) :

Type u_1

root {M : Type u_1} : M → Tree M
A leaf, carrying a single element.
prefixed {M : Type u_1} : M → Tree M → Tree M
Attach an affix before the base.
suffixed {M : Type u_1} : Tree M → M → Tree M
Attach an affix after the base.
infixed {M : Type u_1} : Tree M → M → Tree M
Insert an affix within the base (Khmu s⟨m⟩ka:t "roughen").
circumfixed {M : Type u_1} : M → Tree M → M → Tree M
Wrap the base with a prefix and a suffix (German Ge-sing-e "singing").
compound {M : Type u_1} : Tree M → Tree M → Tree M
Join two stems (bottle + factory).
reduplicated {M : Type u_1} : RedupType → Tree M → Tree M
Total or partial reduplication.
converted {M : Type u_1} : Tree M → Tree M
Convert without added material (noun chain → verb to chain).

Derives Repr.

Built from

Used by Tree.toList, Tree.IsConcatenative, Tree.decIsConcatenative, Tree.attach, Tree.attach_before, Tree.attach_after, Tree.attach_inj, Tree.attach_ne_root, Tree.attachAll, Tree.toList_foldl_attach, Tree.isConcatenative_foldl_attach, Tree.attachMorphs

Used in Fragments/Icelandic/Nouns, Fragments/Mandarin/Resultatives, Morphology/DistributedMorphology/Basic, Baker1985, Svenonius2004 and 1 more

Linearization

The material of the tree, in surface order on the concatenative fragment; an infix follows its base and reduplicative copies contribute nothing.

def Tree.toList L81–92

{M : Type u_1} :

Tree M → List M

(Tree.root m).toList = [m]
(Tree.prefixed afx base).toList = afx :: base.toList
(base.suffixed afx).toList = base.toList ++ [afx]
(base.infixed afx).toList = base.toList ++ [afx]
(Tree.circumfixed pre base suf).toList = pre :: base.toList ++ [suf]
(left.compound right).toList = left.toList ++ right.toList
(Tree.reduplicated a base).toList = base.toList
base.converted.toList = base.toList

Built from

Used by Tree.toList_foldl_attach, Tree.toList_attachAll

Used in Fragments/Icelandic/Nouns, Fragments/Mandarin/Resultatives, Morphology/DistributedMorphology/Basic, Baker1985, Hyman2003 and 1 more

IsConcatenative t asserts that t is built by concatenation alone — no infixation, circumfixation, or reduplication — so toList is the word's segmentation.

def Tree.IsConcatenative L94–105

{M : Type u_1} :

Tree M → Prop

(Tree.root a).IsConcatenative = True
(Tree.prefixed a b).IsConcatenative = b.IsConcatenative
(b.suffixed a).IsConcatenative = b.IsConcatenative
(l.compound r).IsConcatenative = (l.IsConcatenative ∧ r.IsConcatenative)
b.converted.IsConcatenative = b.IsConcatenative
(a.infixed a_1).IsConcatenative = False
(Tree.circumfixed a a_1 a_2).IsConcatenative = False
(Tree.reduplicated a a_1).IsConcatenative = False

Built from

Used by Tree.decIsConcatenative, Tree.isConcatenative_foldl_attach, Tree.isConcatenative_attachAll

Used in Svenonius2004

L107–111

Attachment by side

Attach affixes to a root in order, innermost first.

def Tree.attachAll L133–135

{M : Type u_1} (root : M) (affixes : List (Morph.Side × M)) :

Tree M

The definition is too large to print here; read it in the source.

Built from

Used by Tree.attachAll_nil, Tree.attachAll_concat, Tree.attachAll_injective, Tree.toList_attachAll, Tree.isConcatenative_attachAll

Used in Morphology/DistributedMorphology/Basic

L137

L139–141

The tree records the affixes attached and their order: attachment to a root is injective.

theorem Tree.attachAll_injective L143–156

{M : Type u_1} (root : M) :

Function.Injective (attachAll root)

Built from

L158–165

Attachment surfaces with the affixes of each side read outward from the root in the order they were attached, prefixes outermost first and suffixes innermost first.

theorem Tree.toList_attachAll L167–174

{M : Type u_1} (root : M) (affixes : List (Morph.Side × M)) :

(attachAll root affixes).toList = (List.map (fun (x : Morph.Side × M) => x.2) (List.filter (fun (x : Morph.Side × M) => decide (x.1 = Morph.Side.before)) affixes)).reverse ++ root :: List.map (fun (x : Morph.Side × M) => x.2) (List.filter (fun (x : Morph.Side × M) => decide (x.1 = Morph.Side.after)) affixes)

Built from ,

L176–182

L184–186

Attachment of morphs

Attach morphs to a root in order, each on the side its kind gives; a morph bound on no side, an infix or a free form, is not attached.

def Tree.attachMorphs L190–193

(root : Morph) (ms : List Morph) :

Tree Morph

The definition is too large to print here; read it in the source.

Built from

Used by Tree.attachMorphs_injOn

Used in Baker1985

L195–208