Documentation

Linglib.Features.Case.Grammaticalization

Case Grammaticalization #

The case-marker grammaticalization cline (lexical > adposition > case affix > loss) and the extension paths from Heine (2009) Table 29.6. Three extension targets in Table 29.6 are not representable as Case values and are omitted: purposive (from allative, benefactive), manner (from comitative, instrumental), agent (from locative; collapses with ergative in our system).

Extension is the relation Case.Extends : Case → Case → Prop (Heine's Table 29.6 row pattern). Multi-step extension is just Relation.TransGen Case.Extends from mathlib — there is no separate two-step or n-step predicate to maintain.

Case-marker cline #

inductive CaseGramStage :

Source category of a case marker on the grammaticalization cline ([Hei09a] §29.1 eq. (1), §29.2).

noun, verb (> adverb) > adposition > case affix > loss

Parallel to Grammaticalization.GramStage (for verbal elements), but specific to case-marker development.

lexical : CaseGramStage
Lexical noun or verb source (§29.2.1–29.2.2).
adposition : CaseGramStage
Free adposition: preposition or postposition (§29.2.3).
caseAffix : CaseGramStage
Bound case affix: suffix or prefix (§29.2.3 endpoint).
lost : CaseGramStage
Case marker lost: erosion endpoint or merger.

Instances For

@[implicit_reducible]

instance instDecidableEqCaseGramStage :

DecidableEq CaseGramStage

Equations

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

@[implicit_reducible]

instance instReprCaseGramStage :

Repr CaseGramStage

Equations

instReprCaseGramStage = { reprPrec := instReprCaseGramStage.repr }

def instReprCaseGramStage.repr :

CaseGramStage → ℕ → Std.Format

Equations

instReprCaseGramStage.repr CaseGramStage.lexical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CaseGramStage.lexical")).group prec✝
instReprCaseGramStage.repr CaseGramStage.adposition prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CaseGramStage.adposition")).group prec✝
instReprCaseGramStage.repr CaseGramStage.caseAffix prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CaseGramStage.caseAffix")).group prec✝
instReprCaseGramStage.repr CaseGramStage.lost prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CaseGramStage.lost")).group prec✝

Instances For

def CaseGramStage.boundedness :

CaseGramStage → ℕ

Boundedness increases monotonically along the case cline.

Equations

CaseGramStage.lexical.boundedness = 0
CaseGramStage.adposition.boundedness = 1
CaseGramStage.caseAffix.boundedness = 2
CaseGramStage.lost.boundedness = 3

Instances For

@[implicit_reducible]

instance instLinearOrderCaseGramStage :

LinearOrder CaseGramStage

Equations

instLinearOrderCaseGramStage = LinearOrder.lift' CaseGramStage.boundedness instLinearOrderCaseGramStage._proof_1

theorem caseGramCline_ordered :

CaseGramStage.lexical < CaseGramStage.adposition ∧ CaseGramStage.adposition < CaseGramStage.caseAffix ∧ CaseGramStage.caseAffix < CaseGramStage.lost

Case-extension dot-methods #

These live under namespace Features so they project onto the Case type via dot-notation (mirroring Case.hierarchyRank in Features/Case/Basic.lean).

def Case.Extends :

Case → Case → Prop

Direct extension between case functions ([Hei09a] Table 29.6).

Case.Extends c₁ c₂ holds iff a single row of Heine's table licenses extending a c₁-marker to c₂ uses. Direction is concrete/peripheral → abstract/core: the source function is less grammaticalized than the target.

See also Possession.Source for [Hei09a] Table 29.5 (possessive case sources, adapted from [Hei97]).

Equations

Instances For

def Case.extensionTargets (c : Case) :

Finset Case

Direct-extension targets of c, as a Finset derived from Case.Extends. Useful for membership queries by decide.

Equations

c.extensionTargets = Finset.filter c.Extends Finset.univ

Instances For

theorem Case.mem_extensionTargets {c₁ c₂ : Case} :

c₂ ∈ c₁.extensionTargets ↔ c₁.Extends c₂

Case.Extends itself is the public Table 29.6 spec — concrete extension facts (Case.Extends .abl .inst, ¬ Case.Extends .nom .acc, etc.) are immediate by decide against the def and need not be re-stated as a thicket of named theorems. The chain theorems below bundle multiple table rows into the named Heine (2009) eq. (2) chains.

theorem Features.chain_all_ben :

Case.all.Extends Case.ben

Chain (2a): allative > benefactive > purposive. Only the first step is representable as Case → Case.

theorem Features.chain_all_dat_acc :

Case.all.Extends Case.dat ∧ Case.dat.Extends Case.acc

Chain (2b): allative > dative > accusative/O. Both steps are direct extensions.

theorem Features.chain_loc_com_inst :

Case.loc.Extends Case.com ∧ Case.com.Extends Case.inst

Chain (2c): locative > comitative > instrumental > manner. The first two steps are representable as Case → Case.

@[reducible, inline]

abbrev Case.ExtensionReachable :

Case → Case → Prop

Multi-step extension reachability — the transitive closure of Case.Extends. Composing chain rows of Table 29.6 produces an extension path of any finite length.

Equations

Case.ExtensionReachable = Relation.TransGen Case.Extends

Instances For

@[implicit_reducible]

instance Features.instDecidableRelCaseExtensionReachable :

DecidableRel Case.ExtensionReachable

Case.ExtensionReachable is decidable via the Core.Relation.ReflTransGen substrate's TransGen Fintype headline. The step function is Case.extensionTargets.

Equations

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

theorem Features.acc_reachable_from_all :

Case.all.ExtensionReachable Case.acc

Accusative is reachable from allative via dative (chain 2b).

theorem Features.inst_reachable_from_loc :

Case.loc.ExtensionReachable Case.inst

Instrumental is reachable from locative via comitative (chain 2c).