Word-internal structure

A Word.Tree M is an operation-typed tree over the word-formation signature: each constructor is one of [Boo12]'s morphological operations, with its own arity and material. Every subtree is a partial word; the tree records derivational history and word-internal constituency, which applying the operations as functions would forget.

Main declarations

• Word.Tree — the operation-typed tree
• Word.Tree.toList, Word.Tree.IsConcatenative — linearization, and the shapes where it is the word's segmentation
• Word.Tree.base, Word.Tree.stem, Word.Tree.roots — [Boo12]'s relational notions
• Word.Tree.IsKindCoherent — attachment kinds match their positions

The reduplication index

inductive Morphology.Word.Tree.RedupType : Type

The type of a reduplication step.

• total : RedupType

  Copies the entire base (Javanese omaha → omaha-omaha "various houses").

• partialCopy : RedupType

  Copies a prosodic template (Javanese tamu → tətamu "to visit").

@[implicit_reducible]

instance Morphology.Word.Tree.instDecidableEqRedupType : DecidableEq RedupType

Equations

• Morphology.Word.Tree.instDecidableEqRedupType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Word.Tree.instReprRedupType.repr : RedupType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Word.Tree.instReprRedupType : Repr RedupType

Equations

• Morphology.Word.Tree.instReprRedupType = { reprPrec := Morphology.Word.Tree.instReprRedupType.repr }

The tree

inductive Morphology.Word.Tree (M : Type u_1) : Type u_1

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

• 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).

def Morphology.Word.instReprTree.repr {M✝ : Type u_1} [Repr M✝] : Tree M✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Word.instReprTree {M✝ : Type u_1} [Repr M✝] : Repr (Tree M✝)

Equations

• Morphology.Word.instReprTree = { reprPrec := Morphology.Word.instReprTree.repr }

Linearization

def Morphology.Word.Tree.toList {M : Type u_1} : Tree M → List M

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

Equations

• (Morphology.Word.Tree.root a).toList = [a]
• (Morphology.Word.Tree.prefixed a a_1).toList = a :: a_1.toList
• (a.suffixed a_1).toList = a.toList ++ [a_1]
• (a.infixed a_1).toList = a.toList ++ [a_1]
• (Morphology.Word.Tree.circumfixed a a_1 a_2).toList = a :: a_1.toList ++ [a_2]
• (a.compound a_1).toList = a.toList ++ a_1.toList
• (Morphology.Word.Tree.reduplicated a a_1).toList = a_1.toList
• a.converted.toList = a.toList

theorem Morphology.Word.Tree.toList_ne_nil {M : Type u_1} (t : Tree M) : t.toList ≠ []

def Morphology.Word.Tree.map {M : Type u_1} {N : Type u_2} (f : M → N) : Tree M → Tree N

Apply a function to the material at every node, preserving the tree's shape.

Equations

• Morphology.Word.Tree.map f (Morphology.Word.Tree.root a) = Morphology.Word.Tree.root (f a)
• Morphology.Word.Tree.map f (Morphology.Word.Tree.prefixed a a_1) = Morphology.Word.Tree.prefixed (f a) (Morphology.Word.Tree.map f a_1)
• Morphology.Word.Tree.map f (a.suffixed a_1) = (Morphology.Word.Tree.map f a).suffixed (f a_1)
• Morphology.Word.Tree.map f (a.infixed a_1) = (Morphology.Word.Tree.map f a).infixed (f a_1)
• Morphology.Word.Tree.map f (Morphology.Word.Tree.circumfixed a a_1 a_2) = Morphology.Word.Tree.circumfixed (f a) (Morphology.Word.Tree.map f a_1) (f a_2)
• Morphology.Word.Tree.map f (a.compound a_1) = (Morphology.Word.Tree.map f a).compound (Morphology.Word.Tree.map f a_1)
• Morphology.Word.Tree.map f (Morphology.Word.Tree.reduplicated a a_1) = Morphology.Word.Tree.reduplicated a (Morphology.Word.Tree.map f a_1)
• Morphology.Word.Tree.map f a.converted = (Morphology.Word.Tree.map f a).converted

def Morphology.Word.Tree.IsConcatenative {M : Type u_1} : Tree M → Prop

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

Equations

• (Morphology.Word.Tree.root a).IsConcatenative = True
• (Morphology.Word.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
• (Morphology.Word.Tree.circumfixed a a_1 a_2).IsConcatenative = False
• (Morphology.Word.Tree.reduplicated a a_1).IsConcatenative = False

@[implicit_reducible]

instance Morphology.Word.Tree.decIsConcatenative {M : Type u_1} (t : Tree M) : Decidable t.IsConcatenative

Equations

• (Morphology.Word.Tree.root a).decIsConcatenative = isTrue trivial
• (Morphology.Word.Tree.prefixed a b).decIsConcatenative = b.decIsConcatenative
• (b.suffixed a).decIsConcatenative = b.decIsConcatenative
• b.converted.decIsConcatenative = b.decIsConcatenative
• (l.compound r).decIsConcatenative = instDecidableAnd
• (a.infixed a_1).decIsConcatenative = isFalse ⋯
• (Morphology.Word.Tree.circumfixed a a_1 a_2).decIsConcatenative = isFalse ⋯
• (Morphology.Word.Tree.reduplicated a a_1).decIsConcatenative = isFalse ⋯

Laws

@[simp]

theorem Morphology.Word.Tree.map_id {M : Type u_1} (t : Tree M) : map id t = t

theorem Morphology.Word.Tree.map_map {M : Type u_1} {N : Type u_2} {O : Type u_3} (f : M → N) (g : N → O) (t : Tree M) : map g (map f t) = map (g ∘ f) t

theorem Morphology.Word.Tree.toList_map {M : Type u_1} {N : Type u_2} (f : M → N) (t : Tree M) : (map f t).toList = List.map f t.toList

Linearization is natural in the material.

Structural measures

def Morphology.Word.Tree.depth {M : Type u_1} : Tree M → ℕ

The number of operations above the deepest root.

Equations

• (Morphology.Word.Tree.root a).depth = 0
• (l.compound r).depth = max l.depth r.depth + 1
• (Morphology.Word.Tree.prefixed a b).depth = b.depth + 1
• (b.suffixed a).depth = b.depth + 1
• (b.infixed a).depth = b.depth + 1
• (Morphology.Word.Tree.circumfixed a b a_1).depth = b.depth + 1
• (Morphology.Word.Tree.reduplicated a b).depth = b.depth + 1
• b.converted.depth = b.depth + 1

theorem Morphology.Word.Tree.depth_root {M : Type u_1} (m : M) : (root m).depth = 0

A bare root has depth zero.

Relational accessors

def Morphology.Word.Tree.base {M : Type u_1} : Tree M → Option (Tree M)

The daughter the outermost operation applied to; none for a bare root and for compounds.

Equations

• (Morphology.Word.Tree.root a).base = none
• (l.compound r).base = none
• (Morphology.Word.Tree.prefixed a b).base = some b
• (b.suffixed a).base = some b
• (b.infixed a).base = some b
• (Morphology.Word.Tree.circumfixed a b a_1).base = some b
• (Morphology.Word.Tree.reduplicated a b).base = some b
• b.converted.base = some b

def Morphology.Word.Tree.stem {M : Type u_1} (infl : M → Bool) : Tree M → Tree M

The tree with outer affixation by infl-material stripped.

Equations

• Morphology.Word.Tree.stem infl (Morphology.Word.Tree.prefixed a b) = if infl a = true then Morphology.Word.Tree.stem infl b else Morphology.Word.Tree.prefixed a b
• Morphology.Word.Tree.stem infl (b.suffixed a) = if infl a = true then Morphology.Word.Tree.stem infl b else b.suffixed a
• Morphology.Word.Tree.stem infl (b.infixed a) = if infl a = true then Morphology.Word.Tree.stem infl b else b.infixed a
• Morphology.Word.Tree.stem infl (Morphology.Word.Tree.circumfixed pre b suf) = if (infl pre && infl suf) = true then Morphology.Word.Tree.stem infl b else Morphology.Word.Tree.circumfixed pre b suf
• Morphology.Word.Tree.stem infl x✝ = x✝

def Morphology.Word.Tree.roots {M : Type u_1} : Tree M → List M

The material at the leaves.

Equations

• (Morphology.Word.Tree.root a).roots = [a]
• (l.compound r).roots = l.roots ++ r.roots
• (Morphology.Word.Tree.prefixed a b).roots = b.roots
• (b.suffixed a).roots = b.roots
• (b.infixed a).roots = b.roots
• (Morphology.Word.Tree.circumfixed a b a_1).roots = b.roots
• (Morphology.Word.Tree.reduplicated a b).roots = b.roots
• b.converted.roots = b.roots

theorem Morphology.Word.Tree.stem_root {M : Type u_1} {infl : M → Bool} (m : M) : stem infl (root m) = root m

theorem Morphology.Word.Tree.stem_suffixed_of_infl {M : Type u_1} {infl : M → Bool} {afx : M} (b : Tree M) (h : infl afx = true) : stem infl (b.suffixed afx) = stem infl b

theorem Morphology.Word.Tree.stem_suffixed_of_not_infl {M : Type u_1} {infl : M → Bool} {afx : M} (b : Tree M) (h : ¬infl afx = true) : stem infl (b.suffixed afx) = b.suffixed afx

Kind coherence

def Morphology.Word.Tree.IsKindCoherent : Tree Morph → Prop

IsKindCoherent t asserts that the material's Kinds agree with their positions — no suffixed node holds a prefix morph — and every leaf is a root or a free form.

Equations

• (Morphology.Word.Tree.root m).IsKindCoherent = (m.kind = Morphology.Morph.Kind.root ∨ m.kind = Morphology.Morph.Kind.free)
• (Morphology.Word.Tree.prefixed m b).IsKindCoherent = (m.side? = some Morphology.Morph.Side.before ∧ b.IsKindCoherent)
• (b.suffixed m).IsKindCoherent = (m.side? = some Morphology.Morph.Side.after ∧ b.IsKindCoherent)
• (Morphology.Word.Tree.circumfixed pre b suf).IsKindCoherent = (pre.side? = some Morphology.Morph.Side.before ∧ suf.side? = some Morphology.Morph.Side.after ∧ b.IsKindCoherent)
• (l.compound r).IsKindCoherent = (l.IsKindCoherent ∧ r.IsKindCoherent)
• (b.infixed a).IsKindCoherent = b.IsKindCoherent
• (Morphology.Word.Tree.reduplicated a b).IsKindCoherent = b.IsKindCoherent
• b.converted.IsKindCoherent = b.IsKindCoherent

@[implicit_reducible]

instance Morphology.Word.Tree.decIsKindCoherent (t : Tree Morph) : Decidable t.IsKindCoherent

Equations

• (Morphology.Word.Tree.root m).decIsKindCoherent = Morphology.Word.Tree.decIsKindCoherent._aux_1 m
• (Morphology.Word.Tree.prefixed m b).decIsKindCoherent = instDecidableAnd
• (b.suffixed m).decIsKindCoherent = instDecidableAnd
• (Morphology.Word.Tree.circumfixed pre b suf).decIsKindCoherent = instDecidableAnd
• (l.compound r).decIsKindCoherent = instDecidableAnd
• (b.infixed a).decIsKindCoherent = b.decIsKindCoherent
• (Morphology.Word.Tree.reduplicated a b).decIsKindCoherent = b.decIsKindCoherent
• b.converted.decIsKindCoherent = b.decIsKindCoherent