Mandarin resultative compounds

A Mandarin V-V resultative compound pairs a verb describing the causing event with a verb describing its result: dǎ-pò 打破 'hit-break', kū-lèi 哭累 'cry-tired'. This file enters the component verbs and the compounds built from them, so a compound's argument structure is read off its verbs rather than stipulated: the result verb of every entry is monovalent, a change-of-state verb such as pò 'break' or a stative such as lèi 'tired' (valency_v2). Which argument the result is predicated of is not a property of the entry: zhuī-lèi 'chase-tired' with an object is read with either the chaser or the chased tired, so orientation belongs to a sentence, and the studies state it about the sentences they analyze. Tay's account of the compounds as words built in morphology lives in Studies/Tay2024.lean.

Main definitions

• Mandarin.Resultative — a V-V resultative compound, its causing verb and its result verb.
• Mandarin.Resultative.tree — the compound as a root compound of its verbs.
• Mandarin.resultatives — the inventory of the entries.

References

• [Tay24]

Component verbs

def Mandarin.da : Verb

打 dǎ 'hit'.

Equations

• Mandarin.da = { valency := Verb.Valency.ofFrame ArgumentFrame.np, vendlerClass := some Aspect.VendlerClass.activity, morphs := [Morphology.Morph.root "dǎ"], hanzi := "打" }

def Mandarin.ku : Verb

哭 kū 'cry'.

Equations

• Mandarin.ku = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.activity, morphs := [Morphology.Morph.root "kū"], hanzi := "哭" }

def Mandarin.chi : Verb

吃 chī 'eat'.

Equations

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

def Mandarin.he : Verb

喝 hē 'drink'.

Equations

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

def Mandarin.tui : Verb

推 tuī 'push'.

Equations

• Mandarin.tui = { valency := Verb.Valency.ofFrame ArgumentFrame.np, vendlerClass := some Aspect.VendlerClass.activity, morphs := [Morphology.Morph.root "tuī"], hanzi := "推" }

def Mandarin.zhui : Verb

追 zhuī 'chase'.

Equations

• Mandarin.zhui = { valency := Verb.Valency.ofFrame ArgumentFrame.np, vendlerClass := some Aspect.VendlerClass.activity, morphs := [Morphology.Morph.root "zhuī"], hanzi := "追" }

def Mandarin.she : Verb

射 shè 'shoot'.

Equations

• Mandarin.she = { valency := Verb.Valency.ofFrame ArgumentFrame.np, vendlerClass := some Aspect.VendlerClass.activity, morphs := [Morphology.Morph.root "shè"], hanzi := "射" }

def Mandarin.po : Verb

破 pò 'break', intransitive.

Equations

• Mandarin.po = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.achievement, morphs := [Morphology.Morph.root "pò"], hanzi := "破" }

def Mandarin.si : Verb

死 sǐ 'die'.

Equations

• Mandarin.si = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.achievement, morphs := [Morphology.Morph.root "sǐ"], hanzi := "死" }

def Mandarin.kai : Verb

开 kāi 'open', intransitive.

Equations

• Mandarin.kai = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.achievement, morphs := [Morphology.Morph.root "kāi"], hanzi := "开" }

def Mandarin.lei : Verb

累 lèi 'tired'.

Equations

• Mandarin.lei = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.state, morphs := [Morphology.Morph.root "lèi"], hanzi := "累" }

def Mandarin.bao : Verb

饱 bǎo 'full'.

Equations

• Mandarin.bao = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.state, morphs := [Morphology.Morph.root "bǎo"], hanzi := "饱" }

def Mandarin.shi : Verb

湿 shī 'wet'.

Equations

• Mandarin.shi = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.state, morphs := [Morphology.Morph.root "shī"], hanzi := "湿" }

def Mandarin.zui : Verb

醉 zuì 'drunk'.

Equations

• Mandarin.zui = { valency := Verb.Valency.ofFrame ArgumentFrame.intransitive, vendlerClass := some Aspect.VendlerClass.state, morphs := [Morphology.Morph.root "zuì"], hanzi := "醉" }

Compounds

structure Mandarin.Resultative : Type

A V-V resultative compound: a verb describing the causing event and a verb describing its result.

• v1 : Verb

  The first verb, describing the causing event.

• v2 : Verb

  The second verb, describing the result.

def Mandarin.instBEqResultative.beq : Resultative → Resultative → Bool

Equations

• Mandarin.instBEqResultative.beq { v1 := a, v2 := a_1 } { v1 := b, v2 := b_1 } = (a == b && a_1 == b_1)
• Mandarin.instBEqResultative.beq x✝¹ x✝ = false

@[instance_reducible]

instance Mandarin.instBEqResultative : BEq Resultative

Equations

• Mandarin.instBEqResultative = { beq := Mandarin.instBEqResultative.beq }

def Mandarin.da_po : Resultative

dǎ-pò 打破 'hit-break', 'break by hitting', Tay's (668).

Equations

• Mandarin.da_po = { v1 := Mandarin.da, v2 := Mandarin.po }

def Mandarin.she_si : Resultative

shè-sǐ 射死 'shoot-die', 'shoot dead', Tay's (107).

Equations

• Mandarin.she_si = { v1 := Mandarin.she, v2 := Mandarin.si }

def Mandarin.tui_kai : Resultative

tuī-kāi 推开 'push-open', Tay's (60).

Equations

• Mandarin.tui_kai = { v1 := Mandarin.tui, v2 := Mandarin.kai }

def Mandarin.ku_lei : Resultative

kū-lèi 哭累 'cry-tired', 'cry oneself tired', Tay's (219).

Equations

• Mandarin.ku_lei = { v1 := Mandarin.ku, v2 := Mandarin.lei }

def Mandarin.ku_shi : Resultative

kū-shī 哭湿 'cry-wet', 'become wet from crying', Tay's (221).

Equations

• Mandarin.ku_shi = { v1 := Mandarin.ku, v2 := Mandarin.shi }

def Mandarin.zhui_lei : Resultative

zhuī-lèi 追累 'chase-tired', read with either the chaser or the chased tired, Tay's (362) after Li.

Equations

• Mandarin.zhui_lei = { v1 := Mandarin.zhui, v2 := Mandarin.lei }

def Mandarin.chi_bao : Resultative

chī-bǎo 吃饱 'eat-full', 'become full from eating', Tay's (3).

Equations

• Mandarin.chi_bao = { v1 := Mandarin.chi, v2 := Mandarin.bao }

def Mandarin.he_zui : Resultative

hē-zuì 喝醉 'drink-drunk', 'drink oneself drunk', Tay's (360).

Equations

• Mandarin.he_zui = { v1 := Mandarin.he, v2 := Mandarin.zui }

def Mandarin.resultatives : List Resultative

The inventory of the compounds.

Equations

• Mandarin.resultatives = [Mandarin.da_po, Mandarin.she_si, Mandarin.tui_kai, Mandarin.ku_lei, Mandarin.ku_shi, Mandarin.zhui_lei, Mandarin.chi_bao, Mandarin.he_zui]

def Mandarin.Resultative.tree (c : Resultative) : Morphology.Word.Tree Verb

The compound as a root compound of its two verbs.

Equations

• c.tree = (Morphology.Word.Tree.root c.v1).compound (Morphology.Word.Tree.root c.v2)

@[simp]

theorem Mandarin.Resultative.toList_tree (c : Resultative) : c.tree.toList = [c.v1, c.v2]

theorem Mandarin.Resultative.valency_v2 (c : Resultative) : c ∈ resultatives → ∀ fr ∈ c.v2.valency.frames, fr.valency = 1

The result verb of every compound is monovalent.