Grammaticalization

[Hei93] [And06a] [BPP94] [lehmann-1985] [heine-kuteva-2002] [hopper-traugott-2003]

Grammaticalization: the diachronic process by which lexical items become grammatical markers. The cline of verbal grammaticalization formalized here is the 5-stage variant:

full verb → auxiliary → clitic → affix → zero

Attribution

The verbal cline is anchored on [Hei93] ch. 3 (the source [And06a] cites at p. 5 as Heine (1993: 48ff.)). Anderson's own running shorthand at p. 5 collapses to three stages (L[exical] V[erb] >> A[uxiliary] V > AF[fi]X); the 5-stage form here splits Heine's continuum at the canonical clitic/affix/zero boundaries also used by [lehmann-1985] and [hopper-traugott-2003].

Caveat ([Hei93] p. 66, endorsed by [And06a] p. 5): "we are dealing with chains [of grammaticalization] and since chains are by definition continuous structures, setting up stages along these structures must remain an arbitrary and/or artificial endeavor." The discrete enum below is a working approximation; consumer files that need finer-grained transitions should pair GramStage with their own intermediate-state predicates rather than treat the 5 cases as exhaustive.

This process is cross-linguistically unidirectional: movement is always toward greater morphological boundedness ([lehmann-1985], [hopper-traugott-2003]).

Main definitions

• GramStage: stages on the grammaticalization cline
• GramStage.boundedness: numeric encoding of morphological boundedness
• GramStage.toMorphStatus: projection onto Morphology.MorphStatus
• AVCSource: diachronic source constructions for auxiliary verb constructions

Connections

• Haspelmath2021 (§0): form-frequency correspondence is a parallel diachronic process (phonological erosion of frequent forms). Apparatus co-located in the Haspelmath 2021 study file (single consumer); promote to substrate when a second diachronic study materializes.
• Quantification.Binominal: the bleaching cline for binominals (N+PP → pseudo-partitive → evaluative → modifier → intensifier) is a specialized grammaticalization path in the nominal domain.
• Features.Subjectivity: Traugott's subjectification cline is a semantic dimension of grammaticalization (see Studies/Traugott2010.lean).

inductive Grammaticalization.GramStage : Type

Stage on the grammaticalization cline for verbal elements. Cline anchored on [Hei93] for the broad path LV >> AV >> AFFIX; the specific 5-stage segmentation (fullVerb / auxiliary / clitic / affix / zero) is a coarsening drawn from [lehmann-1985] and [hopper-traugott-2003] ch. 6, NOT a direct rendering of Heine's own staging (Heine 1993 §2.4.2 uses a finer 7-stage A-G chain: concrete-source → starting-down → budding → defective → linguistic-hybrid → firmly-grammaticalized → orphaning). [And06a] p. 5 attributes the LV >> AV > AFX path to Heine 1993:48ff. without committing to a specific stage count; ch. 7 traces grammaticalization of source constructions onto whatever cline the framework adopts. The 5-stage enum here is the linglib working approximation, not Heine's own taxonomy.

• fullVerb : GramStage

  Lexical verb with full argument structure.

• auxiliary : GramStage

  Grammaticalized verb, restricted morphosyntax.

• clitic : GramStage

  Phonologically reduced, syntactically dependent.

• affix : GramStage

  Bound morpheme, part of the verbal word.

• zero : GramStage

  No overt marker (grammaticalization endpoint).

@[implicit_reducible]

instance Grammaticalization.instDecidableEqGramStage : DecidableEq GramStage

Equations

• Grammaticalization.instDecidableEqGramStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Grammaticalization.instReprGramStage.repr : GramStage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Grammaticalization.instReprGramStage : Repr GramStage

Equations

• Grammaticalization.instReprGramStage = { reprPrec := Grammaticalization.instReprGramStage.repr }

def Grammaticalization.GramStage.boundedness : GramStage → ℕ

Boundedness increases monotonically along the cline.

Equations

• Grammaticalization.GramStage.fullVerb.boundedness = 0
• Grammaticalization.GramStage.auxiliary.boundedness = 1
• Grammaticalization.GramStage.clitic.boundedness = 2
• Grammaticalization.GramStage.affix.boundedness = 3
• Grammaticalization.GramStage.zero.boundedness = 4

@[implicit_reducible]

instance Grammaticalization.instLinearOrderGramStage : LinearOrder GramStage

Equations

• Grammaticalization.instLinearOrderGramStage = LinearOrder.lift' Grammaticalization.GramStage.boundedness Grammaticalization.instLinearOrderGramStage._proof_1

def Grammaticalization.isUnidirectional (_s₁ _s₂ : GramStage) (_h : _s₁ < _s₂) : Prop

Unidirectionality: grammaticalization never reverses. Formalized as: if a language has a marker at stage s₂ that historically derives from stage s₁, then s₁ < s₂.

Equations

• Grammaticalization.isUnidirectional _s₁ _s₂ _h = ¬_s₂ < _s₁

theorem Grammaticalization.unidirectional_of_lt {s₁ s₂ : GramStage} (h : s₁ < s₂) : isUnidirectional s₁ s₂ h

def Grammaticalization.GramStage.toMorphStatus : GramStage → Option Morphology.MorphStatus

Project a grammaticalization stage onto its canonical Morphology.MorphStatus realization. Auxiliaries and full verbs are free words on the cline; clitics map to simple-clitic status; affixes to inflectional-affix status; the zero endpoint has no overt morphological realization.

Equations

• Grammaticalization.GramStage.fullVerb.toMorphStatus = some Morphology.MorphStatus.freeWord
• Grammaticalization.GramStage.auxiliary.toMorphStatus = some Morphology.MorphStatus.freeWord
• Grammaticalization.GramStage.clitic.toMorphStatus = some Morphology.MorphStatus.simpleClitic
• Grammaticalization.GramStage.affix.toMorphStatus = some Morphology.MorphStatus.inflAffix
• Grammaticalization.GramStage.zero.toMorphStatus = none

theorem Grammaticalization.affix_more_bound_than_auxiliary : GramStage.affix.boundedness > GramStage.auxiliary.boundedness

The .affix stage is strictly more grammaticalized (more morphologically bound) than the .auxiliary stage. Used by Typology/Negation.lean to compare the cline placement of negative affixes vs negative verbs.

inductive Grammaticalization.AVCSource : Type

Diachronic source construction from which an AVC grammaticalizes. [And06a] §7, [heine-kuteva-2002].

• serialVerb : AVCSource

  Serial verb constructions: two verbs in sequence, one grammaticalizes into an auxiliary. Common in West African, SE Asian.

• complementTaking : AVCSource

  Complement-taking verb: matrix verb takes clausal complement, the matrix verb grammaticalizes. Common source for modals.

• motionVerb : AVCSource

  Motion verb: 'go'/'come' grammaticalize into future/past markers. Cross-linguistically one of the most common paths.

• posturalVerb : AVCSource

  Postural verb: 'sit'/'stand'/'lie' grammaticalize into progressive/habitual aspect markers.

@[implicit_reducible]

instance Grammaticalization.instDecidableEqAVCSource : DecidableEq AVCSource

Equations

• Grammaticalization.instDecidableEqAVCSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Grammaticalization.instReprAVCSource.repr : AVCSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Grammaticalization.instReprAVCSource : Repr AVCSource

Equations

• Grammaticalization.instReprAVCSource = { reprPrec := Grammaticalization.instReprAVCSource.repr }