Grammaticalization

@cite{anderson-2006} @cite{bybee-perkins-pagliuca-1994} @cite{lehmann-1985} @cite{heine-kuteva-2002} @cite{hopper-traugott-2003}

Grammaticalization: the diachronic process by which lexical items become grammatical markers. The canonical cline is:

full verb → auxiliary → clitic → affix → zero

This process is cross-linguistically unidirectional: movement is always toward greater morphological boundedness (@cite{lehmann-1985}, @cite{hopper-traugott-2003}).

Main definitions

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

Connections

• Core.FormFrequency: form-frequency correspondence is a parallel diachronic process (phonological erosion of frequent forms).
• Core.Lexical.Binominal: the bleaching cline for binominals (N+PP → pseudo-partitive → evaluative → modifier → intensifier) is a specialized grammaticalization path in the nominal domain.
• Core.Subjectivity: Traugott's subjectification cline is a semantic dimension of grammaticalization (see Diachronic.Subjectification).

inductive Diachronic.Grammaticalization.GramStage : Type

Stage on the grammaticalization cline for verbal elements. @cite{anderson-2006} Ch 7, @cite{hopper-traugott-2003} Ch 6.

• 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).

instance Diachronic.Grammaticalization.instDecidableEqGramStage : DecidableEq GramStage

Equations

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

def Diachronic.Grammaticalization.instReprGramStage.repr : GramStage → Nat → Std.Format

Equations

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

instance Diachronic.Grammaticalization.instReprGramStage : Repr GramStage

Equations

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

instance Diachronic.Grammaticalization.instBEqGramStage : BEq GramStage

Equations

• Diachronic.Grammaticalization.instBEqGramStage = { beq := Diachronic.Grammaticalization.instBEqGramStage.beq }

def Diachronic.Grammaticalization.instBEqGramStage.beq : GramStage → GramStage → Bool

Equations

• Diachronic.Grammaticalization.instBEqGramStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Diachronic.Grammaticalization.GramStage.boundedness : GramStage → Nat

Boundedness increases monotonically along the cline.

Equations

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

instance Diachronic.Grammaticalization.instLEGramStage : LE GramStage

Equations

• Diachronic.Grammaticalization.instLEGramStage = { le := fun (a b : Diachronic.Grammaticalization.GramStage) => a.boundedness ≤ b.boundedness }

instance Diachronic.Grammaticalization.instLTGramStage : LT GramStage

Equations

• Diachronic.Grammaticalization.instLTGramStage = { lt := fun (a b : Diachronic.Grammaticalization.GramStage) => a.boundedness < b.boundedness }

instance Diachronic.Grammaticalization.instDecidableLeGramStage (a b : GramStage) : Decidable (a ≤ b)

Equations

• Diachronic.Grammaticalization.instDecidableLeGramStage a b = inferInstanceAs (Decidable (a.boundedness ≤ b.boundedness))

instance Diachronic.Grammaticalization.instDecidableLtGramStage (a b : GramStage) : Decidable (a < b)

Equations

• Diachronic.Grammaticalization.instDecidableLtGramStage a b = inferInstanceAs (Decidable (a.boundedness < b.boundedness))

theorem Diachronic.Grammaticalization.cline_strictly_ordered : GramStage.fullVerb < GramStage.auxiliary ∧ GramStage.auxiliary < GramStage.clitic ∧ GramStage.clitic < GramStage.affix ∧ GramStage.affix < GramStage.zero

The cline is strictly ordered: each stage is more bound than the previous.

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

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

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

inductive Diachronic.Grammaticalization.AVCSource : Type

Diachronic source construction from which an AVC grammaticalizes. @cite{anderson-2006} §7, @cite{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.

instance Diachronic.Grammaticalization.instDecidableEqAVCSource : DecidableEq AVCSource

Equations

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

instance Diachronic.Grammaticalization.instReprAVCSource : Repr AVCSource

Equations

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

def Diachronic.Grammaticalization.instReprAVCSource.repr : AVCSource → Nat → Std.Format

Equations

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

def Diachronic.Grammaticalization.instBEqAVCSource.beq : AVCSource → AVCSource → Bool

Equations

• Diachronic.Grammaticalization.instBEqAVCSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Diachronic.Grammaticalization.instBEqAVCSource : BEq AVCSource

Equations

• Diachronic.Grammaticalization.instBEqAVCSource = { beq := Diachronic.Grammaticalization.instBEqAVCSource.beq }