Japanese Numeral Classifier Inventory

[aikhenvald-2000] [downing-1996] [sudo-2016]

The closed inventory of Japanese numeral classifiers (josūshi 助数詞) as a finite inductive type. Properties (form, gloss, encoded semantic parameters, dimensionality, mensural-vs-sortal, default flag) are projection functions or Decidable predicates over the type, not fields on a struct.

Inventory provenance

• The 27 core entries are [downing-1996]'s Table 1.1, the forms every one of its fifteen questionnaire respondents used.
• The 6 extended entries (sao, wa, furi, zen, kyaku, rin) are drawn from the 47 forms of [downing-1996]'s Table 1.2, the forms a majority of its respondents used; rin is also [sudo-2016]'s worked example (eq. 4).
• kumi and daasu are [sudo-2016]'s worked examples of non-atomic classifiers (eqs. 9a, 9b) and hai the textbook counter of cupfuls; all three lie outside [downing-1996]'s definition, which excludes groupings, standard measures and containers (Chapter 1).

Out of scope

• Phonological allomorphy (rendaku/sokuon: ippon/sanbon/roppon for -hon, ippiki/sanbiki/roppiki for -hiki) — would belong with Phonology/.
• Native vs Sino-Japanese numeral series split (tsu selects native hitotsu/futatsu/...; Sino-classifiers select ichi/ni/san/...).
• Inventory expansion to high-frequency classifiers not in Downing's inventory (-kai 回, -bai 倍, -ban 番, -do 度, etc.).

The typological parameters follow [downing-1996] and [aikhenvald-2000]: numeral classifiers suffixed to numerals, chosen on semantic grounds, with tsu as the general classifier; the semantic parameters and the general classifier are read off the inventory.

inductive Japanese.Classifier : Type

The closed inventory of Japanese numeral classifiers. Constructors are named by Hepburn romanization, with kanji-distinct homophones disambiguated by content (e.g., kenBuilding 軒 vs kenIncident 件).

• tsu : Classifier
• nin : Classifier
• mei : Classifier
• hiki : Classifier
• tou : Classifier
• hon : Classifier
• mai : Classifier
• ko : Classifier
• satsu : Classifier
• tsubu : Classifier
• dai : Classifier
• kenBuilding : Classifier
• kenIncident : Classifier
• ki : Classifier
• ku : Classifier
• kyoku : Classifier
• mon : Classifier
• mune : Classifier
• seki : Classifier
• soku : Classifier
• soo : Classifier
• ten : Classifier
• toori : Classifier
• tsuu : Classifier
• kabu : Classifier
• shoku : Classifier
• teki : Classifier
• sao : Classifier
• wa : Classifier
• furi : Classifier
• zen : Classifier
• kyaku : Classifier
• rin : Classifier
• hai : Classifier
• kumi : Classifier
• daasu : Classifier

@[instance_reducible]

instance Japanese.instDecidableEqClassifier : DecidableEq Classifier

Equations

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

def Japanese.instReprClassifier.repr : Classifier → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Japanese.instReprClassifier.repr Japanese.Classifier.tsu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tsu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.nin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.nin")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mei prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mei")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.hiki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.hiki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.tou prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tou")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.hon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.hon")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mai")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ko prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ko")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.satsu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.satsu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.tsubu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tsubu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.dai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.dai")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kyoku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kyoku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mon")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.mune prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.mune")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.seki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.seki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.soku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.soku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.soo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.soo")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.ten prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.ten")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.toori prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.toori")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.tsuu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.tsuu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kabu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kabu")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.shoku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.shoku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.teki prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.teki")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.sao prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.sao")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.wa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.wa")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.furi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.furi")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.zen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.zen")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kyaku prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kyaku")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.rin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.rin")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.hai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.hai")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.kumi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.kumi")).group prec✝
• Japanese.instReprClassifier.repr Japanese.Classifier.daasu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Japanese.Classifier.daasu")).group prec✝

@[instance_reducible]

instance Japanese.instReprClassifier : Repr Classifier

Equations

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

@[instance_reducible]

instance Japanese.instBEqClassifier : BEq Classifier

Equations

• Japanese.instBEqClassifier = { beq := Japanese.instBEqClassifier.beq }

def Japanese.instBEqClassifier.beq : Classifier → Classifier → Bool

Equations

• Japanese.instBEqClassifier.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Japanese.Classifier.core : List Classifier

The 27 core classifiers of [downing-1996], Table 1.1.

Equations

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

def Japanese.Classifier.extended : List Classifier

The classifiers carried from [downing-1996]'s extended inventory, Table 1.2.

Equations

• Japanese.Classifier.extended = [Japanese.Classifier.sao, Japanese.Classifier.wa, Japanese.Classifier.furi, Japanese.Classifier.zen, Japanese.Classifier.kyaku, Japanese.Classifier.rin]

def Japanese.Classifier.additions : List Classifier

The counters outside [downing-1996]'s definition: the textbook -hai (cupful), and [sudo-2016]'s non-atomic -kumi (pair) and -daasu (dozen), eqs. 9a and 9b.

Equations

• Japanese.Classifier.additions = [Japanese.Classifier.hai, Japanese.Classifier.kumi, Japanese.Classifier.daasu]

def Japanese.Classifier.all : List Classifier

The full inventory: Downing core ++ Downing extended ++ additions. Source-of-truth for consumer iteration (lookup, aggregations) and the Fintype instance.

Equations

• Japanese.Classifier.all = Japanese.Classifier.core ++ Japanese.Classifier.extended ++ Japanese.Classifier.additions

theorem Japanese.Classifier.all_nodup : all.Nodup

theorem Japanese.Classifier.mem_all (c : Classifier) : c ∈ all

@[instance_reducible]

instance Japanese.instFintypeClassifier : Fintype Classifier

Equations

• Japanese.instFintypeClassifier = { elems := Japanese.Classifier.all.toFinset, complete := Japanese.instFintypeClassifier._proof_1 }

§1: Surface form

def Japanese.Classifier.form : Classifier → String

The kanji (or hiragana, for -tsu) form of the classifier.

Equations

• Japanese.Classifier.tsu.form = "つ"
• Japanese.Classifier.nin.form = "人"
• Japanese.Classifier.mei.form = "名"
• Japanese.Classifier.hiki.form = "匹"
• Japanese.Classifier.tou.form = "頭"
• Japanese.Classifier.hon.form = "本"
• Japanese.Classifier.mai.form = "枚"
• Japanese.Classifier.ko.form = "個"
• Japanese.Classifier.satsu.form = "冊"
• Japanese.Classifier.tsubu.form = "粒"
• Japanese.Classifier.dai.form = "台"
• Japanese.Classifier.kenBuilding.form = "軒"
• Japanese.Classifier.kenIncident.form = "件"
• Japanese.Classifier.ki.form = "機"
• Japanese.Classifier.ku.form = "句"
• Japanese.Classifier.kyoku.form = "曲"
• Japanese.Classifier.mon.form = "問"
• Japanese.Classifier.mune.form = "棟"
• Japanese.Classifier.seki.form = "隻"
• Japanese.Classifier.soku.form = "足"
• Japanese.Classifier.soo.form = "艘"
• Japanese.Classifier.ten.form = "点"
• Japanese.Classifier.toori.form = "通り"
• Japanese.Classifier.tsuu.form = "通"
• Japanese.Classifier.kabu.form = "株"
• Japanese.Classifier.shoku.form = "食"
• Japanese.Classifier.teki.form = "滴"
• Japanese.Classifier.sao.form = "竿"
• Japanese.Classifier.wa.form = "羽"
• Japanese.Classifier.furi.form = "振"
• Japanese.Classifier.zen.form = "膳"
• Japanese.Classifier.kyaku.form = "脚"
• Japanese.Classifier.hai.form = "杯"
• Japanese.Classifier.rin.form = "輪"
• Japanese.Classifier.kumi.form = "組"
• Japanese.Classifier.daasu.form = "ダース"

def Japanese.Classifier.romaji : Classifier → String

Hepburn romanization of the classifier.

Equations

• Japanese.Classifier.tsu.romaji = "tsu"
• Japanese.Classifier.nin.romaji = "nin"
• Japanese.Classifier.mei.romaji = "mei"
• Japanese.Classifier.hiki.romaji = "hiki"
• Japanese.Classifier.tou.romaji = "tou"
• Japanese.Classifier.hon.romaji = "hon"
• Japanese.Classifier.mai.romaji = "mai"
• Japanese.Classifier.ko.romaji = "ko"
• Japanese.Classifier.satsu.romaji = "satsu"
• Japanese.Classifier.tsubu.romaji = "tsubu"
• Japanese.Classifier.dai.romaji = "dai"
• Japanese.Classifier.kenBuilding.romaji = "ken"
• Japanese.Classifier.kenIncident.romaji = "ken"
• Japanese.Classifier.ki.romaji = "ki"
• Japanese.Classifier.ku.romaji = "ku"
• Japanese.Classifier.kyoku.romaji = "kyoku"
• Japanese.Classifier.mon.romaji = "mon"
• Japanese.Classifier.mune.romaji = "mune"
• Japanese.Classifier.seki.romaji = "seki"
• Japanese.Classifier.soku.romaji = "soku"
• Japanese.Classifier.soo.romaji = "soo"
• Japanese.Classifier.ten.romaji = "ten"
• Japanese.Classifier.toori.romaji = "toori"
• Japanese.Classifier.tsuu.romaji = "tsuu"
• Japanese.Classifier.kabu.romaji = "kabu"
• Japanese.Classifier.shoku.romaji = "shoku"
• Japanese.Classifier.teki.romaji = "teki"
• Japanese.Classifier.sao.romaji = "sao"
• Japanese.Classifier.wa.romaji = "wa"
• Japanese.Classifier.furi.romaji = "furi"
• Japanese.Classifier.zen.romaji = "zen"
• Japanese.Classifier.kyaku.romaji = "kyaku"
• Japanese.Classifier.hai.romaji = "hai"
• Japanese.Classifier.rin.romaji = "rin"
• Japanese.Classifier.kumi.romaji = "kumi"
• Japanese.Classifier.daasu.romaji = "daasu"

def Japanese.Classifier.gloss : Classifier → String

A short English gloss describing the classifier's selection criterion.

Equations

• Japanese.Classifier.tsu.gloss = "general"
• Japanese.Classifier.nin.gloss = "person"
• Japanese.Classifier.mei.gloss = "person.formal"
• Japanese.Classifier.hiki.gloss = "small.animal"
• Japanese.Classifier.tou.gloss = "large.animal"
• Japanese.Classifier.hon.gloss = "long.thin"
• Japanese.Classifier.mai.gloss = "flat.thin"
• Japanese.Classifier.ko.gloss = "small.round"
• Japanese.Classifier.satsu.gloss = "bound.volume"
• Japanese.Classifier.tsubu.gloss = "grain"
• Japanese.Classifier.dai.gloss = "machine/vehicle"
• Japanese.Classifier.kenBuilding.gloss = "building"
• Japanese.Classifier.kenIncident.gloss = "incident"
• Japanese.Classifier.ki.gloss = "air.vehicle"
• Japanese.Classifier.ku.gloss = "poem"
• Japanese.Classifier.kyoku.gloss = "music.piece"
• Japanese.Classifier.mon.gloss = "question"
• Japanese.Classifier.mune.gloss = "building.roof"
• Japanese.Classifier.seki.gloss = "large.boat"
• Japanese.Classifier.soku.gloss = "footwear.pair"
• Japanese.Classifier.soo.gloss = "small.boat"
• Japanese.Classifier.ten.gloss = "point/item"
• Japanese.Classifier.toori.gloss = "method/way"
• Japanese.Classifier.tsuu.gloss = "letter/document"
• Japanese.Classifier.kabu.gloss = "rooted.plant"
• Japanese.Classifier.shoku.gloss = "meal"
• Japanese.Classifier.teki.gloss = "drop"
• Japanese.Classifier.sao.gloss = "pole"
• Japanese.Classifier.wa.gloss = "bird"
• Japanese.Classifier.furi.gloss = "sword"
• Japanese.Classifier.zen.gloss = "tray/chopsticks"
• Japanese.Classifier.kyaku.gloss = "legged.furniture"
• Japanese.Classifier.hai.gloss = "cupful"
• Japanese.Classifier.rin.gloss = "flower"
• Japanese.Classifier.kumi.gloss = "pair/group"
• Japanese.Classifier.daasu.gloss = "dozen"

§2: Semantic parameters and shape

def Japanese.Classifier.encodes : Classifier → List Classifier.Parameter

The semantic parameters this classifier encodes ([aikhenvald-2000] typological vocabulary).

Every constructor has an explicit arm; no fall-through. Adding a classifier requires deciding what it encodes — the type checker enforces it.

Equations

• Japanese.Classifier.tsu.encodes = []
• Japanese.Classifier.nin.encodes = [Classifier.Parameter.humanness]
• Japanese.Classifier.mei.encodes = [Classifier.Parameter.humanness, Classifier.Parameter.register]
• Japanese.Classifier.hiki.encodes = [Classifier.Parameter.animacy, Classifier.Parameter.size]
• Japanese.Classifier.tou.encodes = [Classifier.Parameter.animacy, Classifier.Parameter.size]
• Japanese.Classifier.wa.encodes = [Classifier.Parameter.animacy]
• Japanese.Classifier.hon.encodes = [Classifier.Parameter.shape]
• Japanese.Classifier.mai.encodes = [Classifier.Parameter.shape]
• Japanese.Classifier.ko.encodes = [Classifier.Parameter.shape]
• Japanese.Classifier.satsu.encodes = [Classifier.Parameter.shape]
• Japanese.Classifier.tsubu.encodes = [Classifier.Parameter.shape]
• Japanese.Classifier.sao.encodes = [Classifier.Parameter.shape]
• Japanese.Classifier.rin.encodes = [Classifier.Parameter.shape, Classifier.Parameter.boundedness]
• Japanese.Classifier.dai.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.kenBuilding.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.kenIncident.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.ki.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.ku.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.kyoku.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.mon.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.mune.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.seki.encodes = [Classifier.Parameter.function, Classifier.Parameter.size]
• Japanese.Classifier.soku.encodes = [Classifier.Parameter.function, Classifier.Parameter.arrangement]
• Japanese.Classifier.soo.encodes = [Classifier.Parameter.function, Classifier.Parameter.size]
• Japanese.Classifier.ten.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.toori.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.tsuu.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.kabu.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.furi.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.zen.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.kyaku.encodes = [Classifier.Parameter.function]
• Japanese.Classifier.hai.encodes = [Classifier.Parameter.quanta]
• Japanese.Classifier.shoku.encodes = [Classifier.Parameter.quanta]
• Japanese.Classifier.teki.encodes = [Classifier.Parameter.quanta]
• Japanese.Classifier.daasu.encodes = [Classifier.Parameter.quanta]
• Japanese.Classifier.kumi.encodes = [Classifier.Parameter.arrangement, Classifier.Parameter.quanta]

def Japanese.Classifier.shapeDim : Classifier → Option Classifier.Dimension

Shape dimensionality sub-classification per [allan-1977]'s 1D/2D/3D scheme (cf. [downing-1996]). Only meaningful when encodes includes .shape.

-rin 輪 is left as none: although it encodes shape, it tracks boundedness/ring-form (wheels, single blossoms) rather than fitting cleanly on the 1D/2D/3D axis. See encodes, where -rin carries .shape and .boundedness.

Equations

• Japanese.Classifier.hon.shapeDim = some Classifier.Dimension.oneD
• Japanese.Classifier.sao.shapeDim = some Classifier.Dimension.oneD
• Japanese.Classifier.mai.shapeDim = some Classifier.Dimension.twoD
• Japanese.Classifier.satsu.shapeDim = some Classifier.Dimension.twoD
• Japanese.Classifier.ko.shapeDim = some Classifier.Dimension.threeD
• Japanese.Classifier.tsubu.shapeDim = some Classifier.Dimension.threeD
• x✝.shapeDim = none

§3: Property predicates

def Japanese.Classifier.IsMensural (c : Classifier) : Prop

A classifier is mensural if it counts entities by a measure (containers, portions, drops, fixed-quantity multiples) rather than by atomic instances. -daasu ダース (← English "dozen") is mensural since it counts in fixed groups of 12.

Equations

• c.IsMensural = (c = Japanese.Classifier.hai ∨ c = Japanese.Classifier.shoku ∨ c = Japanese.Classifier.teki ∨ c = Japanese.Classifier.daasu)

@[instance_reducible]

instance Japanese.Classifier.instDecidablePredIsMensural : DecidablePred IsMensural

Equations

• c.instDecidablePredIsMensural = Japanese.Classifier.instDecidablePredIsMensural._aux_1 c

def Japanese.Classifier.IsDefault (c : Classifier) : Prop

A classifier is the default (semantically bleached, residue) classifier of the language. Japanese: tsu.

Equations

• c.IsDefault = (c = Japanese.Classifier.tsu)

@[instance_reducible]

instance Japanese.Classifier.instDecidablePredIsDefault : DecidablePred IsDefault

Equations

• c.instDecidablePredIsDefault = Japanese.Classifier.instDecidablePredIsDefault._aux_1 c

def Japanese.Classifier.Encodes (c : Classifier) (p : Classifier.Parameter) : Prop

c encodes the semantic parameter p iff p ∈ c.encodes.

Equations

• c.Encodes p = (p ∈ c.encodes)

@[instance_reducible]

instance Japanese.Classifier.instDecidableEncodes (c : Classifier) (p : Classifier.Parameter) : Decidable (c.Encodes p)

Equations

• c.instDecidableEncodes p = Japanese.Classifier.instDecidableEncodes._aux_1 c p

§4: Lookup and aggregations

def Japanese.Classifier.defaultClassifier? : Option Classifier

The default classifier of Japanese, derived from IsDefault.

Equations

• Japanese.Classifier.defaultClassifier? = List.find? (fun (c : Japanese.Classifier) => decide c.IsDefault) Japanese.Classifier.all

def Japanese.Classifier.lookup (s : String) : Option Classifier

Lookup a classifier by surface form. Returns none if the form is not in the inventory.

Equations

• Japanese.Classifier.lookup s = List.find? (fun (c : Japanese.Classifier) => decide (c.form = s)) Japanese.Classifier.all

def Japanese.Classifier.allEncodedParams : List Classifier.Parameter

The list of all semantic parameters encoded by some classifier in the inventory (with duplicates removed), the system's classifierSemantics.

Equations

• Japanese.Classifier.allEncodedParams = (List.flatMap Japanese.Classifier.encodes Japanese.Classifier.all).eraseDups

§6: Structural theorems

theorem Japanese.Classifier.inventory_size : all.length = 36

The inventory has 36 classifiers (27 core + 6 extended + 3 additions).

theorem Japanese.Classifier.default_eq_tsu : defaultClassifier? = some tsu

The default classifier exists and is tsu.

theorem Japanese.Classifier.isDefault_iff_tsu (c : Classifier) : c.IsDefault ↔ c = tsu

tsu is the only classifier flagged as default.

theorem Japanese.Classifier.mensural_count : (List.filter (fun (c : Classifier) => decide c.IsMensural) all).length = 4

Exactly four classifiers are mensural: hai, shoku, teki, daasu.

theorem Japanese.Classifier.specific_classifiers_have_semantics (c : Classifier) : ¬c.IsDefault → ¬c.IsMensural → c.encodes ≠ []

Every non-default sortal classifier encodes at least one semantic parameter. The default tsu is the only semantically empty classifier.

theorem Japanese.Classifier.all_dimensions_attested : (∃ (c : Classifier), c.shapeDim = some Classifier.Dimension.oneD) ∧ (∃ (c : Classifier), c.shapeDim = some Classifier.Dimension.twoD) ∧ ∃ (c : Classifier), c.shapeDim = some Classifier.Dimension.threeD

All three shape dimensions are attested in the inventory.

theorem Japanese.Classifier.ken_disambiguation : kenBuilding.form ≠ kenIncident.form

軒 kenBuilding and 件 kenIncident are distinct classifiers sharing the same Hepburn romanization but differing in kanji form.

theorem Japanese.Classifier.ken_homophony : kenBuilding.romaji = kenIncident.romaji

軒 and 件 share their romanization (the homophony Downing flags).

Typological parameters

def Japanese.classifierLocus : Classifier.Scope

Classifiers occur in the numeral phrase and characterize the head noun.

Equations

• Japanese.classifierLocus = Classifier.Scope.numeralNP

def Japanese.classifierConstituent : Classifier.Constituent

Equations

• Japanese.classifierConstituent = Classifier.Constituent.headNoun

@[reducible, inline]

abbrev Japanese.classifierKind : Option Classifier.Kind

The kind of device, read off its locus and the constituent it characterizes.

Equations

• Japanese.classifierKind = Classifier.kind Japanese.classifierLocus Japanese.classifierConstituent

def Japanese.classifierScopes : List Classifier.Scope

Every environment the device operates in.

Equations

• Japanese.classifierScopes = [Classifier.Scope.numeralNP]

def Japanese.classifierAssignment : Classifier.Assignment

Classifier choice is semantic.

Equations

• Japanese.classifierAssignment = Classifier.Assignment.semantic

def Japanese.classifierRealizations : List Classifier.Realization

Suffixes on numerals.

Equations

• Japanese.classifierRealizations = [Classifier.Realization.suffix]

def Japanese.classifierAgreement : Bool

Equations

• Japanese.classifierAgreement = false

def Japanese.classifierObligatory : Bool

Equations

• Japanese.classifierObligatory = true

def Japanese.classifierDefault : Bool

Whether the inventory has a general classifier.

Equations

• Japanese.classifierDefault = Japanese.Classifier.defaultClassifier?.isSome

def Japanese.classifierSemantics : List Classifier.Parameter

Equations

• Japanese.classifierSemantics = Japanese.Classifier.allEncodedParams

def Japanese.obligatoryNumber : Bool

Equations

• Japanese.obligatoryNumber = false