Documentation

Linglib.Phenomena.AuxiliaryVerbs.Typology

Auxiliary Verb Construction Typology #

@cite{anderson-2006}

Cross-linguistic classification of auxiliary verb constructions (AVCs) based on how inflection distributes between auxiliary and lexical verb. Anderson's core insight: the semantic head is always the lexical verb, but the inflectional host varies across 5 macro-patterns.

The Five Patterns #

Pattern	Infl Host	Example Language
Aux-headed	AUX	English will go
Lex-headed	LEX	Pipil weli ni-nehnemi wehka
Doubled	AUX+LEX	Gorum miŋ ne-gaʔ-ru ne-laʔ-ru
Split	AUX or LEX	Doyayo, Jakaltek, Finnish
Split/doubled	AUX+LEX (split)	(various)

Core types #

inductive Phenomena.AuxiliaryVerbs.Typology.InflPattern :

Anderson's 5-way inflectional pattern typology for AVCs.

auxHeaded : InflPattern
Inflection hosted on auxiliary; lexical verb is nonfinite. E.g., English will go, French va manger.
lexHeaded : InflPattern
Inflection hosted on lexical verb; auxiliary is grammaticalized. E.g., Pipil weli ni-nehnemi wehka (AUX uninflected, LV carries person).
doubled : InflPattern
Inflection appears on both auxiliary and lexical verb. E.g., Gorum miŋ ne-gaʔ-ru ne-laʔ-ru (subject + TAM on both).
split : InflPattern
Inflection split between AUX and LV (different features on each). E.g., Jakaltek šk-ach w-ila (absolutive on AUX, ergative on LV).
splitDoubled : InflPattern
Combination of split and doubled: different inflectional features appear on both AUX and LV, but neither hosts the same set. @cite{anderson-2006} discusses this as a logical possibility; clear exemplars are rare.

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instDecidableEqInflPattern :

DecidableEq InflPattern

Equations

Phenomena.AuxiliaryVerbs.Typology.instDecidableEqInflPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.AuxiliaryVerbs.Typology.instReprInflPattern :

Repr InflPattern

Equations

Phenomena.AuxiliaryVerbs.Typology.instReprInflPattern = { reprPrec := Phenomena.AuxiliaryVerbs.Typology.instReprInflPattern.repr }

def Phenomena.AuxiliaryVerbs.Typology.instReprInflPattern.repr :

InflPattern → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instBEqInflPattern :

BEq InflPattern

Equations

Phenomena.AuxiliaryVerbs.Typology.instBEqInflPattern = { beq := Phenomena.AuxiliaryVerbs.Typology.instBEqInflPattern.beq }

def Phenomena.AuxiliaryVerbs.Typology.instBEqInflPattern.beq :

InflPattern → InflPattern → Bool

Equations

Phenomena.AuxiliaryVerbs.Typology.instBEqInflPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.AuxiliaryVerbs.Typology.instInhabitedInflPattern.default :

Equations

Phenomena.AuxiliaryVerbs.Typology.instInhabitedInflPattern.default = Phenomena.AuxiliaryVerbs.Typology.InflPattern.auxHeaded

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instInhabitedInflPattern :

Inhabited InflPattern

Equations

Phenomena.AuxiliaryVerbs.Typology.instInhabitedInflPattern = { default := Phenomena.AuxiliaryVerbs.Typology.instInhabitedInflPattern.default }

inductive Phenomena.AuxiliaryVerbs.Typology.AVCElement :

Which element(s) of an AVC bear a given property.

aux : AVCElement
lex : AVCElement
both : AVCElement

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instDecidableEqAVCElement :

DecidableEq AVCElement

Equations

Phenomena.AuxiliaryVerbs.Typology.instDecidableEqAVCElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Typology.instReprAVCElement.repr :

AVCElement → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instReprAVCElement :

Repr AVCElement

Equations

Phenomena.AuxiliaryVerbs.Typology.instReprAVCElement = { reprPrec := Phenomena.AuxiliaryVerbs.Typology.instReprAVCElement.repr }

instance Phenomena.AuxiliaryVerbs.Typology.instBEqAVCElement :

Equations

Phenomena.AuxiliaryVerbs.Typology.instBEqAVCElement = { beq := Phenomena.AuxiliaryVerbs.Typology.instBEqAVCElement.beq }

def Phenomena.AuxiliaryVerbs.Typology.instBEqAVCElement.beq :

AVCElement → AVCElement → Bool

Equations

Phenomena.AuxiliaryVerbs.Typology.instBEqAVCElement.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

Key functions #

def Phenomena.AuxiliaryVerbs.Typology.InflPattern.semanticHead :

InflPattern → AVCElement

The semantic head is always the lexical verb (Anderson's invariant).

Equations

x✝.semanticHead = Phenomena.AuxiliaryVerbs.Typology.AVCElement.lex

Instances For

def Phenomena.AuxiliaryVerbs.Typology.InflPattern.inflOnlyOnPhrasalHead :

InflPattern → Bool

Whether inflection is hosted exclusively on the phrasal head (= AUX). Only aux-headed AVCs have this property: the AUX hosts all inflection and the LV is fully nonfinite. In doubled AVCs, both elements carry inflection, so the phrasal head is not the sole inflectional host.

Equations

Instances For

Cross-linguistic data #

structure Phenomena.AuxiliaryVerbs.Typology.AVCDatum :

A cross-linguistic AVC datum.

language : String
form : String
inflPattern : InflPattern
distribution : Option Core.Morphology.InflDistribution
gloss : String

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instReprAVCDatum :

Equations

Phenomena.AuxiliaryVerbs.Typology.instReprAVCDatum = { reprPrec := Phenomena.AuxiliaryVerbs.Typology.instReprAVCDatum.repr }

def Phenomena.AuxiliaryVerbs.Typology.instReprAVCDatum.repr :

AVCDatum → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.instBEqAVCDatum.beq :

AVCDatum → AVCDatum → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.AuxiliaryVerbs.Typology.instBEqAVCDatum.beq x✝¹ x✝ = false

Instances For

instance Phenomena.AuxiliaryVerbs.Typology.instBEqAVCDatum :

Equations

Phenomena.AuxiliaryVerbs.Typology.instBEqAVCDatum = { beq := Phenomena.AuxiliaryVerbs.Typology.instBEqAVCDatum.beq }

def Phenomena.AuxiliaryVerbs.Typology.english :

English will go — aux-headed (AUX carries tense, LV is bare infinitive).

Equations

Phenomena.AuxiliaryVerbs.Typology.english = { language := "English", form := "will go", inflPattern := Phenomena.AuxiliaryVerbs.Typology.InflPattern.auxHeaded, gloss := "FUT go.INF" }

Instances For

def Phenomena.AuxiliaryVerbs.Typology.doyayo :

Doyayo — split (AUX hosts subject/benefactive/object; LV hosts tense). Form derived from Fragments.Doyayo.AuxiliaryVerbs.

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.gorum :

Gorum — doubled (subject + TAM marked on both AUX and LV). Form derived from Fragments.Gorum.AuxiliaryVerbs.

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.jakaltek :

Jakaltek — split (absolutive on AUX, ergative on LV). Form derived from Fragments.Jakaltek.AuxiliaryVerbs.

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.pipil :

Pipil — split (auxiliaries mark tense; subject/object on LV). Form derived from Fragments.Pipil.AuxiliaryVerbs. Note: Pipil also has lex-headed AVCs (see Fragments.Pipil.AuxiliaryVerbs.lexHeadedForm).

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.finnish :

Finnish negative auxiliary ei — split (person/number on aux, TAM on main verb). The split nature derives from Fragments.Finnish.Negation.finnishNegDistribution: the negative auxiliary hosts negation, tense, and agreement, while the lexical verb retains only the stem and aspect (connegative form). @cite{karlsson-2017}.

The neg aux form derives from Fragments.Finnish.Negation.negParadigm (1sg).

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.pipilLexHeaded :

Pipil — lex-headed (AUX weli is uninflected; LV carries all agreement). This is Pipil's second AVC pattern, illustrating that a single language can exhibit multiple AVC types. Form derived from Fragments.Pipil.AuxiliaryVerbs.

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.hemba :

Hemba — split/doubled (subject doubled on both AUX and LV; tense on AUX only, mood on LV only). Form derived from Fragments.Hemba.AuxiliaryVerbs.

Equations

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

Instances For

def Phenomena.AuxiliaryVerbs.Typology.allData :

Equations

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

Instances For

Invariant theorems #

theorem Phenomena.AuxiliaryVerbs.Typology.semantic_head_always_lex (p : InflPattern) :

p.semanticHead = AVCElement.lex

Anderson's key insight: the semantic head is always the lexical verb, regardless of inflectional pattern.

theorem Phenomena.AuxiliaryVerbs.Typology.auxHeaded_infl_on_phrasal_head :

InflPattern.auxHeaded.inflOnlyOnPhrasalHead = true

In aux-headed AVCs, inflection is exclusively on the phrasal head (AUX).

theorem Phenomena.AuxiliaryVerbs.Typology.lexHeaded_infl_not_on_phrasal_head :

InflPattern.lexHeaded.inflOnlyOnPhrasalHead = false

In lex-headed AVCs, inflection is not on the phrasal head.

theorem Phenomena.AuxiliaryVerbs.Typology.doubled_infl_not_only_on_phrasal_head :

InflPattern.doubled.inflOnlyOnPhrasalHead = false

In doubled AVCs, inflection appears on both elements, so the phrasal head is not the sole host.

Bridge to UD #

def Phenomena.AuxiliaryVerbs.Typology.InflPattern.lvVerbForm :

InflPattern → UD.VerbForm

Expected verb form of the lexical verb in each AVC pattern. Aux-headed: LV is nonfinite (infinitive/participle). Lex-headed: LV is finite (carries TAM). Doubled/split/splitDoubled: LV is finite (carries at least some inflection).

Equations

Instances For

theorem Phenomena.AuxiliaryVerbs.Typology.auxHeaded_lv_nonfinite :

InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf

In aux-headed AVCs, the lexical verb is nonfinite.

theorem Phenomena.AuxiliaryVerbs.Typology.lexHeaded_lv_finite :

InflPattern.lexHeaded.lvVerbForm = UD.VerbForm.Fin

In lex-headed AVCs, the lexical verb is finite.

Bridge to FunctionWords #

theorem Phenomena.AuxiliaryVerbs.Typology.english_modals_are_aux_type :

Fragments.English.FunctionWords.can.auxType = Fragments.English.FunctionWords.AuxType.modal

English modals are aux-headed: they take AuxType.modal and the LV is bare.

Per-datum verification #

These theorems are load-bearing: changing a Fragment entry's inflPattern breaks exactly one theorem here.

theorem Phenomena.AuxiliaryVerbs.Typology.english_is_auxHeaded :

english.inflPattern = InflPattern.auxHeaded

theorem Phenomena.AuxiliaryVerbs.Typology.doyayo_is_split :

doyayo.inflPattern = InflPattern.split

theorem Phenomena.AuxiliaryVerbs.Typology.gorum_is_doubled :

gorum.inflPattern = InflPattern.doubled

theorem Phenomena.AuxiliaryVerbs.Typology.jakaltek_is_split :

jakaltek.inflPattern = InflPattern.split

theorem Phenomena.AuxiliaryVerbs.Typology.pipil_is_split :

pipil.inflPattern = InflPattern.split

theorem Phenomena.AuxiliaryVerbs.Typology.finnish_is_split :

finnish.inflPattern = InflPattern.split

theorem Phenomena.AuxiliaryVerbs.Typology.pipilLexHeaded_is_lexHeaded :

pipilLexHeaded.inflPattern = InflPattern.lexHeaded

theorem Phenomena.AuxiliaryVerbs.Typology.hemba_is_splitDoubled :

hemba.inflPattern = InflPattern.splitDoubled

Per-datum form verification #

These theorems verify that the forms derive from Fragment entries. Changing a Fragment form breaks the corresponding theorem.

theorem Phenomena.AuxiliaryVerbs.Typology.doyayo_form_from_fragment :

doyayo.form = Fragments.Doyayo.AuxiliaryVerbs.form

theorem Phenomena.AuxiliaryVerbs.Typology.gorum_form_from_fragment :

gorum.form = Fragments.Gorum.AuxiliaryVerbs.form

theorem Phenomena.AuxiliaryVerbs.Typology.jakaltek_form_from_fragment :

jakaltek.form = Fragments.Jakaltek.AuxiliaryVerbs.form

theorem Phenomena.AuxiliaryVerbs.Typology.pipil_form_from_fragment :

pipil.form = Fragments.Pipil.AuxiliaryVerbs.form

theorem Phenomena.AuxiliaryVerbs.Typology.finnish_form_from_fragment :

finnish.form = "en lue"

Per-datum distribution verification #

These theorems verify that distributions derive from Fragment entries. Changing a Fragment's inflDistribution breaks the corresponding theorem.

theorem Phenomena.AuxiliaryVerbs.Typology.doyayo_dist_from_fragment :

doyayo.distribution = some Fragments.Doyayo.AuxiliaryVerbs.inflDistribution

theorem Phenomena.AuxiliaryVerbs.Typology.gorum_dist_from_fragment :

gorum.distribution = some Fragments.Gorum.AuxiliaryVerbs.inflDistribution

theorem Phenomena.AuxiliaryVerbs.Typology.jakaltek_dist_from_fragment :

jakaltek.distribution = some Fragments.Jakaltek.AuxiliaryVerbs.inflDistribution

theorem Phenomena.AuxiliaryVerbs.Typology.pipil_dist_from_fragment :

pipil.distribution = some Fragments.Pipil.AuxiliaryVerbs.inflDistribution

theorem Phenomena.AuxiliaryVerbs.Typology.finnish_dist_from_fragment :

finnish.distribution = some Fragments.Finnish.Negation.finnishNegDistribution

theorem Phenomena.AuxiliaryVerbs.Typology.pipilLexHeaded_dist_from_fragment :

pipilLexHeaded.distribution = some Fragments.Pipil.AuxiliaryVerbs.lexHeadedDistribution

theorem Phenomena.AuxiliaryVerbs.Typology.pipilLexHeaded_form_from_fragment :

pipilLexHeaded.form = Fragments.Pipil.AuxiliaryVerbs.lexHeadedForm

theorem Phenomena.AuxiliaryVerbs.Typology.hemba_form_from_fragment :

hemba.form = Fragments.Hemba.AuxiliaryVerbs.form

theorem Phenomena.AuxiliaryVerbs.Typology.hemba_dist_from_fragment :

hemba.distribution = some Fragments.Hemba.AuxiliaryVerbs.inflDistribution

Bridge to Finnish Fragment #

theorem Phenomena.AuxiliaryVerbs.Typology.finnish_split_from_fragment :

have dist := Fragments.Finnish.Negation.finnishNegDistribution; dist.onAux ≠ [] ∧ dist.onLex ≠ []

The Finnish negative auxiliary construction is a split AVC: the auxiliary hosts some inflectional categories and the lexical verb hosts others, with neither element hosting all categories. Derived from Fragment distribution.