Morphological Word Structure

[Hay09]

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

Circumfixal exponence wraps a stem with morphological material on both sides (prefix + suffix). Theory-neutral surface description; how a circumfix arises (head movement in DM, readjustment elsewhere) is theory-specific.

Examples: German ge-mach-t, Tigrinya ʔay-...-n, Malay ke-baik-an.

structure Morphology.Circumfix.CircumfixExponence : Type

Circumfixal exponence: a stem wrapped by a prefix and suffix.

• prefix_ : String
• suffix_ : String
• stem : String
• gloss : String

def Morphology.Circumfix.instReprCircumfixExponence.repr : CircumfixExponence → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Circumfix.instReprCircumfixExponence : Repr CircumfixExponence

Equations

• Morphology.Circumfix.instReprCircumfixExponence = { reprPrec := Morphology.Circumfix.instReprCircumfixExponence.repr }

@[implicit_reducible]

instance Morphology.Circumfix.instDecidableEqCircumfixExponence : DecidableEq CircumfixExponence

Equations

• Morphology.Circumfix.instDecidableEqCircumfixExponence = Morphology.Circumfix.instDecidableEqCircumfixExponence.decEq

def Morphology.Circumfix.instDecidableEqCircumfixExponence.decEq (x✝ x✝¹ : CircumfixExponence) : Decidable (x✝ = x✝¹)

Equations

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

def Morphology.Circumfix.CircumfixExponence.realize (c : CircumfixExponence) : String

Apply circumfixal exponence to produce the surface form.

Equations

• c.realize = c.prefix_ ++ c.stem ++ c.suffix_

def Morphology.Circumfix.CircumfixExponence.isDiscontinuous (_c : CircumfixExponence) : Bool

A circumfix is discontinuous: its exponents are separated by the stem.

Equations

• _c.isDiscontinuous = true

def Morphology.Circumfix.CircumfixExponence.attachmentSide (_c : CircumfixExponence) : AttachmentSide

The attachment side of a circumfix is AttachmentSide.circumfix.

Equations

• _c.attachmentSide = Morphology.AttachmentSide.circumfix

theorem Morphology.Circumfix.circumfix_attachment (c : CircumfixExponence) : c.attachmentSide = AttachmentSide.circumfix

theorem Morphology.Circumfix.circumfix_discontinuous (c : CircumfixExponence) : c.isDiscontinuous = true

theorem Morphology.Circumfix.circumfix_realize_concat (c : CircumfixExponence) : c.realize = c.prefix_ ++ c.stem ++ c.suffix_

def Morphology.Circumfix.germanPastParticiple (stem : String) : CircumfixExponence

German past participle ge-...-t.

Equations

• Morphology.Circumfix.germanPastParticiple stem = { prefix_ := "ge-", suffix_ := "-t", stem := stem, gloss := "PTCP" }

theorem Morphology.Circumfix.german_pp_example : (germanPastParticiple "mach").realize = "ge-mach-t"

structure 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 : MorphStatus

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

Equations

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

@[implicit_reducible]

instance Morphology.WordStructure.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

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

def Morphology.WordStructure.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.WordStructure.instReprMorpheme : Repr Morpheme

Equations

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

inductive 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

@[implicit_reducible]

instance Morphology.WordStructure.instDecidableEqRedupType : DecidableEq RedupType

Equations

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

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

Equations

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

@[implicit_reducible]

instance Morphology.WordStructure.instReprRedupType : Repr RedupType

Equations

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

def Morphology.WordStructure.instReprRedupType.repr : RedupType → ℕ → Std.Format

Equations

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

inductive 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 → ℕ → 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 Morphology.WordStructure.instReprMorphWord.repr : MorphWord → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.WordStructure.instReprMorphWord : Repr MorphWord

Equations

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

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

Extract the flat surface string from the morphological tree.

Equations

• (Morphology.WordStructure.MorphWord.root a).surface = a.form
• (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)
• (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
• (Morphology.WordStructure.MorphWord.reduplicated Morphology.WordStructure.RedupType.total a_1).surface = a_1.surface ++ a_1.surface
• (Morphology.WordStructure.MorphWord.reduplicated (Morphology.WordStructure.RedupType.partialCopy a_2) a_1).surface = a_2 ++ a_1.surface
• a.converted.surface = a.surface

def 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.
• (Morphology.WordStructure.MorphWord.root a).morphemes = [a]
• (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
• (Morphology.WordStructure.MorphWord.reduplicated a a_1).morphemes = a_1.morphemes
• a.converted.morphemes = a.morphemes

def Morphology.WordStructure.MorphWord.morphemeCount (w : MorphWord) : ℕ

Number of morphemes in the word.

Equations

• w.morphemeCount = w.morphemes.length

def Morphology.WordStructure.MorphWord.boundaryPositions : MorphWord → List ℕ

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.
• (Morphology.WordStructure.MorphWord.root a).boundaryPositions = []
• (Morphology.WordStructure.MorphWord.prefixed a a_1).boundaryPositions = a.form.length :: List.map (fun (x : ℕ) => 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 : ℕ) => x + a.surface.length) a_1.boundaryPositions
• a.converted.boundaryPositions = a.boundaryPositions

def Morphology.WordStructure.MorphWord.IsSimple : MorphWord → Prop

Is this word a bare root (single morpheme)?

Equations

• (Morphology.WordStructure.MorphWord.root a).IsSimple = True
• x✝.IsSimple = False

@[implicit_reducible]

instance Morphology.WordStructure.instDecidablePredMorphWordIsSimple : DecidablePred MorphWord.IsSimple

Equations

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

def Morphology.WordStructure.MorphWord.IsCompound : MorphWord → Prop

Is this word a compound?

Equations

• (a.compound a_1).IsCompound = True
• x✝.IsCompound = False

@[implicit_reducible]

instance Morphology.WordStructure.instDecidablePredMorphWordIsCompound : DecidablePred MorphWord.IsCompound

Equations

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

def Morphology.WordStructure.MorphWord.IsReduplicated : MorphWord → Prop

Does this word involve reduplication?

Equations

• (Morphology.WordStructure.MorphWord.reduplicated a a_1).IsReduplicated = True
• x✝.IsReduplicated = False

@[implicit_reducible]

instance Morphology.WordStructure.instDecidablePredMorphWordIsReduplicated : DecidablePred MorphWord.IsReduplicated

Equations

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

def Morphology.WordStructure.MorphWord.IsConverted : MorphWord → Prop

Is this word derived by conversion (zero affixation)?

Equations

• a.converted.IsConverted = True
• x✝.IsConverted = False

@[implicit_reducible]

instance Morphology.WordStructure.instDecidablePredMorphWordIsConverted : DecidablePred MorphWord.IsConverted

Equations

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

def Morphology.WordStructure.MorphWord.depth : MorphWord → ℕ

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

Equations

• (Morphology.WordStructure.MorphWord.root a).depth = 0
• (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
• (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
• (Morphology.WordStructure.MorphWord.reduplicated a a_1).depth = 1 + a_1.depth
• a.converted.depth = 1 + a.depth

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

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

Equations

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

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

Conversion preserves the surface form.

theorem 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 Morphology.WordStructure.total_redup_surface (w : MorphWord) : (MorphWord.reduplicated RedupType.total w).surface = w.surface ++ w.surface

Total reduplication doubles the surface form.

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

A bare root has depth zero.

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

A bare root contains exactly one morpheme.

theorem 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.