Word

@cite{biberauer-roberts-2014} @cite{dryer-1992}

The lexical unit and its building blocks: morphological feature types (aliased to Universal Dependencies), the Features bundle, and the Word structure.

Universal Dependencies Integration

Morphological features are aliased to UD types:

• Number = UD.Number (with compatibility constructors sg, pl)
• Person = UD.Person (with compatibility constructors first, second, third)
• Case = UD.Case (with compatibility constructors nom, acc, gen)
• Voice = UD.Voice (with compatibility constructors active, passive)
• VForm = UD.VerbForm (with compatibility constructors)

Syntactic categories use UD.UPOS directly (the 17 universal POS tags).

Types without UD equivalents remain defined here:

• Valence (argument structure)
• HeadDirection (word-order typology)

@[reducible, inline]

abbrev Number : Type

Grammatical number. Aliased to UD.Number for cross-linguistic compatibility.

Equations

• Number = UD.Number

@[reducible, match_pattern, inline]

abbrev Number.sg : Number

Singular (compatibility alias for UD.Number.Sing)

Equations

• Number.sg = UD.Number.Sing

@[reducible, match_pattern, inline]

abbrev Number.pl : Number

Plural (compatibility alias for UD.Number.Plur)

Equations

• Number.pl = UD.Number.Plur

@[reducible, inline]

abbrev Person : Type

Grammatical person. Aliased to UD.Person for cross-linguistic compatibility.

Constructors are: .first, .second, .third, .zero (no compatibility aliases needed - names match)

Equations

• Person = UD.Person

@[reducible, inline]

abbrev Case : Type

Grammatical case. Aliased to UD.Case for cross-linguistic compatibility.

Equations

• Case = UD.Case

@[reducible, inline]

abbrev Case.nom : Case

Nominative (compatibility alias)

Equations

• Case.nom = UD.Case.Nom

@[reducible, inline]

abbrev Case.acc : Case

Accusative (compatibility alias)

Equations

• Case.acc = UD.Case.Acc

@[reducible, inline]

abbrev Case.gen : Case

Genitive (compatibility alias)

Equations

• Case.gen = UD.Case.Gen

@[reducible, inline]

abbrev Voice : Type

Voice: active vs passive. Aliased to UD.Voice.

Equations

• Voice = UD.Voice

@[reducible, inline]

abbrev Voice.active : Voice

Active voice (compatibility alias)

Equations

• Voice.active = UD.Voice.Act

@[reducible, inline]

abbrev Voice.passive : Voice

Passive voice (compatibility alias)

Equations

• Voice.passive = UD.Voice.Pass

@[reducible, inline]

abbrev VForm : Type

Verb form. Aliased to UD.VerbForm.

Equations

• VForm = UD.VerbForm

@[reducible, inline]

abbrev VForm.finite : VForm

Finite (compatibility alias)

Equations

• VForm.finite = UD.VerbForm.Fin

@[reducible, inline]

abbrev VForm.infinitive : VForm

Infinitive (compatibility alias)

Equations

• VForm.infinitive = UD.VerbForm.Inf

@[reducible, inline]

abbrev VForm.pastParticiple : VForm

Past participle (compatibility alias - maps to Part)

Equations

• VForm.pastParticiple = UD.VerbForm.Part

@[reducible, inline]

abbrev VForm.presParticiple : VForm

Present participle (compatibility alias - maps to Part)

Equations

• VForm.presParticiple = UD.VerbForm.Part

@[reducible, inline]

abbrev Tense : Type

Tense. Aliased to UD.Tense.

Equations

• Tense = UD.Tense

@[reducible, inline]

abbrev Tense.past : Tense

Past tense (compatibility alias)

Equations

• Tense.past = UD.Tense.Past

@[reducible, inline]

abbrev Tense.present : Tense

Present tense (compatibility alias)

Equations

• Tense.present = UD.Tense.Pres

@[reducible, inline]

abbrev Tense.future : Tense

Future tense (compatibility alias)

Equations

• Tense.future = UD.Tense.Fut

inductive MassCount : Type

Morphosyntactic mass/count feature. No direct UD equivalent.

A formal feature parallel to grammatical gender — not an ontological distinction. Determines kind-anaphor morphology: [MASS] → it, [COUNT] → they. Evidence: pollen[MASS] → it vs pollen grains[COUNT] → they for the same referent (@cite{krifka-2026} §2).

• mass : MassCount
• count : MassCount

def instReprMassCount.repr : MassCount → Nat → Std.Format

Equations

• instReprMassCount.repr MassCount.mass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MassCount.mass")).group prec✝
• instReprMassCount.repr MassCount.count prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MassCount.count")).group prec✝

instance instReprMassCount : Repr MassCount

Equations

• instReprMassCount = { reprPrec := instReprMassCount.repr }

instance instDecidableEqMassCount : DecidableEq MassCount

Equations

• instDecidableEqMassCount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqMassCount : BEq MassCount

Equations

• instBEqMassCount = { beq := instBEqMassCount.beq }

def instBEqMassCount.beq : MassCount → MassCount → Bool

Equations

• instBEqMassCount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def instHashableMassCount.hash : MassCount → UInt64

Equations

• instHashableMassCount.hash MassCount.mass = 0
• instHashableMassCount.hash MassCount.count = 1

instance instHashableMassCount : Hashable MassCount

Equations

• instHashableMassCount = { hash := instHashableMassCount.hash }

inductive Valence : Type

Transitivity / argument structure. No direct UD equivalent.

• intransitive : Valence
• transitive : Valence
• ditransitive : Valence
• dative : Valence
• locative : Valence
• copular : Valence
• clausal : Valence

def instReprValence.repr : Valence → Nat → Std.Format

Equations

• instReprValence.repr Valence.intransitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.intransitive")).group prec✝
• instReprValence.repr Valence.transitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.transitive")).group prec✝
• instReprValence.repr Valence.ditransitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.ditransitive")).group prec✝
• instReprValence.repr Valence.dative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.dative")).group prec✝
• instReprValence.repr Valence.locative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.locative")).group prec✝
• instReprValence.repr Valence.copular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.copular")).group prec✝
• instReprValence.repr Valence.clausal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Valence.clausal")).group prec✝

instance instReprValence : Repr Valence

Equations

• instReprValence = { reprPrec := instReprValence.repr }

instance instDecidableEqValence : DecidableEq Valence

Equations

• instDecidableEqValence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instInhabitedValence.default : Valence

Equations

• instInhabitedValence.default = Valence.intransitive

instance instInhabitedValence : Inhabited Valence

Equations

• instInhabitedValence = { default := instInhabitedValence.default }

inductive HeadDirection : Type

Head direction of a syntactic construction. Used for word-order typology and constraints like FOFC.

• headInitial : HeadDirection
• headFinal : HeadDirection

def instReprHeadDirection.repr : HeadDirection → Nat → Std.Format

Equations

• instReprHeadDirection.repr HeadDirection.headInitial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeadDirection.headInitial")).group prec✝
• instReprHeadDirection.repr HeadDirection.headFinal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeadDirection.headFinal")).group prec✝

instance instReprHeadDirection : Repr HeadDirection

Equations

• instReprHeadDirection = { reprPrec := instReprHeadDirection.repr }

instance instDecidableEqHeadDirection : DecidableEq HeadDirection

Equations

• instDecidableEqHeadDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqHeadDirection : BEq HeadDirection

Equations

• instBEqHeadDirection = { beq := instBEqHeadDirection.beq }

def instBEqHeadDirection.beq : HeadDirection → HeadDirection → Bool

Equations

• instBEqHeadDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Features : Type

Feature bundle for words. Uses aliased UD types.

• wh : Bool
• finite : Bool
• number : Option Number
• person : Option Person
• case_ : Option Case
• valence : Option Valence
• voice : Option Voice
• vform : Option VForm
• tense : Option Tense
• countable : Option MassCount

def instReprFeatures.repr : Features → Nat → Std.Format

Equations

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

instance instReprFeatures : Repr Features

Equations

• instReprFeatures = { reprPrec := instReprFeatures.repr }

instance instDecidableEqFeatures : DecidableEq Features

Equations

• instDecidableEqFeatures = instDecidableEqFeatures.decEq

def instDecidableEqFeatures.decEq (x✝ x✝¹ : Features) : Decidable (x✝ = x✝¹)

Equations

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

structure Word : Type

A word: form + category + features.

• form : String
• cat : UD.UPOS
• features : Features

def instReprWord.repr : Word → Nat → Std.Format

Equations

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

instance instReprWord : Repr Word

Equations

• instReprWord = { reprPrec := instReprWord.repr }

def Word.mk' (form : String) (cat : UD.UPOS) : Word

Convenience constructor for a featureless word (form + category only).

Equations

• Word.mk' form cat = { form := form, cat := cat }

def Word.asPassive (w : Word) : Word

Derive a passive variant: sets voice to passive, valence to intransitive. Used to compose with VerbEntry.toWordPastPart for passive constructions.

Equations

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

instance instBEqWord : BEq Word

Equations

• instBEqWord = { beq := fun (w1 w2 : Word) => w1.form == w2.form && w1.cat == w2.cat }

instance instToStringWord : ToString Word

Equations

• instToStringWord = { toString := fun (w : Word) => w.form }

def wordsToString (ws : List Word) : String

Convert a word list to a readable string.

Equations

• wordsToString ws = " ".intercalate (List.map (fun (x : Word) => x.form) ws)