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.

Classifier handles are typed Fragments.Japanese.Classifier constructors from the enum-as-source-of-truth fragment (Fragments.Japanese.Classifier).

structure Fragments.Japanese.Nouns.NounEntry : Type

A lexical entry for a Japanese noun.

• form : String
• romaji : String
• pluralForm : Option String
• classifier : Option Classifier
• proper : Bool

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Nouns.instReprNounEntry : Repr NounEntry

Equations

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

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

@[implicit_reducible]

instance Fragments.Japanese.Nouns.instBEqNounEntry : BEq NounEntry

Equations

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

structure Fragments.Japanese.Nouns.NP : Type

Japanese NP structure (no articles).

Case marking on the NP is not represented at this layer — the authoritative case-marker registry lives in Fragments.Japanese.Case (CaseMarker with fields romaji, kana, cases : Finset Core.Case, omissibleInCasual). A case-marked NP type is intentionally not introduced here; downstream consumers that need NP-with-case should pair NP with a CaseMarker explicitly rather than embedding a case slot of unknown semantics.

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

@[implicit_reducible]

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.

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

@[implicit_reducible]

instance Fragments.Japanese.Nouns.instBEqNP : BEq NP

Equations

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

def Fragments.Japanese.Nouns.japaneseBlocking : Semantics.Kinds.NMP.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.Kinds.NMP.NominalMapping

Equations

• Fragments.Japanese.Nouns.japaneseMapping = Semantics.Kinds.NMP.NominalMapping.argOnly

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

Equations

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

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.Classifier.hiki }

def Fragments.Japanese.Nouns.neko : NounEntry

Equations

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

def Fragments.Japanese.Nouns.hito : NounEntry

Equations

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

def Fragments.Japanese.Nouns.hon : NounEntry

Equations

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

def Fragments.Japanese.Nouns.kuruma : NounEntry

Equations

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

def Fragments.Japanese.Nouns.tori : NounEntry

Equations

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

def Fragments.Japanese.Nouns.hana : NounEntry

Equations

• Fragments.Japanese.Nouns.hana = { form := "花", romaji := "hana", classifier := some Fragments.Japanese.Classifier.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 Classifier.hiki) = true

Small animals take 匹.

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

Birds take 羽.

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

Books take 冊.

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

Vehicles/machines take 台.

theorem Fragments.Japanese.Nouns.people_take_nin : hito.classifier = some Classifier.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.konoInu : NP

Equations

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