Mandarin Chinese Noun Lexicon Fragment

@cite{chierchia-1998}

Mandarin-specific noun entries. Mandarin is [+arg, -pred]: all nouns are kind-denoting by default, no number morphology, no articles, classifiers required for counting, bare nouns freely occur as arguments.

Classifiers are now typed ClassifierEntry values from the classifier lexicon (Fragments.Mandarin.Classifiers), replacing the previous unstructured Option String representation. This enables verification of Aikhenvald's semantic generalizations about classifier selection.

structure Fragments.Mandarin.Nouns.NounEntry : Type

A lexical entry for a Mandarin noun.

The classifier field points to a typed ClassifierEntry from the classifier lexicon, carrying semantic information about why that classifier is selected (animacy, shape, function, etc.).

• form : String
• pinyin : String
• classifier : Option Typology.ClassifierEntry
• proper : Bool

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

Equations

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

@[implicit_reducible]

instance Fragments.Mandarin.Nouns.instReprNounEntry : Repr NounEntry

Equations

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

@[implicit_reducible]

instance Fragments.Mandarin.Nouns.instBEqNounEntry : BEq NounEntry

Equations

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

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

Equations

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

structure Fragments.Mandarin.Nouns.NP : Type

Mandarin NP structure (no grammatical number or articles).

• noun : NounEntry
• isBare : Bool
• demonstrative : Option String
• numeral : Option ℕ
• classifierOverride : Option Typology.ClassifierEntry

@[implicit_reducible]

instance Fragments.Mandarin.Nouns.instReprNP : Repr NP

Equations

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Mandarin.Nouns.instBEqNP : BEq NP

Equations

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

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

Equations

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

def Fragments.Mandarin.Nouns.NP.classifier (np : NP) : Option Typology.ClassifierEntry

Equations

• np.classifier = (np.classifierOverride <|> np.noun.classifier)

def Fragments.Mandarin.Nouns.NP.classifierForm (np : NP) : Option String

The form string of the classifier (for display).

Equations

• np.classifierForm = Option.map (fun (x : Typology.ClassifierEntry) => x.form) np.classifier

def Fragments.Mandarin.Nouns.mandarinBlocking : Semantics.Kinds.NMP.BlockingPrinciple

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

Equations

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

def Fragments.Mandarin.Nouns.mandarinMapping : Semantics.Kinds.NMP.NominalMapping

Equations

• Fragments.Mandarin.Nouns.mandarinMapping = Semantics.Kinds.NMP.NominalMapping.argOnly

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

Equations

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

def Fragments.Mandarin.Nouns.zheNP (n : NounEntry) : NP

Equations

• Fragments.Mandarin.Nouns.zheNP n = { noun := n, isBare := false, demonstrative := some "这" }

def Fragments.Mandarin.Nouns.naNP (n : NounEntry) : NP

Equations

• Fragments.Mandarin.Nouns.naNP n = { noun := n, isBare := false, demonstrative := some "那" }

def Fragments.Mandarin.Nouns.numNP (n : NounEntry) (num : ℕ) : NP

Equations

• Fragments.Mandarin.Nouns.numNP n num = { noun := n, isBare := false, numeral := some num }

def Fragments.Mandarin.Nouns.gou : NounEntry

Equations

• Fragments.Mandarin.Nouns.gou = { form := "狗", pinyin := "gǒu", classifier := some Fragments.Mandarin.Classifiers.zhi }

def Fragments.Mandarin.Nouns.mao : NounEntry

Equations

• Fragments.Mandarin.Nouns.mao = { form := "猫", pinyin := "māo", classifier := some Fragments.Mandarin.Classifiers.zhi }

def Fragments.Mandarin.Nouns.niao : NounEntry

Equations

• Fragments.Mandarin.Nouns.niao = { form := "鸟", pinyin := "niǎo", classifier := some Fragments.Mandarin.Classifiers.zhi }

def Fragments.Mandarin.Nouns.ren : NounEntry

Equations

• Fragments.Mandarin.Nouns.ren = { form := "人", pinyin := "rén" }

def Fragments.Mandarin.Nouns.xuesheng : NounEntry

Equations

• Fragments.Mandarin.Nouns.xuesheng = { form := "学生", pinyin := "xuésheng" }

def Fragments.Mandarin.Nouns.pengyou : NounEntry

Equations

• Fragments.Mandarin.Nouns.pengyou = { form := "朋友", pinyin := "péngyou" }

def Fragments.Mandarin.Nouns.laoshi : NounEntry

Equations

• Fragments.Mandarin.Nouns.laoshi = { form := "老师", pinyin := "lǎoshī", classifier := some Fragments.Mandarin.Classifiers.wei }

def Fragments.Mandarin.Nouns.nuer : NounEntry

Equations

• Fragments.Mandarin.Nouns.nuer = { form := "女儿", pinyin := "nǚ'ér" }

def Fragments.Mandarin.Nouns.erzi : NounEntry

Equations

• Fragments.Mandarin.Nouns.erzi = { form := "儿子", pinyin := "érzi" }

def Fragments.Mandarin.Nouns.shu : NounEntry

Equations

• Fragments.Mandarin.Nouns.shu = { form := "书", pinyin := "shū", classifier := some Fragments.Mandarin.Classifiers.ben }

def Fragments.Mandarin.Nouns.che : NounEntry

Equations

• Fragments.Mandarin.Nouns.che = { form := "车", pinyin := "chē", classifier := some Fragments.Mandarin.Classifiers.liang }

def Fragments.Mandarin.Nouns.hua : NounEntry

Equations

• Fragments.Mandarin.Nouns.hua = { form := "花", pinyin := "huā", classifier := some Fragments.Mandarin.Classifiers.duo }

def Fragments.Mandarin.Nouns.shui : NounEntry

Equations

• Fragments.Mandarin.Nouns.shui = { form := "水", pinyin := "shuǐ", classifier := none }

def Fragments.Mandarin.Nouns.fan : NounEntry

Equations

• Fragments.Mandarin.Nouns.fan = { form := "饭", pinyin := "fàn", classifier := none }

def Fragments.Mandarin.Nouns.zuoyi : NounEntry

Equations

• Fragments.Mandarin.Nouns.zuoyi = { form := "座椅", pinyin := "zuòyǐ" }

def Fragments.Mandarin.Nouns.fangxiangpan : NounEntry

Equations

• Fragments.Mandarin.Nouns.fangxiangpan = { form := "方向盘", pinyin := "fāngxiàngpán" }

def Fragments.Mandarin.Nouns.lunzi : NounEntry

Equations

• Fragments.Mandarin.Nouns.lunzi = { form := "轮子", pinyin := "lúnzi" }

def Fragments.Mandarin.Nouns.fengmian : NounEntry

Equations

• Fragments.Mandarin.Nouns.fengmian = { form := "封面", pinyin := "fēngmiàn" }

def Fragments.Mandarin.Nouns.zuozhe : NounEntry

Equations

• Fragments.Mandarin.Nouns.zuozhe = { form := "作者", pinyin := "zuòzhě", classifier := some Fragments.Mandarin.Classifiers.wei }

def Fragments.Mandarin.Nouns.muqin : NounEntry

Equations

• Fragments.Mandarin.Nouns.muqin = { form := "母亲", pinyin := "mǔqīn", classifier := some Fragments.Mandarin.Classifiers.wei }

def Fragments.Mandarin.Nouns.fuqin : NounEntry

Equations

• Fragments.Mandarin.Nouns.fuqin = { form := "父亲", pinyin := "fùqīn", classifier := some Fragments.Mandarin.Classifiers.wei }

def Fragments.Mandarin.Nouns.laobanniang : NounEntry

Equations

• Fragments.Mandarin.Nouns.laobanniang = { form := "老板娘", pinyin := "lǎobǎnniáng", classifier := some Fragments.Mandarin.Classifiers.wei }

def Fragments.Mandarin.Nouns.laoban : NounEntry

Equations

• Fragments.Mandarin.Nouns.laoban = { form := "老板", pinyin := "lǎobǎn", classifier := some Fragments.Mandarin.Classifiers.wei }

def Fragments.Mandarin.Nouns.zhangsan : NounEntry

Equations

• Fragments.Mandarin.Nouns.zhangsan = { form := "张三", pinyin := "Zhāng Sān", proper := true }

def Fragments.Mandarin.Nouns.lisi : NounEntry

Equations

• Fragments.Mandarin.Nouns.lisi = { form := "李四", pinyin := "Lǐ Sì", proper := true }

def Fragments.Mandarin.Nouns.xiaoming : NounEntry

Equations

• Fragments.Mandarin.Nouns.xiaoming = { form := "小明", pinyin := "Xiǎo Míng", proper := true }

def Fragments.Mandarin.Nouns.allNouns : List NounEntry

Equations

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

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

Equations

• Fragments.Mandarin.Nouns.lookup form = List.find? (fun (n : Fragments.Mandarin.Nouns.NounEntry) => n.form == form) Fragments.Mandarin.Nouns.allNouns

def Fragments.Mandarin.Nouns.bareNPLicensed : Bool

Equations

• Fragments.Mandarin.Nouns.bareNPLicensed = true

theorem Fragments.Mandarin.Nouns.animals_take_zhi : ([gou, mao, niao].all fun (x : NounEntry) => x.classifier == some Classifiers.zhi) = true

All animal nouns take the animal classifier 只.

theorem Fragments.Mandarin.Nouns.honorific_humans_take_wei : ([laoshi, zuozhe, muqin, fuqin].all fun (x : NounEntry) => x.classifier == some Classifiers.wei) = true

Honorific-human nouns take 位.

theorem Fragments.Mandarin.Nouns.books_take_ben : shu.classifier = some Classifiers.ben

Books take the bound-volume classifier 本.

theorem Fragments.Mandarin.Nouns.vehicles_take_liang : che.classifier = some Classifiers.liang

Vehicles take the vehicle classifier 辆.

theorem Fragments.Mandarin.Nouns.mass_nouns_no_classifier : ([shui, fan].all fun (x : NounEntry) => x.classifier == none) = true

Mass nouns have no classifier.

def Fragments.Mandarin.Nouns.gouNP : NP

Equations

• Fragments.Mandarin.Nouns.gouNP = Fragments.Mandarin.Nouns.bareNP Fragments.Mandarin.Nouns.gou

def Fragments.Mandarin.Nouns.shuiNP : NP

Equations

• Fragments.Mandarin.Nouns.shuiNP = Fragments.Mandarin.Nouns.bareNP Fragments.Mandarin.Nouns.shui

def Fragments.Mandarin.Nouns.zheGou : NP

Equations

• Fragments.Mandarin.Nouns.zheGou = Fragments.Mandarin.Nouns.zheNP Fragments.Mandarin.Nouns.gou

def Fragments.Mandarin.Nouns.sanBenShu : NP

Equations

• Fragments.Mandarin.Nouns.sanBenShu = Fragments.Mandarin.Nouns.numNP Fragments.Mandarin.Nouns.shu 3