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 word-level semantic contribution is delegated to a higher composition layer (e.g., tense rules that delegate to Theories/Semantics/Tense/, agreement rules that contribute no truth-conditional meaning) carry delegatedSemantics := true. The Bool flag is not a claim that the morpheme is meaningless — Bybee 1985 Ch 1 §3 explicitly argues against the vacuity-of-inflection position. It tracks where the meaning is computed (delegate to Theory layer vs. compute at the morphological word level), not whether meaning exists.

inductive Core.Morphology.AttachmentSide : Type

Side on which a bound morpheme attaches to its host.

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

@[implicit_reducible]

instance Core.Morphology.instDecidableEqAttachmentSide : DecidableEq AttachmentSide

Equations

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

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

Equations

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

@[implicit_reducible]

instance Core.Morphology.instReprAttachmentSide : Repr AttachmentSide

Equations

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

inductive Core.Morphology.FormativePosition : Type

Typological position classification for formatives. @cite{bickel-nichols-2001} Table 2.

Superset of AttachmentSide: adds simulfixation (process morphology), detached formatives (Wackernagel clitics, free auxiliaries), and endoclisis (clitic insertion inside a word).

• praefixed : FormativePosition
• postfixed : FormativePosition
• infixed : FormativePosition
• circumfixed : FormativePosition
• simultaneous : FormativePosition
• detached : FormativePosition
• endoclitic : FormativePosition

@[implicit_reducible]

instance Core.Morphology.instDecidableEqFormativePosition : DecidableEq FormativePosition

Equations

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

@[implicit_reducible]

instance Core.Morphology.instReprFormativePosition : Repr FormativePosition

Equations

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

def Core.Morphology.instReprFormativePosition.repr : FormativePosition → ℕ → Std.Format

Equations

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

def Core.Morphology.AttachmentSide.toFormativePosition : AttachmentSide → FormativePosition

Map AttachmentSide to the richer FormativePosition classification.

Equations

• Core.Morphology.AttachmentSide.prefix.toFormativePosition = Core.Morphology.FormativePosition.praefixed
• Core.Morphology.AttachmentSide.suffix.toFormativePosition = Core.Morphology.FormativePosition.postfixed
• Core.Morphology.AttachmentSide.infix.toFormativePosition = Core.Morphology.FormativePosition.infixed
• Core.Morphology.AttachmentSide.circumfix.toFormativePosition = Core.Morphology.FormativePosition.circumfixed

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.

@[implicit_reducible]

instance Core.Morphology.instDecidableEqSelectionDegree : DecidableEq SelectionDegree

Equations

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

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

Equations

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

@[implicit_reducible]

instance Core.Morphology.instReprSelectionDegree : Repr SelectionDegree

Equations

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

def Core.Morphology.SelectionDegree.IsHighSelection (s : SelectionDegree) : Prop

Affixes are more selective than clitics.

Equations

• s.IsHighSelection = (s ≠ Core.Morphology.SelectionDegree.low)

@[implicit_reducible]

instance Core.Morphology.instDecidablePredSelectionDegreeIsHighSelection : DecidablePred SelectionDegree.IsHighSelection

Equations

• Core.Morphology.instDecidablePredSelectionDegreeIsHighSelection s = id inferInstance

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 bound form that can attach to hosts of virtually any syntactic category. @cite{bickel-nichols-2001}: defined primarily by low selectivity (categorical freedom) + phonological dependence, not necessarily by being a reduced variant of a free word. Many simple clitics have no free-word counterpart (Latin -que). English contracted auxiliaries ('s, 've, 'd) are a subcase where a free variant exists.

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

@[implicit_reducible]

instance Core.Morphology.instDecidableEqMorphStatus : DecidableEq MorphStatus

Equations

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

@[implicit_reducible]

instance Core.Morphology.instReprMorphStatus : Repr MorphStatus

Equations

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

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

Equations

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

def Core.Morphology.MorphStatus.IsAffix (s : MorphStatus) : Prop

Is this an affix (inflectional or derivational)?

Equations

• s.IsAffix = (s = Core.Morphology.MorphStatus.inflAffix ∨ s = Core.Morphology.MorphStatus.derivAffix)

@[implicit_reducible]

instance Core.Morphology.instDecidablePredMorphStatusIsAffix : DecidablePred MorphStatus.IsAffix

Equations

• Core.Morphology.instDecidablePredMorphStatusIsAffix x✝ = Core.Morphology.instDecidablePredMorphStatusIsAffix._aux_1 x✝

def Core.Morphology.MorphStatus.IsClitic (s : MorphStatus) : Prop

Is this a clitic (simple or special)?

Equations

• s.IsClitic = (s = Core.Morphology.MorphStatus.simpleClitic ∨ s = Core.Morphology.MorphStatus.specialClitic)

@[implicit_reducible]

instance Core.Morphology.instDecidablePredMorphStatusIsClitic : DecidablePred MorphStatus.IsClitic

Equations

• Core.Morphology.instDecidablePredMorphStatusIsClitic x✝ = Core.Morphology.instDecidablePredMorphStatusIsClitic._aux_1 x✝

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?

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

@[implicit_reducible]

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

Equations

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

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

Does this cell represent a paradigm gap?

Equations

• c.isGap = (c.form = none)

@[implicit_reducible]

instance Core.Morphology.instDecidableIsGap {F : Type} (c : ParadigmCell F) : Decidable c.isGap

Equations

• Core.Morphology.instDecidableIsGap c = Core.Morphology.instDecidableIsGap._aux_1 c

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

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

Equations

• c.isIrregular = (c.regular = false ∧ c.form ≠ none)

@[implicit_reducible]

instance Core.Morphology.instDecidableIsIrregular {F : Type} (c : ParadigmCell F) : Decidable c.isIrregular

Equations

• Core.Morphology.instDecidableIsIrregular c = Core.Morphology.instDecidableIsIrregular._aux_1 c

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 (controller : Agreement.Controller) : MorphCategory

  Agreement morphology, parameterized by the grammatical role of the controlling NP (Core.Agreement.Controller). The role distinction (subj vs obj vs poss vs ...) is what allows Anderson Ch 5 §5.2 split/doubled AVC typology to be Lean-checkable; Bybee 1985's personAgr / personAgrObj / genderAgr source distinctions also round-trip cleanly. See scratch/morphcategory_agreement_split_plan.md for the design rationale (0.230.578-0.230.584).

• nonfinite : MorphCategory
• number : MorphCategory
• degree : MorphCategory

@[implicit_reducible]

instance Core.Morphology.instReprMorphCategory : Repr MorphCategory

Equations

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

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

Equations

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

def Core.Morphology.instDecidableEqMorphCategory.decEq (x✝ x✝¹ : MorphCategory) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.Morphology.instDecidableEqMorphCategory : DecidableEq MorphCategory

Equations

• Core.Morphology.instDecidableEqMorphCategory = Core.Morphology.instDecidableEqMorphCategory.decEq

def Core.Morphology.MorphCategory.IsAgreement : MorphCategory → Bool

Predicate testing whether a MorphCategory is an agreement category, independent of which Controller role parameterizes it. Used for Bybee-style relevance-hierarchy code that doesn't care which role triggers the agreement, only that agreement IS the category.

Equations

• (Core.Morphology.MorphCategory.agreement controller).IsAgreement = true
• x✝.IsAgreement = false

def Core.Morphology.MorphCategory.peripherality : MorphCategory → ℕ

Peripherality: numerical embedding of Bybee's relevance hierarchy where higher = farther from stem = less semantically relevant.

In Bybee's text, "high relevance" means more semantically integrated with the stem (@cite{bybee-1985} Ch 2 §2.1 p. 13). The substrate uses the opposite numerical direction: stem = 0 (most relevant), agreement = 8 (least relevant), so that Nat ordering mirrors stem-outward linear position in suffixing morphology (Ch 2 §6 iconicity, p. 33). The field name peripherality makes this directionality explicit and avoids the wrong-on-its-face gloss "high relevance rank means low relevance."

Categories from Bybee 1985 Ch 2 §3 (verified against the book): valence, voice, aspect, tense, mood, agreement.

Linglib extensions (NOT in Bybee 1985 — flag in any consumer that reads these ranks):

• derivation (rank 1): Bybee Ch 4 argues lex/deriv/infl is a continuum, not a discrete level on the relevance scale.
• number (rank 3): Bybee discusses verbal-number agreement at the low end (with person agreement). Noun number is treated separately (Ch 2 §6 cites Greenberg 1963 only, "stem < number < case" for nouns). Cross-comparison of noun-number rank with verb-aspect rank is an artifact of unifying both onto one scale.
• degree (rank 5): Bybee never discusses adjectival degree morphology. Comparative morphology is often derivational cross-linguistically (Stassen WALS).
• negation (rank 7): Bybee discusses negation as a kind of mood (Part II Ch 8 §5), not a separate level. Rank 7 is plausible per Miestamo 2005 cross-linguistic ordering data, but is a linglib extension.
• nonfinite (rank 9): not on Bybee's hierarchy at all (nonfinite morphology often changes syntactic category, outside the scope of inflectional categories proper).

Equations

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

def Core.Morphology.RespectsRelevanceHierarchy (slots : List MorphCategory) : Prop

A morpheme ordering respects the relevance hierarchy if peripherality is non-decreasing from stem outward (stem-adjacent first).

Equations

• Core.Morphology.RespectsRelevanceHierarchy slots = List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) (List.map Core.Morphology.MorphCategory.peripherality slots)

@[implicit_reducible]

instance Core.Morphology.instDecidablePredListMorphCategoryRespectsRelevanceHierarchy : DecidablePred RespectsRelevanceHierarchy

Equations

• Core.Morphology.instDecidablePredListMorphCategoryRespectsRelevanceHierarchy x✝ = id inferInstance

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 rules whose word-level semantic contribution is delegated to a higher composition layer (verb agreement -s carries no truth-conditional meaning at the word level; tense rules delegate to the intensional layer), making it explicit which inflections compute meaning at the word level and which delegate.

• 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 (id when meaning is delegated to a higher layer)

• delegatedSemantics : Bool

  Is the word-level semantic contribution delegated to a higher composition layer? (Set true for agreement, tense, etc., where Theories/Semantics/{Tense,Aspect,Modality,Agreement}/ handle the meaning. NOT a claim that the morpheme is meaningless — see file docstring.)

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

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

Equations

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

@[implicit_reducible]

instance Core.Morphology.instReprInflDistribution : Repr InflDistribution

Equations

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

@[implicit_reducible]

instance Core.Morphology.instDecidableEqInflDistribution : DecidableEq InflDistribution

Equations

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

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

Equations

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