Word — the morphosyntactic word (ms-word) token

[KBC+26]

The surface token: the unit that (morpho)syntax treats as a word. Wordhood minimally splits into the ms-word (this type) and the p-word (the prosodic word, Phonology/Prosodic/Word.lean) — the "one area of robust consensus" on the wordhood problem ([KBC+26] §3.2); we follow the Element in calling ms-words simply words. The split is descriptive, not a Lexicalist commitment: ms-words are "crucial for lexicalist theories" but used descriptively by non-lexicalist ones too (§3.2.1, §3.3), and this token carries no theory of how words are formed.

Word completes Morphology's word inventory: MorphWord is word-internal structure, MorphRule/Stem are word-forming processes, Word is the resulting token — form + UD category + one UD.MorphFeatures bundle, i.e. a CoNLL-U row. The ms- vs p-boundness typology relating the two word notions ([KBC+26] Table 3) is formalized in Studies/KalinBjorkmanEtAl2026.lean.

Main declarations

• Word — the token, with its admission rule (see the declaration docstring).
• Word.phi — the φ-feature projection (person/number/gender).
• Word.Agree — φ-agreement: a reflexive, symmetric, non-transitive tolerance relation.
• Word.asPassive — passive variant (voice morphology only; valence effects are DepTree.frames-level facts).

structure Word : Type

A word: the pure CoNLL-U surface token — surface form, UD category, and UD morphology (one UD.MorphFeatures bundle; there is no separate word-level feature record).

Admission rule: a property belongs on Word iff a Fragment-free token-level engine reads it off the token's own data; otherwise it lives on the typed lexical carrier (Pronoun, NounEntry, Verb, …) or on the consuming framework's own structures (e.g. DG subcategorization premises live on DepTree.frames, not here). Identity caveat: BEq is form + category, so homographs collapse; a CoNLL-U lemma field is the known fix, deferred until a consumer needs it.

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

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

Equations

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

@[implicit_reducible]

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.phi (w : Word) : UD.MorphFeatures

The φ-feature subset (person, number, gender) of a word, as a UD.MorphFeatures bundle.

Equations

• w.phi = { number := w.features.number, gender := w.features.gender, person := w.features.person }

def Word.Agree (w1 w2 : Word) : Prop

φ-agreement between two words: their person/number/gender features are compatible (an unspecified feature is a wildcard). A reflexive, symmetric tolerance relation on Word (not transitive), decided by the shared UD.MorphFeatures.compatible. This is the feature-based agreement primitive binding and concord consumers share — no surface-form gender lookup.

Equations

• w1.Agree w2 = (w1.phi.compatible w2.phi = true)

@[implicit_reducible]

instance instDecidableAgree (w1 w2 : Word) : Decidable (w1.Agree w2)

Equations

• instDecidableAgree w1 w2 = id inferInstance

theorem Word.Agree.refl (w : Word) : w.Agree w

theorem Word.Agree.symm {w1 w2 : Word} (h : w1.Agree w2) : w2.Agree w1

φ-agreement is symmetric — the docstring's "symmetric tolerance relation", as a theorem.

theorem Word.Agree.not_transitive : ¬∀ (w1 w2 w3 : Word), w1.Agree w2 → w2.Agree w3 → w1.Agree w3

φ-agreement is not transitive: an unspecified feature is a wildcard, so underspecified they agrees with both she and he while she ≁ he.

@[implicit_reducible]

instance instHasNumberWord : HasNumber Word

A word bears the number its UD morphology ingests (Number.fromUD).

Equations

• instHasNumberWord = { numberOf := fun (w : Word) => w.features.number.bind Number.fromUD }

@[implicit_reducible]

instance instHasPersonWord : HasPerson Word

Equations

• instHasPersonWord = { personOf := fun (w : Word) => Option.map Person.fromUD w.features.person }

@[implicit_reducible]

instance instHasCaseWord : HasCase Word

Equations

• instHasCaseWord = { caseOf := fun (w : Word) => Option.map Case.fromUD w.features.case_ }

@[simp]

theorem Word.numberOf_phi (w : Word) : HasNumber.numberOf w.phi = HasNumber.numberOf w

The φ-projection preserves numberOf: a word and its phi bundle bear the same number — the defeq Word.Agree.hasNumber_compatible relies on.

theorem Word.Agree.hasNumber_compatible {w1 w2 : Word} (h : w1.Agree w2) : HasNumber.Compatible w1 w2

φ-agreement entails number compatibility: the HasNumber mixin never diverges from the agreement engine on Word.

def Word.asPassive (w : Word) : Word

Derive a passive variant: sets voice to passive. The valence change (detransitivization) is a frame-level fact carried by the passive analysis on DepTree.frames, not token data. Composes with VerbEntry.toWordPastPart.

Equations

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

@[implicit_reducible]

instance instBEqWord : BEq Word

Equations

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

@[implicit_reducible]

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)