Lexical Rules for Word Grammar @cite{hudson-2010}

Lexical rules derive new lexical entries from existing ones, following Word Grammar and HPSG @cite{pollard-sag-1994}. The two rules formalised here are central to the @cite{hudson-2010} treatment of English auxiliaries (also discussed in @cite{gibson-2025}):

1. Auxiliary Inversion: V+aux → V+aux,+inv (subject moves from left to right — Hudson treats this as a word-class subtype, not a movement rule; see WordGrammar.Network.englishAuxNet's inverted_auxiliary node).
2. Passive: VN → V+passive (object promoted, subject demoted to by-phrase).

A third rule — Dative Alternation — is mentioned in the literature but not formalised here.

structure WordGrammar.LexEntry : Type

A lexical entry: word form + category + features + argument structure. Uses the shared Features bundle from Core/Basic.lean. The inv field is DG-specific (auxiliary inversion state).

• form : String
• cat : UD.UPOS
• features : Features
• argStr : DepGrammar.ArgStr
• inv : Bool

def WordGrammar.instReprLexEntry.repr : LexEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WordGrammar.instReprLexEntry : Repr LexEntry

Equations

• WordGrammar.instReprLexEntry = { reprPrec := WordGrammar.instReprLexEntry.repr }

def WordGrammar.argStr_Aux : DepGrammar.ArgStr

Auxiliary verb (non-inverted): subject left, main verb right

Equations

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

def WordGrammar.argStr_AuxInv : DepGrammar.ArgStr

Auxiliary verb (inverted): subject right, main verb right

Equations

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

structure WordGrammar.LexRule : Type

A lexical rule transforms one lexical entry into another

• name : String
• applies : LexEntry → Bool

  Condition for the rule to apply

• transform : LexEntry → LexEntry

  Transform the entry

def WordGrammar.auxInversionRule : LexRule

Auxiliary Inversion Rule: V+aux,-inv → V+aux,+inv The subject moves from left to right position

Equations

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

def WordGrammar.passiveRule : LexRule

Passive Rule: VN → V+passive Object is removed (promoted to subject), by-phrase added as optional

Equations

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

def WordGrammar.applyRule (rule : LexRule) (entry : LexEntry) : Option LexEntry

Apply a lexical rule if it matches

Equations

• WordGrammar.applyRule rule entry = if rule.applies entry = true then some (rule.transform entry) else none

def WordGrammar.deriveEntries (rules : List LexRule) (entry : LexEntry) : List LexEntry

Apply all applicable rules to generate derived entries

Equations

• WordGrammar.deriveEntries rules entry = entry :: List.filterMap (fun (x : WordGrammar.LexRule) => WordGrammar.applyRule x entry) rules