Morphological Infrastructure

@cite{bybee-1985} @cite{champollion-2017} @cite{link-1983} @cite{zwicky-pullum-1983}

Framework-agnostic types for morphological analysis and compositional morphological rules.

Typological Classification

• AttachmentSide: prefix, suffix, infix, circumfix
• SelectionDegree: how restrictive a morpheme's host selection is
• MorphStatus: free word / simple clitic / special clitic / affix
• ParadigmCell: one cell in a morphological paradigm (form + features)

@cite{bybee-1985} Relevance Hierarchy

MorphCategory classifies morpheme functional categories ordered by semantic relevance to the stem:

stem < derivation < valence < voice < aspect < tense < mood < negation < agreement

Compositional Rules

• MorphRule σ: a morphological rule carrying formal AND semantic effects
• Stem σ: a lexical stem with its inflectional paradigm

A MorphRule σ transforms a stem's surface form, morphosyntactic features, and meaning of type σ simultaneously. Rules where the semantic effect is id (e.g., verb agreement) are marked isVacuous := true.

inductive Core.Morphology.AttachmentSide : Type

Side on which a bound morpheme attaches to its host.

• prefix : AttachmentSide
• suffix : AttachmentSide
• infix : AttachmentSide
• circumfix : AttachmentSide

instance Core.Morphology.instDecidableEqAttachmentSide : DecidableEq AttachmentSide

Equations

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

instance Core.Morphology.instReprAttachmentSide : Repr AttachmentSide

Equations

• Core.Morphology.instReprAttachmentSide = { reprPrec := Core.Morphology.instReprAttachmentSide.repr }

def Core.Morphology.instReprAttachmentSide.repr : AttachmentSide → Nat → Std.Format

Equations

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

instance Core.Morphology.instBEqAttachmentSide : BEq AttachmentSide

Equations

• Core.Morphology.instBEqAttachmentSide = { beq := Core.Morphology.instBEqAttachmentSide.beq }

def Core.Morphology.instBEqAttachmentSide.beq : AttachmentSide → AttachmentSide → Bool

Equations

• Core.Morphology.instBEqAttachmentSide.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Core.Morphology.SelectionDegree : Type

How restrictive a morpheme is about what it can attach to.

@cite{zwicky-pullum-1983} criterion A: clitics exhibit low selection (attach to virtually any word), while affixes exhibit high selection (attach only to specific stems or categories).

• low : SelectionDegree

  Attaches to words of virtually any category (prepositions, verbs, adjectives, adverbs). Characteristic of simple clitics.

• singleCategory : SelectionDegree

  Attaches to words of a single major category (e.g., past tense -ed to verbs, plural -s to nouns). Characteristic of inflectional affixes.

• closedClass : SelectionDegree

  Attaches only to a closed list of stems (e.g., -n't only to finite auxiliaries). Maximally selective.

instance Core.Morphology.instDecidableEqSelectionDegree : DecidableEq SelectionDegree

Equations

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

instance Core.Morphology.instReprSelectionDegree : Repr SelectionDegree

Equations

• Core.Morphology.instReprSelectionDegree = { reprPrec := Core.Morphology.instReprSelectionDegree.repr }

def Core.Morphology.instReprSelectionDegree.repr : SelectionDegree → Nat → Std.Format

Equations

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

def Core.Morphology.instBEqSelectionDegree.beq : SelectionDegree → SelectionDegree → Bool

Equations

• Core.Morphology.instBEqSelectionDegree.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Morphology.instBEqSelectionDegree : BEq SelectionDegree

Equations

• Core.Morphology.instBEqSelectionDegree = { beq := Core.Morphology.instBEqSelectionDegree.beq }

def Core.Morphology.SelectionDegree.isHighSelection : SelectionDegree → Bool

Affixes are more selective than clitics.

Equations

• Core.Morphology.SelectionDegree.low.isHighSelection = false
• Core.Morphology.SelectionDegree.singleCategory.isHighSelection = true
• Core.Morphology.SelectionDegree.closedClass.isHighSelection = true

inductive Core.Morphology.MorphStatus : Type

Morphological status of a linguistic form.

Classifies forms by their degree of syntactic independence and mode of combination. The clitic–affix boundary is the central question of @cite{zwicky-pullum-1983}: the criteria A–F serve to locate a given morpheme on this scale.

• freeWord : MorphStatus

  Syntactically independent word.

• simpleClitic : MorphStatus

  Simple clitic: phonologically reduced variant of a free word, occurring in the same syntactic positions. English contracted auxiliaries 's, 've, 'd.

• specialClitic : MorphStatus

  Special clitic: either no corresponding free word exists, or the distribution differs from the free word. Romance pronominal clitics, Latin -que.

• inflAffix : MorphStatus

  Inflectional affix: paradigmatic, category-preserving, highly selective, with possible gaps and idiosyncrasies. English -ed, -s, -est, -n't.

• derivAffix : MorphStatus

  Derivational affix: potentially category-changing, often productive but may show lexical restrictions. English -ness, un-, -ize.

instance Core.Morphology.instDecidableEqMorphStatus : DecidableEq MorphStatus

Equations

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

instance Core.Morphology.instReprMorphStatus : Repr MorphStatus

Equations

• Core.Morphology.instReprMorphStatus = { reprPrec := Core.Morphology.instReprMorphStatus.repr }

def Core.Morphology.instReprMorphStatus.repr : MorphStatus → Nat → Std.Format

Equations

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

instance Core.Morphology.instBEqMorphStatus : BEq MorphStatus

Equations

• Core.Morphology.instBEqMorphStatus = { beq := Core.Morphology.instBEqMorphStatus.beq }

def Core.Morphology.instBEqMorphStatus.beq : MorphStatus → MorphStatus → Bool

Equations

• Core.Morphology.instBEqMorphStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Morphology.MorphStatus.isBound : MorphStatus → Bool

Is this form bound (i.e., not a free word)?

Equations

• Core.Morphology.MorphStatus.freeWord.isBound = false
• x✝.isBound = true

def Core.Morphology.MorphStatus.isAffix : MorphStatus → Bool

Is this an affix (inflectional or derivational)?

Equations

• Core.Morphology.MorphStatus.inflAffix.isAffix = true
• Core.Morphology.MorphStatus.derivAffix.isAffix = true
• x✝.isAffix = false

def Core.Morphology.MorphStatus.isClitic : MorphStatus → Bool

Is this a clitic (simple or special)?

Equations

• Core.Morphology.MorphStatus.simpleClitic.isClitic = true
• Core.Morphology.MorphStatus.specialClitic.isClitic = true
• x✝.isClitic = false

structure Core.Morphology.ParadigmCell (F : Type) : Type

A single cell in a morphological paradigm: one form of a lexeme in a particular morphosyntactic context.

The type parameter F is the feature bundle type (e.g., UD.MorphFeatures for a full UD specification, or a simpler domain-specific type).

• features : F

  The morphosyntactic features selecting this cell.

• form : Option String

  The surface form, or none for a paradigm gap.

• regular : Bool

  Is this form predictable from the stem by regular rule?

def Core.Morphology.instReprParadigmCell.repr {F✝ : Type} [Repr F✝] : ParadigmCell F✝ → Nat → Std.Format

Equations

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

instance Core.Morphology.instReprParadigmCell {F✝ : Type} [Repr F✝] : Repr (ParadigmCell F✝)

Equations

• Core.Morphology.instReprParadigmCell = { reprPrec := Core.Morphology.instReprParadigmCell.repr }

instance Core.Morphology.instBEqParadigmCell {F✝ : Type} [BEq F✝] : BEq (ParadigmCell F✝)

Equations

• Core.Morphology.instBEqParadigmCell = { beq := Core.Morphology.instBEqParadigmCell.beq }

def Core.Morphology.instBEqParadigmCell.beq {F✝ : Type} [BEq F✝] : ParadigmCell F✝ → ParadigmCell F✝ → Bool

Equations

• Core.Morphology.instBEqParadigmCell.beq { features := a, form := a_1, regular := a_2 } { features := b, form := b_1, regular := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Core.Morphology.instBEqParadigmCell.beq x✝¹ x✝ = false

def Core.Morphology.ParadigmCell.isGap {F : Type} (c : ParadigmCell F) : Bool

Does this cell represent a paradigm gap?

Equations

• c.isGap = c.form.isNone

def Core.Morphology.ParadigmCell.isIrregular {F : Type} (c : ParadigmCell F) : Bool

Does this cell show irregularity (suppletion or unpredictable allomorphy)?

Equations

• c.isIrregular = (!c.regular && c.form.isSome)

inductive Core.Morphology.MorphCategory : Type

Morpheme functional category.

Categories are ordered by semantic relevance to the verb stem: more relevant categories appear closer to the stem in suffixal morphology.

• stem : MorphCategory
• derivation : MorphCategory
• valence : MorphCategory
• voice : MorphCategory
• aspect : MorphCategory
• tense : MorphCategory
• mood : MorphCategory
• negation : MorphCategory
• agreement : MorphCategory
• nonfinite : MorphCategory
• number : MorphCategory
• degree : MorphCategory

instance Core.Morphology.instReprMorphCategory : Repr MorphCategory

Equations

• Core.Morphology.instReprMorphCategory = { reprPrec := Core.Morphology.instReprMorphCategory.repr }

def Core.Morphology.instReprMorphCategory.repr : MorphCategory → Nat → Std.Format

Equations

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

instance Core.Morphology.instDecidableEqMorphCategory : DecidableEq MorphCategory

Equations

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

instance Core.Morphology.instBEqMorphCategory : BEq MorphCategory

Equations

• Core.Morphology.instBEqMorphCategory = { beq := Core.Morphology.instBEqMorphCategory.beq }

def Core.Morphology.instBEqMorphCategory.beq : MorphCategory → MorphCategory → Bool

Equations

• Core.Morphology.instBEqMorphCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Morphology.MorphCategory.relevanceRank : MorphCategory → Nat

Relevance rank: lower = closer to the stem.

Stem = 0 (most relevant to verb meaning). Derivation = 1 (changes verb category). ... Agreement = 8 (least relevant to verb meaning).

number on nouns is ranked 3 (same as voice): it changes the noun's denotation via @cite{link-1983}, unlike verb agreement which is semantically vacuous.

degree on adjectives is ranked 5 (same as tense on verbs): comparative/superlative morphology compositionally modifies the adjective's interpretation, analogous to how tense modifies the verb's temporal reference.

Equations

• Core.Morphology.MorphCategory.stem.relevanceRank = 0
• Core.Morphology.MorphCategory.derivation.relevanceRank = 1
• Core.Morphology.MorphCategory.valence.relevanceRank = 2
• Core.Morphology.MorphCategory.number.relevanceRank = 3
• Core.Morphology.MorphCategory.voice.relevanceRank = 3
• Core.Morphology.MorphCategory.aspect.relevanceRank = 4
• Core.Morphology.MorphCategory.degree.relevanceRank = 5
• Core.Morphology.MorphCategory.tense.relevanceRank = 5
• Core.Morphology.MorphCategory.mood.relevanceRank = 6
• Core.Morphology.MorphCategory.negation.relevanceRank = 7
• Core.Morphology.MorphCategory.agreement.relevanceRank = 8
• Core.Morphology.MorphCategory.nonfinite.relevanceRank = 9

def Core.Morphology.respectsRelevanceHierarchy (slots : List MorphCategory) : Bool

A morpheme ordering respects the relevance hierarchy if ranks are non-decreasing from stem outward.

Equations

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

structure Core.Morphology.MorphRule (σ : Type) : Type

A morphological rule: carries formal AND semantic effects.

The type parameter σ is the meaning type, so this works uniformly across Bool/Frac/Float semantic backends.

Design principle: semEffect can be id for semantically vacuous morphology (e.g., verb agreement -s), making it explicit which inflections carry semantic content and which don't.

• category : MorphCategory

  Which morphological category this rule realizes

• value : String

  The feature value this rule realizes

• formRule : String → String

  How the surface form changes

• featureRule : Features → Features

  How morphosyntactic features change

• semEffect : σ → σ

  Semantic effect (identity if semantically vacuous)

• isVacuous : Bool

  Is this rule semantically vacuous? (agreement, etc.)

structure Core.Morphology.Stem (σ : Type) : Type

A lexical stem: a root meaning plus its morphological paradigm.

• lemma_ : String

  Base form (lemma)

• cat : UD.UPOS

  Syntactic category

• baseFeatures : Features

  Base morphosyntactic features

• paradigm : List (MorphRule σ)

  Available inflectional rules

def Core.Morphology.Stem.inflect {σ : Type} (s : Stem σ) (rule : MorphRule σ) (baseMeaning : σ) : String × Features × σ

Apply a morphological rule to generate an inflected form + meaning.

Equations

• s.inflect rule baseMeaning = (rule.formRule s.lemma_, rule.featureRule s.baseFeatures, rule.semEffect baseMeaning)

def Core.Morphology.Stem.allForms {σ : Type} (s : Stem σ) (baseMeaning : σ) : List (String × Features × σ)

Generate all forms in the paradigm (base + inflected).

Equations

• s.allForms baseMeaning = (s.lemma_, s.baseFeatures, baseMeaning) :: List.map (fun (x : Core.Morphology.MorphRule σ) => s.inflect x baseMeaning) s.paradigm

structure Core.Morphology.InflDistribution : Type

Distribution of inflectional categories between two elements of a periphrastic construction (e.g., auxiliary and lexical verb in an AVC). @cite{anderson-2006} @cite{bybee-1985}

In an aux-headed AVC, onLex is minimal (stem only or empty). In a lex-headed AVC, onAux is empty. In a split AVC, onAux and onLex host different category types. In a doubled AVC, onAux and onLex overlap.

• onAux : List MorphCategory
• onLex : List MorphCategory

instance Core.Morphology.instReprInflDistribution : Repr InflDistribution

Equations

• Core.Morphology.instReprInflDistribution = { reprPrec := Core.Morphology.instReprInflDistribution.repr }

def Core.Morphology.instReprInflDistribution.repr : InflDistribution → Nat → Std.Format

Equations

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

instance Core.Morphology.instBEqInflDistribution : BEq InflDistribution

Equations

• Core.Morphology.instBEqInflDistribution = { beq := Core.Morphology.instBEqInflDistribution.beq }

def Core.Morphology.instBEqInflDistribution.beq : InflDistribution → InflDistribution → Bool

Equations

• Core.Morphology.instBEqInflDistribution.beq { onAux := a, onLex := a_1 } { onAux := b, onLex := b_1 } = (a == b && a_1 == b_1)
• Core.Morphology.instBEqInflDistribution.beq x✝¹ x✝ = false

def Core.Morphology.instDecidableEqInflDistribution.decEq (x✝ x✝¹ : InflDistribution) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.Morphology.instDecidableEqInflDistribution : DecidableEq InflDistribution

Equations

• Core.Morphology.instDecidableEqInflDistribution = Core.Morphology.instDecidableEqInflDistribution.decEq