Japanese case markers

Japanese marks the relations of a noun phrase with particles after it. Tsujimura separates the case particles, the nominative ga, the accusative o, the dative ni and the genitive no, from the postpositions, the counterparts of English prepositions (Japanese.Adpositions): de 'at', e 'to', to 'with', made 'until' and kara 'from'. The nominative and the accusative, unlike case endings, may be dropped in casual speech, Tomodati(-ga) kita? 'Has my friend come?', and replaced by mo 'also' and sae 'even'. Two markers are polysemous: ni marks recipients, goals, times and the location of existence, and de the location of an action and its instrument, so ni and de share the locative and ni and e the allative. Ga is recorded as the nominative, setting aside the exhaustive-listing reading of Kuroda and Kuno; no is also a nominalizer, to a quotative complementizer and kara a reason conjunction, uses outside case marking. Sadakane and Koizumi's four ni lexemes refine the single ni entry, the matter of Studies/SadakaneKoizumi1995.lean.

Main definitions

• Japanese.Case, Japanese.Case.exponents: the four cases of the case particles, and the particles.
• Japanese.Case.label, Japanese.Case.functions: the comparative value each case is named for, and the values it expresses.
• Japanese.Case.droppable: the cases whose particles casual speech drops.

References

• [Kun73]
• [Kur65]
• [SK95]
• [Tsu14]

Case particles

inductive Japanese.Case : Type

The four cases the case particles mark.

• nom : Case

  The nominative, ga.

• acc : Case

  The accusative, o.

• gen : Case

  The genitive, no.

• dat : Case

  The dative, ni.

@[instance_reducible]

instance Japanese.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Japanese.instFintypeCase : Fintype Case

Equations

• Japanese.instFintypeCase = { elems := { val := ↑Japanese.Case.enumList, nodup := Japanese.Case.enumList_nodup }, complete := Japanese.instFintypeCase._proof_1 }

def Japanese.instReprCase.repr : Case → ℕ → Std.Format

Equations

• Japanese.instReprCase.repr Japanese.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Case.nom")).group prec✝
• Japanese.instReprCase.repr Japanese.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Case.acc")).group prec✝
• Japanese.instReprCase.repr Japanese.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Case.gen")).group prec✝
• Japanese.instReprCase.repr Japanese.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Case.dat")).group prec✝

@[instance_reducible]

instance Japanese.instReprCase : Repr Case

Equations

• Japanese.instReprCase = { reprPrec := Japanese.instReprCase.repr }

def Japanese.Case.exponents : Case → List Morphology.Morph

c.exponents is the case particle of c, enclitic ga が, o を, no の or ni に.

Equations

• Japanese.Case.nom.exponents = [Morphology.Morph.encl "ga"]
• Japanese.Case.acc.exponents = [Morphology.Morph.encl "o"]
• Japanese.Case.gen.exponents = [Morphology.Morph.encl "no"]
• Japanese.Case.dat.exponents = [Morphology.Morph.encl "ni"]

def Japanese.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Japanese.Case.nom.label = Case.nom
• Japanese.Case.acc.label = Case.acc
• Japanese.Case.gen.label = Case.gen
• Japanese.Case.dat.label = Case.dat

def Japanese.Case.functions : Case → Finset _root_.Case

c.functions are the comparative values c expresses; ni marks the recipient, the goal, the time and the location of existence.

Equations

• Japanese.Case.dat.functions = {Case.dat, Case.loc, Case.all, Case.tem}
• x✝.functions = {x✝.label}

theorem Japanese.Case.label_mem_functions (c : Case) : c.label ∈ c.functions

def Japanese.Case.droppable : Finset Case

The cases whose particles casual speech drops, the nominative and the accusative.

Equations

• Japanese.Case.droppable = {Japanese.Case.nom, Japanese.Case.acc}