Auxiliary

An auxiliary is a closed-class function word of verbal predication: it carries tense, aspect, modality, or voice while a lexical verb carries the content (UD AUX). Modal auxiliaries additionally have meanings in the force–flavor space — must is necessity over epistemic, deontic or circumstantial backgrounds — and may sit at a marked register (shall).

This file provides the auxiliary as a lexical object: its form, its agreement and verb-form features, its modality, and its register. Per-language fragments supply the entries.

Main declarations

• Auxiliary — the lexical object.
• Auxiliary.toWord — the AUX word it spells out.
• Auxiliary.toModalItem, Auxiliary.modalFeature — its modality as a ModalItem, and as the uninterpretable modal feature of [zeijlstra-2007].

References

• [anderson-2006a], §1.2
• [zeijlstra-2007]

structure Auxiliary : Type

An auxiliary: form, agreement and verb-form features, modality (empty for non-modal auxiliaries), and register.

• form : String
• features : UD.MorphFeatures
• modality : List Modality.ForceFlavor

  The modality, as force–flavor pairs; empty for the non-modal auxiliaries.

• register : Features.Register.Level

def instDecidableEqAuxiliary.decEq (x✝ x✝¹ : Auxiliary) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqAuxiliary : DecidableEq Auxiliary

Equations

• instDecidableEqAuxiliary = instDecidableEqAuxiliary.decEq

def instReprAuxiliary.repr : Auxiliary → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprAuxiliary : Repr Auxiliary

Equations

• instReprAuxiliary = { reprPrec := instReprAuxiliary.repr }

def Auxiliary.toWord (a : Auxiliary) : Morphology.Word

The AUX word an auxiliary spells out.

Equations

• a.toWord = { form := a.form, cat := UD.UPOS.AUX, features := a.features }

@[simp]

theorem Auxiliary.toWord_cat (a : Auxiliary) : a.toWord.cat = UD.UPOS.AUX

def Auxiliary.tense (a : Auxiliary) : Option UD.Tense

Morphological tense; none for base forms such as can and will.

Equations

• a.tense = a.features.tense

def Auxiliary.person (a : Auxiliary) : Option UD.Person

Agreement person.

Equations

• a.person = a.features.person

def Auxiliary.number (a : Auxiliary) : Option UD.Number

Agreement number.

Equations

• a.number = a.features.number

def Auxiliary.toModalItem (a : Auxiliary) : Modality.ModalItem

The modal item an auxiliary contributes: form, meanings, register.

Equations

• a.toModalItem = { form := a.form, meaning := a.modality, register := a.register }

def Auxiliary.modalFeature (a : Auxiliary) : Option Modality.ModalFeature

The modal feature a modal auxiliary carries ([zeijlstra-2007]): the force of its primary meaning, uninterpretable — semantically vacuous and checked by a c-commanding interpretable operator. none for an auxiliary with no modality.

Equations

• a.modalFeature = Option.map (fun (ff : Modality.ForceFlavor) => { force := ff.force, interp := Modality.ModalInterpretability.uninterpretable }) a.modality.head?

def Auxiliary.interpretability (a : Auxiliary) : Option Modality.ModalInterpretability

The interpretability of the auxiliary's modal feature, if it has one.

Equations

• a.interpretability = Option.map (fun (x : Modality.ModalFeature) => x.interp) a.modalFeature

@[instance_reducible]

instance Auxiliary.instHasNumber : HasNumber Auxiliary

Equations

• Auxiliary.instHasNumber = { numberOf := fun (a : Auxiliary) => Option.bind a.features.number Number.fromUD }

@[instance_reducible]

instance Auxiliary.instHasPerson : HasPerson Auxiliary

Equations

• Auxiliary.instHasPerson = { personOf := fun (a : Auxiliary) => Option.map Person.fromUD a.features.person }