Japanese Noun Lexicon Fragment

Japanese-specific noun entries and NP structure. Japanese is [+arg, -pred]: no articles, optional number morphology, classifiers for counting, bare nouns freely occur as arguments with multiple interpretations.

Classifiers are typed ClassifierEntry values from the classifier lexicon (Fragments.Japanese.Classifiers).

structure Fragments.Japanese.Nouns.NounEntry : Type

A lexical entry for a Japanese noun.

• form : String
• romaji : String
• pluralForm : Option String
• classifier : Option Core.NounCategorization.ClassifierEntry
• proper : Bool

def Fragments.Japanese.Nouns.instReprNounEntry.repr : NounEntry → ℕ → Std.Format

Equations

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

instance Fragments.Japanese.Nouns.instReprNounEntry : Repr NounEntry

Equations

• Fragments.Japanese.Nouns.instReprNounEntry = { reprPrec := Fragments.Japanese.Nouns.instReprNounEntry.repr }

instance Fragments.Japanese.Nouns.instBEqNounEntry : BEq NounEntry

Equations

• Fragments.Japanese.Nouns.instBEqNounEntry = { beq := Fragments.Japanese.Nouns.instBEqNounEntry.beq }

def Fragments.Japanese.Nouns.instBEqNounEntry.beq : NounEntry → NounEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.Nouns.instBEqNounEntry.beq x✝¹ x✝ = false

inductive Fragments.Japanese.Nouns.CaseParticle : Type

Japanese case particles.

• ga : CaseParticle
• wo : CaseParticle
• ni : CaseParticle
• de : CaseParticle
• no : CaseParticle
• wa : CaseParticle

instance Fragments.Japanese.Nouns.instDecidableEqCaseParticle : DecidableEq CaseParticle

Equations

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

def Fragments.Japanese.Nouns.instReprCaseParticle.repr : CaseParticle → ℕ → Std.Format

Equations

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

instance Fragments.Japanese.Nouns.instReprCaseParticle : Repr CaseParticle

Equations

• Fragments.Japanese.Nouns.instReprCaseParticle = { reprPrec := Fragments.Japanese.Nouns.instReprCaseParticle.repr }

def Fragments.Japanese.Nouns.instBEqCaseParticle.beq : CaseParticle → CaseParticle → Bool

Equations

• Fragments.Japanese.Nouns.instBEqCaseParticle.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Japanese.Nouns.instBEqCaseParticle : BEq CaseParticle

Equations

• Fragments.Japanese.Nouns.instBEqCaseParticle = { beq := Fragments.Japanese.Nouns.instBEqCaseParticle.beq }

structure Fragments.Japanese.Nouns.NP : Type

Japanese NP structure (no articles, but has case particles).

• noun : NounEntry
• isBare : Bool
• caseParticle : Option CaseParticle
• demonstrative : Option String
• numeral : Option ℕ
• usePlural : Bool

instance Fragments.Japanese.Nouns.instReprNP : Repr NP

Equations

• Fragments.Japanese.Nouns.instReprNP = { reprPrec := Fragments.Japanese.Nouns.instReprNP.repr }

def Fragments.Japanese.Nouns.instReprNP.repr : NP → ℕ → Std.Format

Equations

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

instance Fragments.Japanese.Nouns.instBEqNP : BEq NP

Equations

• Fragments.Japanese.Nouns.instBEqNP = { beq := Fragments.Japanese.Nouns.instBEqNP.beq }

def Fragments.Japanese.Nouns.instBEqNP.beq : NP → NP → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.Nouns.instBEqNP.beq x✝¹ x✝ = false

def Fragments.Japanese.Nouns.japaneseBlocking : Semantics.Lexical.Noun.Kind.Chierchia1998.BlockingPrinciple

Japanese has no articles, so no type shifts are blocked.

Equations

• Fragments.Japanese.Nouns.japaneseBlocking = { determiners := [], iotaBlocked := false, existsBlocked := false, downBlocked := false }

def Fragments.Japanese.Nouns.japaneseMapping : Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping

Equations

• Fragments.Japanese.Nouns.japaneseMapping = Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argOnly

def Fragments.Japanese.Nouns.bareNP (n : NounEntry) : NP

Equations

• Fragments.Japanese.Nouns.bareNP n = { noun := n, isBare := true }

def Fragments.Japanese.Nouns.gaNP (n : NounEntry) : NP

Equations

• Fragments.Japanese.Nouns.gaNP n = { noun := n, isBare := true, caseParticle := some Fragments.Japanese.Nouns.CaseParticle.ga }

def Fragments.Japanese.Nouns.woNP (n : NounEntry) : NP

Equations

• Fragments.Japanese.Nouns.woNP n = { noun := n, isBare := true, caseParticle := some Fragments.Japanese.Nouns.CaseParticle.wo }

def Fragments.Japanese.Nouns.waNP (n : NounEntry) : NP

Equations

• Fragments.Japanese.Nouns.waNP n = { noun := n, isBare := true, caseParticle := some Fragments.Japanese.Nouns.CaseParticle.wa }

def Fragments.Japanese.Nouns.konoNP (n : NounEntry) : NP

Equations

• Fragments.Japanese.Nouns.konoNP n = { noun := n, isBare := false, demonstrative := some "この" }

def Fragments.Japanese.Nouns.sonoNP (n : NounEntry) : NP

Equations

• Fragments.Japanese.Nouns.sonoNP n = { noun := n, isBare := false, demonstrative := some "その" }

def Fragments.Japanese.Nouns.inu : NounEntry

Equations

• Fragments.Japanese.Nouns.inu = { form := "犬", romaji := "inu", classifier := some Fragments.Japanese.Classifiers.hiki }

def Fragments.Japanese.Nouns.neko : NounEntry

Equations

• Fragments.Japanese.Nouns.neko = { form := "猫", romaji := "neko", classifier := some Fragments.Japanese.Classifiers.hiki }

def Fragments.Japanese.Nouns.hito : NounEntry

Equations

• Fragments.Japanese.Nouns.hito = { form := "人", romaji := "hito", pluralForm := some "人たち", classifier := some Fragments.Japanese.Classifiers.nin }

def Fragments.Japanese.Nouns.hon : NounEntry

Equations

• Fragments.Japanese.Nouns.hon = { form := "本", romaji := "hon", classifier := some Fragments.Japanese.Classifiers.satsu }

def Fragments.Japanese.Nouns.kuruma : NounEntry

Equations

• Fragments.Japanese.Nouns.kuruma = { form := "車", romaji := "kuruma", classifier := some Fragments.Japanese.Classifiers.dai }

def Fragments.Japanese.Nouns.tori : NounEntry

Equations

• Fragments.Japanese.Nouns.tori = { form := "鳥", romaji := "tori", classifier := some Fragments.Japanese.Classifiers.wa }

def Fragments.Japanese.Nouns.hana : NounEntry

Equations

• Fragments.Japanese.Nouns.hana = { form := "花", romaji := "hana", classifier := some Fragments.Japanese.Classifiers.hon' }

def Fragments.Japanese.Nouns.mizu : NounEntry

Equations

• Fragments.Japanese.Nouns.mizu = { form := "水", romaji := "mizu", classifier := none }

def Fragments.Japanese.Nouns.gohan : NounEntry

Equations

• Fragments.Japanese.Nouns.gohan = { form := "ご飯", romaji := "gohan", classifier := none }

def Fragments.Japanese.Nouns.musume : NounEntry

Equations

• Fragments.Japanese.Nouns.musume = { form := "娘", romaji := "musume", pluralForm := some "娘たち" }

def Fragments.Japanese.Nouns.musuko : NounEntry

Equations

• Fragments.Japanese.Nouns.musuko = { form := "息子", romaji := "musuko", pluralForm := some "息子たち" }

def Fragments.Japanese.Nouns.gakusei : NounEntry

Equations

• Fragments.Japanese.Nouns.gakusei = { form := "学生", romaji := "gakusei", pluralForm := some "学生たち" }

def Fragments.Japanese.Nouns.sensei : NounEntry

Equations

• Fragments.Japanese.Nouns.sensei = { form := "先生", romaji := "sensei", pluralForm := some "先生たち" }

def Fragments.Japanese.Nouns.tomodachi : NounEntry

Equations

• Fragments.Japanese.Nouns.tomodachi = { form := "友達", romaji := "tomodachi" }

def Fragments.Japanese.Nouns.taro : NounEntry

Equations

• Fragments.Japanese.Nouns.taro = { form := "太郎", romaji := "Tarō", proper := true }

def Fragments.Japanese.Nouns.hanako : NounEntry

Equations

• Fragments.Japanese.Nouns.hanako = { form := "花子", romaji := "Hanako", proper := true }

def Fragments.Japanese.Nouns.yamada : NounEntry

Equations

• Fragments.Japanese.Nouns.yamada = { form := "山田", romaji := "Yamada", proper := true }

def Fragments.Japanese.Nouns.tanaka : NounEntry

Equations

• Fragments.Japanese.Nouns.tanaka = { form := "田中", romaji := "Tanaka", proper := true }

def Fragments.Japanese.Nouns.allNouns : List NounEntry

Equations

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

def Fragments.Japanese.Nouns.lookup (form : String) : Option NounEntry

Equations

• Fragments.Japanese.Nouns.lookup form = List.find? (fun (n : Fragments.Japanese.Nouns.NounEntry) => n.form == form || n.pluralForm == some form) Fragments.Japanese.Nouns.allNouns

def Fragments.Japanese.Nouns.bareNPLicensed : Bool

Equations

• Fragments.Japanese.Nouns.bareNPLicensed = true

theorem Fragments.Japanese.Nouns.animals_take_hiki : ([inu, neko].all fun (x : NounEntry) => x.classifier == some Classifiers.hiki) = true

Small animals take 匹.

theorem Fragments.Japanese.Nouns.birds_take_wa : tori.classifier = some Classifiers.wa

Birds take 羽.

theorem Fragments.Japanese.Nouns.books_take_satsu : hon.classifier = some Classifiers.satsu

Books take 冊.

theorem Fragments.Japanese.Nouns.vehicles_take_dai : kuruma.classifier = some Classifiers.dai

Vehicles/machines take 台.

theorem Fragments.Japanese.Nouns.people_take_nin : hito.classifier = some Classifiers.nin

People take 人.

theorem Fragments.Japanese.Nouns.mass_nouns_no_classifier : ([mizu, gohan].all fun (x : NounEntry) => x.classifier == none) = true

Mass nouns have no classifier.

def Fragments.Japanese.Nouns.inuNP : NP

Equations

• Fragments.Japanese.Nouns.inuNP = Fragments.Japanese.Nouns.bareNP Fragments.Japanese.Nouns.inu

def Fragments.Japanese.Nouns.inuGa : NP

Equations

• Fragments.Japanese.Nouns.inuGa = Fragments.Japanese.Nouns.gaNP Fragments.Japanese.Nouns.inu

def Fragments.Japanese.Nouns.inuWo : NP

Equations

• Fragments.Japanese.Nouns.inuWo = Fragments.Japanese.Nouns.woNP Fragments.Japanese.Nouns.inu

def Fragments.Japanese.Nouns.konoInu : NP

Equations

• Fragments.Japanese.Nouns.konoInu = Fragments.Japanese.Nouns.konoNP Fragments.Japanese.Nouns.inu