Documentation

Linglib.Core.Case

Case #

@cite{blake-1994} @cite{anderson-jm-2006} @cite{stassen-1985} @cite{comrie-1978} @cite{dixon-1994} @cite{heine-2009}

Framework-agnostic case infrastructure drawn from @cite{blake-1994}'s cross-linguistic survey and @cite{anderson-jm-2006}'s localist case grammar.

§ 1–3: Case Inventory (@cite{blake-1994}). 19 cross-linguistic case values, exhaustive enumeration, and case assignment modes.

§ 4–5: Blake's Hierarchy (@cite{blake-1994}, §5.8). Implicational hierarchy over case inventories with contiguity checking.

§ 6–11: Feature Decomposition (@cite{anderson-jm-2006}). Three first-order case features [abs, src, loc], 8 case relations, subject selection hierarchy, scenarios, and morphological case mapping.

§ 12: Split Ergativity (@cite{blake-1994}, @cite{dixon-1994}). Parameterized split-ergative conditioning.

§ 13: Case Extension (@cite{heine-2009}). Grammaticalization of case functions: source categories, extension paths (Table 29.6), chains, principles, and beyond-case targets.

§ 14: Comparative Entry (@cite{stassen-1985}). Typed record for comparative construction parameters.

Nanosyntax-specific material (Caha's containment hierarchy, *ABA constraint, syncretism adjacency) lives in Theories/Morphology/CaseContainment.lean.

inductive Core.AlignmentFamily :

The two major morphosyntactic alignment families.

accusative : AlignmentFamily
ergative : AlignmentFamily

Instances For

instance Core.instDecidableEqAlignmentFamily :

DecidableEq AlignmentFamily

Equations

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

def Core.instBEqAlignmentFamily.beq :

AlignmentFamily → AlignmentFamily → Bool

Equations

Core.instBEqAlignmentFamily.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.instBEqAlignmentFamily :

BEq AlignmentFamily

Equations

Core.instBEqAlignmentFamily = { beq := Core.instBEqAlignmentFamily.beq }

instance Core.instReprAlignmentFamily :

Repr AlignmentFamily

Equations

Core.instReprAlignmentFamily = { reprPrec := Core.instReprAlignmentFamily.repr }

def Core.instReprAlignmentFamily.repr :

AlignmentFamily → Nat → Std.Format

Equations

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

Instances For

inductive Core.Case :

Cross-linguistic case inventory (@cite{blake-1994}, Chs. 2, 5).

The 19 values cover the morphological cases attested across Blake's typological sample. Ordered roughly by the Blake hierarchy, from core grammatical cases to peripheral semantic cases.

nom : Case
acc : Case
erg : Case
abs : Case
gen : Case
dat : Case
loc : Case
abl : Case
all : Case
inst : Case
com : Case
voc : Case
part : Case
perl : Case
ben : Case
caus : Case
ess : Case
transl : Case
abess : Case

Instances For

instance Core.instDecidableEqCase :

DecidableEq Case

Equations

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

def Core.instBEqCase.beq :

Case → Case → Bool

Equations

Core.instBEqCase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.instBEqCase :

Equations

Core.instBEqCase = { beq := Core.instBEqCase.beq }

instance Core.instReprCase :

Equations

Core.instReprCase = { reprPrec := Core.instReprCase.repr }

def Core.instReprCase.repr :

Case → Nat → Std.Format

Equations

Core.instReprCase.repr Core.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.nom")).group prec✝
Core.instReprCase.repr Core.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.acc")).group prec✝
Core.instReprCase.repr Core.Case.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.erg")).group prec✝
Core.instReprCase.repr Core.Case.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.abs")).group prec✝
Core.instReprCase.repr Core.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.gen")).group prec✝
Core.instReprCase.repr Core.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.dat")).group prec✝
Core.instReprCase.repr Core.Case.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.loc")).group prec✝
Core.instReprCase.repr Core.Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.abl")).group prec✝
Core.instReprCase.repr Core.Case.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.all")).group prec✝
Core.instReprCase.repr Core.Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.inst")).group prec✝
Core.instReprCase.repr Core.Case.com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.com")).group prec✝
Core.instReprCase.repr Core.Case.voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.voc")).group prec✝
Core.instReprCase.repr Core.Case.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.part")).group prec✝
Core.instReprCase.repr Core.Case.perl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.perl")).group prec✝
Core.instReprCase.repr Core.Case.ben prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.ben")).group prec✝
Core.instReprCase.repr Core.Case.caus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.caus")).group prec✝
Core.instReprCase.repr Core.Case.ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.ess")).group prec✝
Core.instReprCase.repr Core.Case.transl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.transl")).group prec✝
Core.instReprCase.repr Core.Case.abess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Case.abess")).group prec✝

Instances For

def Core.instInhabitedCase.default :

Equations

Core.instInhabitedCase.default = Core.Case.nom

Instances For

instance Core.instInhabitedCase :

Equations

Core.instInhabitedCase = { default := Core.instInhabitedCase.default }

def Core.Case.allCases :

All 19 case values (for finite verification).

Equations

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

Instances For

theorem Core.Case.allCases_length :

allCases.length = 19

def Core.Case.inAllCases (c : Case) :

Equations

c.inAllCases = Core.Case.allCases.any fun (x : Core.Case) => x == c

Instances For

theorem Core.Case.allCases_complete (c : Case) :

c.inAllCases = true

inductive Core.CaseAssignment :

How case is assigned to an NP in a given construction (@cite{stassen-1985}, §2.2.1).

derived : CaseAssignment
fixed : CaseAssignment

Instances For

instance Core.instDecidableEqCaseAssignment :

DecidableEq CaseAssignment

Equations

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

instance Core.instBEqCaseAssignment :

BEq CaseAssignment

Equations

Core.instBEqCaseAssignment = { beq := Core.instBEqCaseAssignment.beq }

def Core.instBEqCaseAssignment.beq :

CaseAssignment → CaseAssignment → Bool

Equations

Core.instBEqCaseAssignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Core.instReprCaseAssignment.repr :

CaseAssignment → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Core.instReprCaseAssignment.repr Core.CaseAssignment.fixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseAssignment.fixed")).group prec✝

Instances For

instance Core.instReprCaseAssignment :

Repr CaseAssignment

Equations

Core.instReprCaseAssignment = { reprPrec := Core.instReprCaseAssignment.repr }

inductive Core.FixedCaseEncoding :

For fixed-case NPs, what syntactic role the NP occupies.

directObject : FixedCaseEncoding
adverbial : FixedCaseEncoding

Instances For

instance Core.instDecidableEqFixedCaseEncoding :

DecidableEq FixedCaseEncoding

Equations

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

instance Core.instBEqFixedCaseEncoding :

BEq FixedCaseEncoding

Equations

Core.instBEqFixedCaseEncoding = { beq := Core.instBEqFixedCaseEncoding.beq }

def Core.instBEqFixedCaseEncoding.beq :

FixedCaseEncoding → FixedCaseEncoding → Bool

Equations

Core.instBEqFixedCaseEncoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.instReprFixedCaseEncoding :

Repr FixedCaseEncoding

Equations

Core.instReprFixedCaseEncoding = { reprPrec := Core.instReprFixedCaseEncoding.repr }

def Core.instReprFixedCaseEncoding.repr :

FixedCaseEncoding → Nat → Std.Format

Equations

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

Instances For

def Core.Case.spatialTriad :

The three spatial cases that serve as adverbial markers cross-linguistically (@cite{stassen-1985}, §2.2.3).

Equations

Core.Case.spatialTriad = [Core.Case.abl , Core.Case.all , Core.Case.loc ]

Instances For

theorem Core.Case.spatialTriad_length :

spatialTriad.length = 3

def Core.Case.hierarchyRank :

Position on Blake's case hierarchy (@cite{blake-1994}, §5.8, ex. 68).

Higher rank = more likely to exist in a language's case inventory.

Ranks: 6 = core (NOM/ACC/ERG/ABS), 5 = GEN, 4 = DAT, 3 = LOC, 2 = ABL/INST, 1 = COM/ALL/PERL/BEN, 0 = VOC/PART/CAUS/ESS/TRANSL/ABESS.

Equations

Instances For

def Core.validInventory (inv : List Case) :

A case inventory is contiguous (no rank gaps) on the hierarchy. Formalizes Blake's implicational tendency (1994, §5.8).

Equations

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

Instances For

theorem Core.core_highest :

Case.nom.hierarchyRank = 6

theorem Core.gen_above_dat :

Case.gen.hierarchyRank > Case.dat.hierarchyRank

theorem Core.dat_above_loc :

Case.dat.hierarchyRank > Case.loc.hierarchyRank

theorem Core.loc_above_abl :

Case.loc.hierarchyRank > Case.abl.hierarchyRank

theorem Core.loc_above_inst :

Case.loc.hierarchyRank > Case.inst.hierarchyRank

theorem Core.abl_inst_same_rank :

Case.abl.hierarchyRank = Case.inst.hierarchyRank

theorem Core.two_case_valid :

validInventory [Case.nom , Case.acc ] = true

theorem Core.three_case_with_gen_valid :

validInventory [Case.nom , Case.acc , Case.gen ] = true

theorem Core.four_case_valid :

validInventory [Case.nom , Case.acc , Case.gen , Case.dat ] = true

theorem Core.five_case_valid :

validInventory [Case.nom , Case.acc , Case.gen , Case.dat , Case.loc ] = true

theorem Core.seven_case_valid :

validInventory [Case.nom , Case.acc , Case.gen , Case.dat , Case.loc , Case.abl , Case.inst ] = true

theorem Core.ergative_four_case_valid :

validInventory [Case.erg , Case.abs , Case.gen , Case.dat ] = true

theorem Core.split_ergative_valid :

validInventory [Case.nom , Case.erg , Case.abs , Case.gen ] = true

theorem Core.skip_gen_invalid :

validInventory [Case.nom , Case.acc , Case.dat ] = false

theorem Core.skip_gen_dat_invalid :

validInventory [Case.nom , Case.acc , Case.loc ] = false

theorem Core.skip_to_abl_invalid :

validInventory [Case.nom , Case.acc , Case.abl ] = false

theorem Core.skip_dat_invalid :

validInventory [Case.nom , Case.acc , Case.gen , Case.loc ] = false

inductive Core.CaseFeature :

Anderson's three first-order case features (@cite{anderson-jm-2006}, Ch. 6).

Instances For

instance Core.instDecidableEqCaseFeature :

DecidableEq CaseFeature

Equations

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

def Core.instBEqCaseFeature.beq :

CaseFeature → CaseFeature → Bool

Equations

Core.instBEqCaseFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.instBEqCaseFeature :

BEq CaseFeature

Equations

Core.instBEqCaseFeature = { beq := Core.instBEqCaseFeature.beq }

instance Core.instReprCaseFeature :

Repr CaseFeature

Equations

Core.instReprCaseFeature = { reprPrec := Core.instReprCaseFeature.repr }

def Core.instReprCaseFeature.repr :

CaseFeature → Nat → Std.Format

Equations

Core.instReprCaseFeature.repr Core.CaseFeature.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseFeature.abs")).group prec✝
Core.instReprCaseFeature.repr Core.CaseFeature.src prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseFeature.src")).group prec✝
Core.instReprCaseFeature.repr Core.CaseFeature.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseFeature.loc")).group prec✝

Instances For

structure Core.CaseRelation :

An argument's case specification: a bundle of first-order features (@cite{anderson-jm-2006}, Ch. 6). 8 possible bundles from 3 Bools.

abs : Bool
src : Bool
loc : Bool

Instances For

def Core.instDecidableEqCaseRelation.decEq (x✝ x✝¹ : CaseRelation) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Core.instDecidableEqCaseRelation :

DecidableEq CaseRelation

Equations

Core.instDecidableEqCaseRelation = Core.instDecidableEqCaseRelation.decEq

def Core.instBEqCaseRelation.beq :

CaseRelation → CaseRelation → Bool

Equations

Core.instBEqCaseRelation.beq { abs := a, src := a_1, loc := a_2 } { abs := b, src := b_1, loc := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
Core.instBEqCaseRelation.beq x✝¹ x✝ = false

Instances For

instance Core.instBEqCaseRelation :

BEq CaseRelation

Equations

Core.instBEqCaseRelation = { beq := Core.instBEqCaseRelation.beq }

instance Core.instReprCaseRelation :

Repr CaseRelation

Equations

Core.instReprCaseRelation = { reprPrec := Core.instReprCaseRelation.repr }

def Core.instReprCaseRelation.repr :

CaseRelation → Nat → Std.Format

Equations

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

Instances For

instance Core.instInhabitedCaseRelation :

Inhabited CaseRelation

Equations

Core.instInhabitedCaseRelation = { default := Core.instInhabitedCaseRelation.default }

def Core.instInhabitedCaseRelation.default :

Equations

Core.instInhabitedCaseRelation.default = { abs := default, src := default, loc := default }

Instances For

def Core.CaseRelation.neutral :

Equations

Core.CaseRelation.neutral = { abs := false, src := false, loc := false }

Instances For

def Core.CaseRelation.absolutive :

Equations

Core.CaseRelation.absolutive = { abs := true, src := false, loc := false }

Instances For

def Core.CaseRelation.ergative :

Equations

Core.CaseRelation.ergative = { abs := false, src := true, loc := false }

Instances For

def Core.CaseRelation.locative :

Equations

Core.CaseRelation.locative = { abs := false, src := false, loc := true }

Instances For

def Core.CaseRelation.srcAbs :

Equations

Core.CaseRelation.srcAbs = { abs := true, src := true, loc := false }

Instances For

def Core.CaseRelation.srcLoc :

Equations

Core.CaseRelation.srcLoc = { abs := false, src := true, loc := true }

Instances For

def Core.CaseRelation.absLoc :

Equations

Core.CaseRelation.absLoc = { abs := true, src := false, loc := true }

Instances For

def Core.CaseRelation.absSrcLoc :

Equations

Core.CaseRelation.absSrcLoc = { abs := true, src := true, loc := true }

Instances For

def Core.CaseRelation.subjectRank (cr : CaseRelation) :

The subject selection rank (@cite{anderson-jm-2006}, eq. 38'). src (agent) outranks abs (patient) outranks loc (spatial).

Equations

cr.subjectRank = if cr.src = true then 2 else if cr.abs = true then 1 else 0

Instances For

theorem Core.ergative_rank :

CaseRelation.ergative.subjectRank = 2

theorem Core.absolutive_rank :

CaseRelation.absolutive.subjectRank = 1

theorem Core.locative_rank :

CaseRelation.locative.subjectRank = 0

theorem Core.neutral_rank :

CaseRelation.neutral.subjectRank = 0

theorem Core.erg_above_abs :

CaseRelation.ergative.subjectRank > CaseRelation.absolutive.subjectRank

theorem Core.abs_above_loc :

CaseRelation.absolutive.subjectRank > CaseRelation.locative.subjectRank

theorem Core.experiencer_agent_same_rank :

CaseRelation.srcLoc.subjectRank = CaseRelation.ergative.subjectRank

theorem Core.selfMover_agent_same_rank :

CaseRelation.srcAbs.subjectRank = CaseRelation.ergative.subjectRank

theorem Core.contactive_abs_same_rank :

CaseRelation.absLoc.subjectRank = CaseRelation.absolutive.subjectRank

theorem Core.src_determines_subject_rank (cr : CaseRelation) (h : cr.src = true) :

cr.subjectRank = 2

theorem Core.abs_without_src_rank (cr : CaseRelation) (h1 : cr.src = false) (h2 : cr.abs = true) :

cr.subjectRank = 1

def Core.CaseRelation.isSubsetOf (inner outer : CaseRelation) :

Equations

inner.isSubsetOf outer = ((!inner.abs || outer.abs) && (!inner.src || outer.src) && (!inner.loc || outer.loc))

Instances For

theorem Core.absSrcLoc_is_top (cr : CaseRelation) :

cr.isSubsetOf CaseRelation.absSrcLoc = true

theorem Core.neutral_is_bottom (cr : CaseRelation) :

CaseRelation.neutral.isSubsetOf cr = true

def Core.CaseRelation.all :

List CaseRelation

Equations

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

Instances For

theorem Core.CaseRelation.all_length :

def Core.CaseRelation.inAll (cr : CaseRelation) :

Equations

cr.inAll = Core.CaseRelation.all.any fun (x : Core.CaseRelation) => x == cr

Instances For

theorem Core.CaseRelation.all_complete (cr : CaseRelation) :

cr.inAll = true

structure Core.Scenario :

A predicate's scenario (@cite{anderson-jm-2006}, Ch. 6): the case relations assigned to its arguments.

relations : List CaseRelation

Instances For

instance Core.instReprScenario :

Equations

Core.instReprScenario = { reprPrec := Core.instReprScenario.repr }

def Core.instReprScenario.repr :

Scenario → Nat → Std.Format

Equations

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

Instances For

def Core.Scenario.arity (s : Scenario) :

Equations

s.arity = s.relations.length

Instances For

def Core.Scenario.subjectRelation (s : Scenario) :

Option CaseRelation

Equations

s.subjectRelation = s.relations.head?

Instances For

def Core.Scenario.objectRelation (s : Scenario) :

Option CaseRelation

Equations

s.objectRelation = match s.relations with | head :: cr :: tail => some cr | x => none

Instances For

def Core.Scenario.transitive :

Equations

Core.Scenario.transitive = { relations := [Core.CaseRelation.ergative , Core.CaseRelation.absolutive ] }

Instances For

def Core.Scenario.unergative :

Equations

Core.Scenario.unergative = { relations := [Core.CaseRelation.ergative ] }

Instances For

def Core.Scenario.unaccusative :

Equations

Core.Scenario.unaccusative = { relations := [Core.CaseRelation.absolutive , Core.CaseRelation.locative ] }

Instances For

def Core.Scenario.selfMoving :

Equations

Core.Scenario.selfMoving = { relations := [Core.CaseRelation.srcAbs , Core.CaseRelation.locative ] }

Instances For

def Core.Scenario.experiencer :

Equations

Core.Scenario.experiencer = { relations := [Core.CaseRelation.srcLoc , Core.CaseRelation.absolutive ] }

Instances For

theorem Core.transitive_subject_object :

Scenario.transitive.subjectRelation = some CaseRelation.ergative ∧ Scenario.transitive.objectRelation = some CaseRelation.absolutive

theorem Core.unergative_subject_only :

Scenario.unergative.subjectRelation = some CaseRelation.ergative ∧ Scenario.unergative.objectRelation = none

theorem Core.unaccusative_subject_loc :

Scenario.unaccusative.subjectRelation = some CaseRelation.absolutive ∧ Scenario.unaccusative.objectRelation = some CaseRelation.locative

theorem Core.selfMoving_subject :

Scenario.selfMoving.subjectRelation = some CaseRelation.srcAbs ∧ Scenario.selfMoving.objectRelation = some CaseRelation.locative

theorem Core.experiencer_subject_object :

Scenario.experiencer.subjectRelation = some CaseRelation.srcLoc ∧ Scenario.experiencer.objectRelation = some CaseRelation.absolutive

theorem Core.transitive_subject_outranks_object :

CaseRelation.ergative.subjectRank > CaseRelation.absolutive.subjectRank

theorem Core.unergative_unaccusative_differ :

Scenario.unergative.subjectRelation ≠ Scenario.unaccusative.subjectRelation

def Core.Case.toCaseRelation :

Case → Option CaseRelation

Canonical mapping from Blake's morphological cases to Anderson's case-feature bundles (@cite{anderson-jm-2006}, Ch. 6).

Equations

Instances For

theorem Core.Case.nom_erg_same_relation :

nom.toCaseRelation = erg.toCaseRelation

theorem Core.Case.acc_abs_same_relation :

acc.toCaseRelation = abs.toCaseRelation

structure Core.SplitErgativity (Factor : Type) :

A split-ergative system (@cite{blake-1994}, @cite{dixon-1994}): alignment varies by some conditioning factor.

ergCondition : Factor → Bool

Instances For

def Core.SplitErgativity.alignment {Factor : Type} (split : SplitErgativity Factor) (f : Factor) :

AlignmentFamily

Equations

split.alignment f = if split.ergCondition f = true then Core.AlignmentFamily.ergative else Core.AlignmentFamily.accusative

Instances For

inductive Core.Aspect :

perfective : Aspect
imperfective : Aspect

Instances For

instance Core.instDecidableEqAspect :

DecidableEq Aspect

Equations

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

instance Core.instBEqAspect :

Equations

Core.instBEqAspect = { beq := Core.instBEqAspect.beq }

def Core.instBEqAspect.beq :

Aspect → Aspect → Bool

Equations

Core.instBEqAspect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Core.instReprAspect.repr :

Aspect → Nat → Std.Format

Equations

Core.instReprAspect.repr Core.Aspect.perfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Aspect.perfective")).group prec✝
Core.instReprAspect.repr Core.Aspect.imperfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Aspect.imperfective")).group prec✝

Instances For

instance Core.instReprAspect :

Equations

Core.instReprAspect = { reprPrec := Core.instReprAspect.repr }

def Core.hindiSplit :

SplitErgativity Aspect

Equations

Core.hindiSplit = { ergCondition := fun (a : Core.Aspect) => a == Core.Aspect.perfective }

Instances For

theorem Core.hindi_perfective_erg :

hindiSplit.alignment Aspect.perfective = AlignmentFamily.ergative

theorem Core.hindi_imperfective_acc :

hindiSplit.alignment Aspect.imperfective = AlignmentFamily.accusative

inductive Core.GramPrinciple :

The four principles governing grammaticalization of case markers. Development from lexical item to case marker is unidirectional and involves all or a subset of these principles.

extension : GramPrinciple
Use extended to wider range of complement nouns; meaning generalizes.
desemanticization : GramPrinciple
Lexical meaning lost; schematic case function acquired.
decategorialization : GramPrinciple
Morphosyntactic properties lost: becomes invariable clitic/affix, positionally restricted, paradigm shrinks.
erosion : GramPrinciple
Phonetic substance lost: loses stress, assimilates to host, may reduce to zero.

Instances For

instance Core.instDecidableEqGramPrinciple :

DecidableEq GramPrinciple

Equations

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

def Core.instBEqGramPrinciple.beq :

GramPrinciple → GramPrinciple → Bool

Equations

Core.instBEqGramPrinciple.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.instBEqGramPrinciple :

BEq GramPrinciple

Equations

Core.instBEqGramPrinciple = { beq := Core.instBEqGramPrinciple.beq }

def Core.instReprGramPrinciple.repr :

GramPrinciple → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Core.instReprGramPrinciple.repr Core.GramPrinciple.erosion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.GramPrinciple.erosion")).group prec✝

Instances For

instance Core.instReprGramPrinciple :

Repr GramPrinciple

Equations

Core.instReprGramPrinciple = { reprPrec := Core.instReprGramPrinciple.repr }

inductive Core.CaseGramStage :

Source category of a case marker on the grammaticalization cline (@cite{heine-2009} §29.1 eq. (1), §29.2).

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

Parallel to Diachronic.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

instance Core.instDecidableEqCaseGramStage :

DecidableEq CaseGramStage

Equations

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

instance Core.instBEqCaseGramStage :

BEq CaseGramStage

Equations

Core.instBEqCaseGramStage = { beq := Core.instBEqCaseGramStage.beq }

def Core.instBEqCaseGramStage.beq :

CaseGramStage → CaseGramStage → Bool

Equations

Core.instBEqCaseGramStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Core.instReprCaseGramStage.repr :

CaseGramStage → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Core.instReprCaseGramStage.repr Core.CaseGramStage.lexical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseGramStage.lexical")).group prec✝
Core.instReprCaseGramStage.repr Core.CaseGramStage.lost prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseGramStage.lost")).group prec✝

Instances For

instance Core.instReprCaseGramStage :

Repr CaseGramStage

Equations

Core.instReprCaseGramStage = { reprPrec := Core.instReprCaseGramStage.repr }

def Core.CaseGramStage.boundedness :

CaseGramStage → Nat

Boundedness increases monotonically along the case cline.

Equations

Instances For

instance Core.instLECaseGramStage :

LE CaseGramStage

Equations

Core.instLECaseGramStage = { le := fun (a b : Core.CaseGramStage) => a.boundedness ≤ b.boundedness }

instance Core.instLTCaseGramStage :

LT CaseGramStage

Equations

Core.instLTCaseGramStage = { lt := fun (a b : Core.CaseGramStage) => a.boundedness < b.boundedness }

instance Core.instDecidableLeCaseGramStage (a b : CaseGramStage) :

Decidable (a ≤ b)

Equations

Core.instDecidableLeCaseGramStage a b = inferInstanceAs (Decidable (a.boundedness ≤ b.boundedness))

instance Core.instDecidableLtCaseGramStage (a b : CaseGramStage) :

Decidable (a < b)

Equations

Core.instDecidableLtCaseGramStage a b = inferInstanceAs (Decidable (a.boundedness < b.boundedness))

theorem Core.caseGramCline_ordered :

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

def Core.caseExtension :

Case → List Case

Extension from one case function to another (@cite{heine-2009} Table 29.6).

When a case marker's use is extended from one syntactic context to another, the source function is less grammaticalized than the target. Direction is always concrete/peripheral → abstract/core.

Three Table 29.6 targets 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). The A → S core realignment is also omitted (it concerns grammatical roles, not morphological cases).

See also Phenomena.Possession.Typology.PossessionSource for @cite{heine-2009} Table 29.5 (possessive case sources, adapted from @cite{heine-1997}).

Equations

Instances For

theorem Core.abl_extends_inst :

Case.inst ∈ caseExtension Case.abl

theorem Core.abl_extends_caus :

Case.caus ∈ caseExtension Case.abl

theorem Core.abl_extends_gen :

Case.gen ∈ caseExtension Case.abl

theorem Core.abl_extends_part :

Case.part ∈ caseExtension Case.abl

theorem Core.all_extends_ben :

Case.ben ∈ caseExtension Case.all

theorem Core.all_extends_dat :

Case.dat ∈ caseExtension Case.all

theorem Core.all_extends_acc :

Case.acc ∈ caseExtension Case.all

theorem Core.com_extends_inst :

Case.inst ∈ caseExtension Case.com

theorem Core.com_extends_erg :

Case.erg ∈ caseExtension Case.com

theorem Core.com_extends_gen :

Case.gen ∈ caseExtension Case.com

theorem Core.dat_extends_acc :

Case.acc ∈ caseExtension Case.dat

theorem Core.inst_extends_erg :

Case.erg ∈ caseExtension Case.inst

theorem Core.loc_extends_com :

Case.com ∈ caseExtension Case.loc

theorem Core.loc_extends_erg :

Case.erg ∈ caseExtension Case.loc

theorem Core.loc_extends_inst :

Case.inst ∈ caseExtension Case.loc

theorem Core.nom_no_extension :

caseExtension Case.nom = []

theorem Core.acc_no_extension :

caseExtension Case.acc = []

theorem Core.erg_no_extension :

caseExtension Case.erg = []

theorem Core.abs_no_extension :

caseExtension Case.abs = []

theorem Core.chain_all_ben :

Case.ben ∈ caseExtension Case.all

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

theorem Core.chain_all_dat_acc :

Case.dat ∈ caseExtension Case.all ∧ Case.acc ∈ caseExtension Case.dat

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

theorem Core.chain_loc_com_inst :

Case.com ∈ caseExtension Case.loc ∧ Case.inst ∈ caseExtension Case.com

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

def Core.caseExtensionReachable2 (c₁ c₃ : Case) :

Transitivity: if c₁ extends to c₂ and c₂ extends to c₃, then c₃ is reachable from c₁ via a two-step grammaticalization chain.

Equations

Core.caseExtensionReachable2 c₁ c₃ = (Core.caseExtension c₁).any fun (c₂ : Core.Case) => (Core.caseExtension c₂).any fun (x : Core.Case) => x == c₃

Instances For

theorem Core.acc_reachable_from_all :

caseExtensionReachable2 Case.all Case.acc = true

Accusative is reachable from allative in two steps (via dative).

theorem Core.inst_reachable_from_loc :

caseExtensionReachable2 Case.loc Case.inst = true

Instrumental is reachable from locative in two steps (via comitative).

inductive Core.BeyondCaseTarget :

Case markers can further grammaticalize into non-case functions. These are the four main directions (@cite{heine-2009} §29.4).

clauseSubordinator : BeyondCaseTarget
Case → clause subordinator (e.g., Newari instrumental -na → temporal subordinator).
modalMarker : BeyondCaseTarget
Case → modality marker: subordinate clauses acquire subjunctive/ irrealis readings (connects to Semantics.Modality.Narrog).
conjunction : BeyondCaseTarget
Comitative → NP conjunction 'and' (e.g., X with Y → X and Y).
tenseMarker : BeyondCaseTarget
Purposive → future tense marker.

Instances For

instance Core.instDecidableEqBeyondCaseTarget :

DecidableEq BeyondCaseTarget

Equations

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

def Core.instBEqBeyondCaseTarget.beq :

BeyondCaseTarget → BeyondCaseTarget → Bool

Equations

Core.instBEqBeyondCaseTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.instBEqBeyondCaseTarget :

BEq BeyondCaseTarget

Equations

Core.instBEqBeyondCaseTarget = { beq := Core.instBEqBeyondCaseTarget.beq }

instance Core.instReprBeyondCaseTarget :

Repr BeyondCaseTarget

Equations

Core.instReprBeyondCaseTarget = { reprPrec := Core.instReprBeyondCaseTarget.repr }

def Core.instReprBeyondCaseTarget.repr :

BeyondCaseTarget → Nat → Std.Format

Equations

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

Instances For

structure Core.ComparativeEntry :

A language's comparative construction entry (@cite{stassen-1985}).

standardCase : Case
caseAssignment : CaseAssignment
fixedEncoding : Option FixedCaseEncoding
standardMarker : String
hasDegreeMorphology : Bool

Instances For

def Core.instReprComparativeEntry.repr :

ComparativeEntry → Nat → Std.Format

Equations

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

Instances For

instance Core.instReprComparativeEntry :

Repr ComparativeEntry

Equations

Core.instReprComparativeEntry = { reprPrec := Core.instReprComparativeEntry.repr }

def Core.instBEqComparativeEntry.beq :

ComparativeEntry → ComparativeEntry → Bool

Equations

One or more equations did not get rendered due to their size.
Core.instBEqComparativeEntry.beq x✝¹ x✝ = false

Instances For

instance Core.instBEqComparativeEntry :

BEq ComparativeEntry

Equations

Core.instBEqComparativeEntry = { beq := Core.instBEqComparativeEntry.beq }