Morphological Word Structure

@cite{hayes-2009}

Hierarchical representation of word-internal structure via the MorphWord inductive type: a tree of morphemes where affixation, compounding, reduplication, and conversion are structural operations.

Design

MorphWord and MorphRule are complementary:

• MorphRule represents inflectional processes (String → String)
• MorphWord represents derivational/compositional structure (tree of morphemes)

Morpheme boundaries fall out naturally from linearization — the boundary positions are implicit between adjacent morphemes in the flattened list.

Constructors

Constructor	Operation	Example
root	leaf morpheme	walk
prefixed	prefix attachment	un- + happy
suffixed	suffix attachment	walk + -ed
infixed	infix insertion	Tagalog -um- in sulat
circumfixed	circumfix wrapping	German ge-mach-t
compound	compounding	desk + lamp
reduplicated	total or partial reduplication	Warlpiri kijikiji
converted	zero affixation / conversion	noun telephone → verb

structure Theories.Morphology.WordStructure.Morpheme : Type

A morpheme: the minimal meaningful unit (Hayes §5.1).

Carries a surface form, an optional gloss, and its morphological status (free word, clitic, or affix).

• form : String
• gloss : String
• status : Core.Morphology.MorphStatus

instance Theories.Morphology.WordStructure.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Theories.Morphology.WordStructure.instDecidableEqMorpheme = Theories.Morphology.WordStructure.instDecidableEqMorpheme.decEq

def Theories.Morphology.WordStructure.instDecidableEqMorpheme.decEq (x✝ x✝¹ : Morpheme) : Decidable (x✝ = x✝¹)

Equations

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

def Theories.Morphology.WordStructure.instBEqMorpheme.beq : Morpheme → Morpheme → Bool

Equations

• Theories.Morphology.WordStructure.instBEqMorpheme.beq { form := a, gloss := a_1, status := a_2 } { form := b, gloss := b_1, status := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Theories.Morphology.WordStructure.instBEqMorpheme.beq x✝¹ x✝ = false

instance Theories.Morphology.WordStructure.instBEqMorpheme : BEq Morpheme

Equations

• Theories.Morphology.WordStructure.instBEqMorpheme = { beq := Theories.Morphology.WordStructure.instBEqMorpheme.beq }

instance Theories.Morphology.WordStructure.instReprMorpheme : Repr Morpheme

Equations

• Theories.Morphology.WordStructure.instReprMorpheme = { reprPrec := Theories.Morphology.WordStructure.instReprMorpheme.repr }

def Theories.Morphology.WordStructure.instReprMorpheme.repr : Morpheme → Nat → Std.Format

Equations

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

inductive Theories.Morphology.WordStructure.RedupType : Type

Type of reduplication (Hayes §5.2).

• total: copies the entire base (Warlpiri kijikiji from kiji)
• partialCopy copied: copies a prosodic template; the copied material is stored explicitly since it depends on prosodic shape (determined at construction time, not derivable from strings alone). Example: Ilokano ag-tráb-trabáho (partial copy trab).

• total : RedupType
• partialCopy (copied : String) : RedupType

def Theories.Morphology.WordStructure.instDecidableEqRedupType.decEq (x✝ x✝¹ : RedupType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Theories.Morphology.WordStructure.instDecidableEqRedupType.decEq Theories.Morphology.WordStructure.RedupType.total Theories.Morphology.WordStructure.RedupType.total = isTrue ⋯
• Theories.Morphology.WordStructure.instDecidableEqRedupType.decEq Theories.Morphology.WordStructure.RedupType.total (Theories.Morphology.WordStructure.RedupType.partialCopy copied) = isFalse ⋯
• Theories.Morphology.WordStructure.instDecidableEqRedupType.decEq (Theories.Morphology.WordStructure.RedupType.partialCopy copied) Theories.Morphology.WordStructure.RedupType.total = isFalse ⋯

instance Theories.Morphology.WordStructure.instDecidableEqRedupType : DecidableEq RedupType

Equations

• Theories.Morphology.WordStructure.instDecidableEqRedupType = Theories.Morphology.WordStructure.instDecidableEqRedupType.decEq

instance Theories.Morphology.WordStructure.instBEqRedupType : BEq RedupType

Equations

• Theories.Morphology.WordStructure.instBEqRedupType = { beq := Theories.Morphology.WordStructure.instBEqRedupType.beq }

def Theories.Morphology.WordStructure.instBEqRedupType.beq : RedupType → RedupType → Bool

Equations

• Theories.Morphology.WordStructure.instBEqRedupType.beq Theories.Morphology.WordStructure.RedupType.total Theories.Morphology.WordStructure.RedupType.total = true
• Theories.Morphology.WordStructure.instBEqRedupType.beq (Theories.Morphology.WordStructure.RedupType.partialCopy a) (Theories.Morphology.WordStructure.RedupType.partialCopy b) = (a == b)
• Theories.Morphology.WordStructure.instBEqRedupType.beq x✝¹ x✝ = false

def Theories.Morphology.WordStructure.instReprRedupType.repr : RedupType → Nat → Std.Format

Equations

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

instance Theories.Morphology.WordStructure.instReprRedupType : Repr RedupType

Equations

• Theories.Morphology.WordStructure.instReprRedupType = { reprPrec := Theories.Morphology.WordStructure.instReprRedupType.repr }

inductive Theories.Morphology.WordStructure.MorphWord : Type

Hierarchical word structure as a tree of morphemes.

Each constructor corresponds to a morphological operation from Hayes §5.2–5.5. The tree structure captures the derivational history and word-internal constituency.

• root : Morpheme → MorphWord

  Leaf node: a single morpheme (free or bound).

• prefixed : Morpheme → MorphWord → MorphWord

  Hayes §5.2: attach morpheme before base.

• suffixed : MorphWord → Morpheme → MorphWord

  Hayes §5.2: attach morpheme after base.

• infixed : MorphWord → Morpheme → Nat → MorphWord

  Hayes §5.2: insert morpheme at position pos within base's surface form. Example: Tagalog -um- in s⟨um⟩ulat.

• circumfixed : Morpheme → MorphWord → Morpheme → MorphWord

  Hayes §5.2: wrap base with a prefix and suffix. Example: German ge-mach-t.

• compound : MorphWord → MorphWord → MorphWord

  Hayes §5.4: two stems joined. Example: desk + lamp.

• reduplicated : RedupType → MorphWord → MorphWord

  Hayes §5.2: total or partial reduplication.

• converted : MorphWord → MorphWord

  Hayes §5.2: zero affixation / conversion. Example: noun telephone → verb to telephone.

def Theories.Morphology.WordStructure.instReprMorphWord.repr : MorphWord → Nat → Std.Format

Equations

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

instance Theories.Morphology.WordStructure.instReprMorphWord : Repr MorphWord

Equations

• Theories.Morphology.WordStructure.instReprMorphWord = { reprPrec := Theories.Morphology.WordStructure.instReprMorphWord.repr }

def Theories.Morphology.WordStructure.MorphWord.surface : MorphWord → String

Extract the flat surface string from the morphological tree.

Equations

• (Theories.Morphology.WordStructure.MorphWord.root a).surface = a.form
• (Theories.Morphology.WordStructure.MorphWord.prefixed a a_1).surface = a.form ++ a_1.surface
• (a.suffixed a_1).surface = a.surface ++ a_1.form
• (a.infixed a_1 a_2).surface = String.ofList (List.take a_2 a.surface.toList) ++ a_1.form ++ String.ofList (List.drop a_2 a.surface.toList)
• (Theories.Morphology.WordStructure.MorphWord.circumfixed a a_1 a_2).surface = a.form ++ a_1.surface ++ a_2.form
• (a.compound a_1).surface = a.surface ++ a_1.surface
• (Theories.Morphology.WordStructure.MorphWord.reduplicated Theories.Morphology.WordStructure.RedupType.total a_1).surface = a_1.surface ++ a_1.surface
• (Theories.Morphology.WordStructure.MorphWord.reduplicated (Theories.Morphology.WordStructure.RedupType.partialCopy a_2) a_1).surface = a_2 ++ a_1.surface
• a.converted.surface = a.surface

def Theories.Morphology.WordStructure.MorphWord.morphemes : MorphWord → List Morpheme

Flatten the morphological tree into a list of morphemes in linear (left-to-right surface) order. Morpheme boundaries are implicit: they fall between adjacent elements.

Equations

• One or more equations did not get rendered due to their size.
• (Theories.Morphology.WordStructure.MorphWord.root a).morphemes = [a]
• (Theories.Morphology.WordStructure.MorphWord.prefixed a a_1).morphemes = a :: a_1.morphemes
• (a.suffixed a_1).morphemes = a.morphemes ++ [a_1]
• (a.infixed a_1 a_2).morphemes = a.morphemes ++ [a_1]
• (a.compound a_1).morphemes = a.morphemes ++ a_1.morphemes
• (Theories.Morphology.WordStructure.MorphWord.reduplicated a a_1).morphemes = a_1.morphemes
• a.converted.morphemes = a.morphemes

def Theories.Morphology.WordStructure.MorphWord.morphemeCount (w : MorphWord) : Nat

Number of morphemes in the word.

Equations

• w.morphemeCount = w.morphemes.length

def Theories.Morphology.WordStructure.MorphWord.boundaryPositions : MorphWord → List Nat

Positions of morpheme boundaries in the surface string. Each Nat is a character offset where one morpheme ends and the next begins. Phonological rules can reference these positions (Hayes Chs 6–8).

Equations

• One or more equations did not get rendered due to their size.
• (Theories.Morphology.WordStructure.MorphWord.root a).boundaryPositions = []
• (Theories.Morphology.WordStructure.MorphWord.prefixed a a_1).boundaryPositions = a.form.length :: List.map (fun (x : Nat) => x + a.form.length) a_1.boundaryPositions
• (a.suffixed a_1).boundaryPositions = a.boundaryPositions ++ [a.surface.length, a.surface.length + a_1.form.length]
• (a.compound a_1).boundaryPositions = a.boundaryPositions ++ [a.surface.length] ++ List.map (fun (x : Nat) => x + a.surface.length) a_1.boundaryPositions
• a.converted.boundaryPositions = a.boundaryPositions

def Theories.Morphology.WordStructure.MorphWord.isSimple : MorphWord → Bool

Is this word a bare root (single morpheme)?

Equations

• (Theories.Morphology.WordStructure.MorphWord.root a).isSimple = true
• x✝.isSimple = false

def Theories.Morphology.WordStructure.MorphWord.isCompound : MorphWord → Bool

Is this word a compound?

Equations

• (a.compound a_1).isCompound = true
• x✝.isCompound = false

def Theories.Morphology.WordStructure.MorphWord.isReduplicated : MorphWord → Bool

Does this word involve reduplication?

Equations

• (Theories.Morphology.WordStructure.MorphWord.reduplicated a a_1).isReduplicated = true
• x✝.isReduplicated = false

def Theories.Morphology.WordStructure.MorphWord.isConverted : MorphWord → Bool

Is this word derived by conversion (zero affixation)?

Equations

• a.converted.isConverted = true
• x✝.isConverted = false

def Theories.Morphology.WordStructure.MorphWord.depth : MorphWord → Nat

Morphological depth: number of derivational steps from the root(s).

Equations

• (Theories.Morphology.WordStructure.MorphWord.root a).depth = 0
• (Theories.Morphology.WordStructure.MorphWord.prefixed a a_1).depth = 1 + a_1.depth
• (a.suffixed a_1).depth = 1 + a.depth
• (a.infixed a_1 a_2).depth = 1 + a.depth
• (Theories.Morphology.WordStructure.MorphWord.circumfixed a a_1 a_2).depth = 1 + a_1.depth
• (a.compound a_1).depth = 1 + max a.depth a_1.depth
• (Theories.Morphology.WordStructure.MorphWord.reduplicated a a_1).depth = 1 + a_1.depth
• a.converted.depth = 1 + a.depth

def Theories.Morphology.WordStructure.MorphWord.toCircumfixExponence : MorphWord → Option Morphology.Circumfix.CircumfixExponence

Convert a circumfixed MorphWord to a CircumfixExponence. Returns none for non-circumfixed words.

Equations

• (Theories.Morphology.WordStructure.MorphWord.circumfixed pre base suf).toCircumfixExponence = some { prefix_ := pre.form, suffix_ := suf.form, stem := base.surface }
• x✝.toCircumfixExponence = none

theorem Theories.Morphology.WordStructure.conversion_preserves_surface (w : MorphWord) : w.converted.surface = w.surface

Conversion preserves the surface form.

theorem Theories.Morphology.WordStructure.compound_surface (l r : MorphWord) : (l.compound r).surface = l.surface ++ r.surface

The surface form of a compound is the concatenation of its parts.

theorem Theories.Morphology.WordStructure.total_redup_surface (w : MorphWord) : (MorphWord.reduplicated RedupType.total w).surface = w.surface ++ w.surface

Total reduplication doubles the surface form.

theorem Theories.Morphology.WordStructure.root_depth_zero (m : Morpheme) : (MorphWord.root m).depth = 0

A bare root has depth zero.

theorem Theories.Morphology.WordStructure.root_morphemeCount_one (m : Morpheme) : (MorphWord.root m).morphemeCount = 1

A bare root contains exactly one morpheme.

theorem Theories.Morphology.WordStructure.circumfixed_bridge (pre suf : Morpheme) (base : MorphWord) : (MorphWord.circumfixed pre base suf).toCircumfixExponence = some { prefix_ := pre.form, suffix_ := suf.form, stem := base.surface }

The circumfix bridge extracts the correct prefix, suffix, and stem.