Documentation

Linglib.Syntax.AuxiliaryVerbs

Auxiliary verb constructions: inflection-locus typology #

The auxiliary-verb-construction (AVC) inflection typology of [And06a]: the semantic head is always the lexical verb, but the inflectional host varies across five macro-patterns. Graduated from the dissolved Typology/ drawer (the orthogonal be/have-selection typology split off to Semantics/ArgumentStructure/AuxiliarySelection.lean).

The five patterns #

Pattern	Infl host	Example
Aux-headed	AUX	English have eaten, is eating
Lex-headed	LEX	Pipil weli ni-nehnemi
Doubled	AUX+LEX	Gorum miŋ ne-gaʔ-ru ne-laʔ-ru
Split	AUX or LEX	Jakaltek (abs/erg), Finnish neg-aux ei
Split/doubled	AUX+LEX	Pipil, Doyayo (Ch 5), Hemba

Main definitions #

InflPattern — the five-way inflectional-distribution macro-classification.
AVCElement — which element(s) of an AVC bear a given property.
InflPattern.semanticHead / inflHost / inflOnlyOnPhrasalHead / lvVerbForm.

Per-language AVCDatum instances + Fragment-grounding verification theorems live in Studies/Anderson2006.lean (paper-anchored data).

Core types #

inductive AuxiliaryVerbs.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 (AUX uninflected, LV carries person); Doyayo mi¹ (gi²) kpel¹-ko¹ (Ch 3 ex 15a).
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 element, with no overlap). E.g., Jakaltek šk-ach w-ila (absolutive on AUX, ergative on LV); Finnish neg-aux ei (person/number on AUX, connegative + aspect on LV).
splitDoubled : InflPattern
Some categories on both AUX and LV (doubled), others exclusive to one element (split). [And06a] ch. 5 §5.2 dedicates ~30 pages to this pattern with 30+ language exemplars across §§5.2.1–5.2.3 (Limbu, Manam, Kuot, Doyayo, Mbay, Lamba, Pipil, Persian, Swahili, Panyjima, Kemantney, Oshikwanyama, Shambala, Vinmavis, Nambiquara, Baure, Luganda, Nasioi, Os, Xhosa, ...). Common, not marginal.

Instances For

@[implicit_reducible]

instance AuxiliaryVerbs.instDecidableEqInflPattern :

DecidableEq InflPattern

Equations

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

def AuxiliaryVerbs.instReprInflPattern.repr :

InflPattern → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance AuxiliaryVerbs.instReprInflPattern :

Repr InflPattern

Equations

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

@[implicit_reducible]

instance AuxiliaryVerbs.instInhabitedInflPattern :

Inhabited InflPattern

Equations

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

inductive AuxiliaryVerbs.AVCElement :

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

aux : AVCElement
lex : AVCElement
both : AVCElement

Instances For

@[implicit_reducible]

instance AuxiliaryVerbs.instDecidableEqAVCElement :

DecidableEq AVCElement

Equations

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

def AuxiliaryVerbs.instReprAVCElement.repr :

AVCElement → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance AuxiliaryVerbs.instReprAVCElement :

Repr AVCElement

Equations

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

Key functions #

def AuxiliaryVerbs.InflPattern.semanticHead :

InflPattern → AVCElement

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

Equations

x✝.semanticHead = AuxiliaryVerbs.AVCElement.lex

Instances For

def AuxiliaryVerbs.InflPattern.inflHost :

InflPattern → AVCElement

Which element hosts inflection in each pattern.

Equations

Instances For

def AuxiliaryVerbs.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

def AuxiliaryVerbs.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

Invariant theorems #

About InflPattern itself — Fragment-independent substrate facts. Per-language verification theorems live in Studies/Anderson2006.lean.

theorem AuxiliaryVerbs.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 AuxiliaryVerbs.auxHeaded_infl_on_phrasal_head :

InflPattern.auxHeaded.inflOnlyOnPhrasalHead = true

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

theorem AuxiliaryVerbs.lexHeaded_infl_not_on_phrasal_head :

InflPattern.lexHeaded.inflOnlyOnPhrasalHead = false

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

theorem AuxiliaryVerbs.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.

theorem AuxiliaryVerbs.auxHeaded_lv_nonfinite :

InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf

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

theorem AuxiliaryVerbs.lexHeaded_lv_finite :

InflPattern.lexHeaded.lvVerbForm = UD.VerbForm.Fin

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