Korean converbs

Korean chains clauses with conjunctive suffixes, Sohn's term for its converbs, on the nonfinite verb of each medial clause before a single final verb, without switch-reference. The nonfinite verb keeps its voice, subject-honorific and tense slots but takes no sentence ender. -go 'and' coordinates, -go(seo), -eoseo, -jamaja and -daga sequence events, -myeonseo 'while' marks simultaneity, -eoseo, -(eu)ni and -(eu)nikka give the reason, -(eu)myeon 'if' conditions, -jiman, -(eu)na and -eodo concede, -dorok gives a result or limit, -(eu)ryeogo and -(eu)reo the purpose, -neunde background, and -geona and -deunji 'or' disjoin. Tense before a suffix is relative to the final verb; some suffixes admit the past -eoss and the modal -gess before them and others exclude both. The negative adverbs and the negative verb occur in a medial clause, governed by the sentence type of the final clause. Forms are in the Revised Romanization; Sohn writes -ko, -e(se), -(u)myense, -(u)nikka, -ciman, -tolok, -(u)lyeko, -taka, -ca(maca), -kena.

Implementation notes

• AllowsTense and AllowsModal follow the features Sohn attaches to each conjunctor and, for -geona, -deunji and -jamaja, which his list omits, the attachment statements of the National Institute of Korean Language's dictionary; Sohn marks -tunci as excluding the modal, which the dictionary admits in one of its senses.
• The clause-chaining typology over the converbs is in Studies/SarvasyAikhenvald2025.lean.

References

• [Soh94]
• [Soh99]
• [NIKL16]

inductive Korean.Converb : Type

The conjunctive suffixes.

• go : Converb

  -go 'and', the coordinative suffix, tense before it absolute or relative.

• goseo : Converb

  -go(seo) 'and then', the contracted temporal suffix, also the manner, malaeul tagoseo 'riding a horse'.

• myeonseo : Converb

  -myeonseo 'while', the two events overlapping; the past before it when the medial event comes first.

• eoseo : Converb

  -eoseo 'and then, so, by', the sequence, cause or manner; no past before it.

• myeon : Converb

  -(eu)myeon 'if, when', taking the past for hypothetical readings.

• jiman : Converb

  -jiman 'but, although'.

• na : Converb

  -(eu)na 'but', the formal concessive.

• eodo : Converb

  -eodo 'although, even if, no matter'.

• dorok : Converb

  -dorok 'so that, to the extent that, until', a result, extent or temporal limit; no past before it.

• nikka : Converb

  -(eu)nikka 'because, as, since, when', the reason as the speaker presents it.

• ni : Converb

  -(eu)ni 'since, as, after'.

• neunde : Converb

  -neunde 'given that, and, but', supplying background.

• ryeo : Converb

  -(eu)ryeogo 'intending to'.

• reo : Converb

  -(eu)reo 'in order to'.

• daga : Converb

  -daga 'and then, while', the transferentive, marking alternation when repeated.

• jamaja : Converb

  -jamaja 'as soon as'; no past before it.

• geona : Converb

  -geona 'or'.

• deunji : Converb

  -deunji 'or', beside -geona.

@[instance_reducible]

instance Korean.instDecidableEqConverb : DecidableEq Converb

Equations

• Korean.instDecidableEqConverb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Korean.instReprConverb : Repr Converb

Equations

• Korean.instReprConverb = { reprPrec := Korean.instReprConverb.repr }

def Korean.instReprConverb.repr : Converb → ℕ → Std.Format

Equations

• Korean.instReprConverb.repr Korean.Converb.go prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.go")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.goseo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.goseo")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.myeonseo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.myeonseo")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.eoseo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.eoseo")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.myeon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.myeon")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.jiman prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.jiman")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.na prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.na")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.eodo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.eodo")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.dorok prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.dorok")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.nikka prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.nikka")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.ni prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.ni")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.neunde prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.neunde")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.ryeo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.ryeo")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.reo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.reo")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.daga prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.daga")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.jamaja prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.jamaja")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.geona prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.geona")).group prec✝
• Korean.instReprConverb.repr Korean.Converb.deunji prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Converb.deunji")).group prec✝

@[instance_reducible]

instance Korean.instFintypeConverb : Fintype Converb

Equations

• Korean.instFintypeConverb = { elems := { val := ↑Korean.Converb.enumList, nodup := Korean.Converb.enumList_nodup }, complete := Korean.instFintypeConverb._proof_1 }

def Korean.Converb.morphs : Converb → List Morphology.Morph

The morphs of a converb.

Equations

• Korean.Converb.go.morphs = [Morphology.Morph.suff "go"]
• Korean.Converb.goseo.morphs = [Morphology.Morph.suff "go(seo)"]
• Korean.Converb.myeonseo.morphs = [Morphology.Morph.suff "myeonseo"]
• Korean.Converb.eoseo.morphs = [Morphology.Morph.suff "eoseo"]
• Korean.Converb.myeon.morphs = [Morphology.Morph.suff "(eu)myeon"]
• Korean.Converb.jiman.morphs = [Morphology.Morph.suff "jiman"]
• Korean.Converb.na.morphs = [Morphology.Morph.suff "(eu)na"]
• Korean.Converb.eodo.morphs = [Morphology.Morph.suff "eodo"]
• Korean.Converb.dorok.morphs = [Morphology.Morph.suff "dorok"]
• Korean.Converb.nikka.morphs = [Morphology.Morph.suff "(eu)nikka"]
• Korean.Converb.ni.morphs = [Morphology.Morph.suff "(eu)ni"]
• Korean.Converb.neunde.morphs = [Morphology.Morph.suff "neunde"]
• Korean.Converb.ryeo.morphs = [Morphology.Morph.suff "(eu)ryeogo"]
• Korean.Converb.reo.morphs = [Morphology.Morph.suff "(eu)reo"]
• Korean.Converb.daga.morphs = [Morphology.Morph.suff "daga"]
• Korean.Converb.jamaja.morphs = [Morphology.Morph.suff "jamaja"]
• Korean.Converb.geona.morphs = [Morphology.Morph.suff "geona"]
• Korean.Converb.deunji.morphs = [Morphology.Morph.suff "deunji"]

def Korean.Converb.form (c : Converb) : String

The form of a converb in boundary notation.

Equations

• c.form = Morphology.Morph.surface c.morphs

def Korean.Converb.gloss : Converb → String

The gloss.

Equations

• Korean.Converb.go.gloss = "and"
• Korean.Converb.goseo.gloss = "and then"
• Korean.Converb.myeonseo.gloss = "while"
• Korean.Converb.eoseo.gloss = "and then, so, by"
• Korean.Converb.myeon.gloss = "if, when"
• Korean.Converb.jiman.gloss = "but, although"
• Korean.Converb.na.gloss = "but"
• Korean.Converb.eodo.gloss = "although, even if"
• Korean.Converb.dorok.gloss = "so that, to the extent that, until"
• Korean.Converb.nikka.gloss = "because, as, since, when"
• Korean.Converb.ni.gloss = "since, as, after"
• Korean.Converb.neunde.gloss = "given that, and, but"
• Korean.Converb.ryeo.gloss = "intending to"
• Korean.Converb.reo.gloss = "in order to"
• Korean.Converb.daga.gloss = "and then, while"
• Korean.Converb.jamaja.gloss = "as soon as"
• Korean.Converb.geona.gloss = "or"
• Korean.Converb.deunji.gloss = "or"

def Korean.Converb.relations : Converb → Finset Clause.Chaining.InterclauseRelation

The interclausal relations a converb encodes.

Equations

• Korean.Converb.go.relations = {Clause.Chaining.InterclauseRelation.additive}
• Korean.Converb.goseo.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.manner}
• Korean.Converb.myeonseo.relations = {Clause.Chaining.InterclauseRelation.simultaneous}
• Korean.Converb.eoseo.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.causal, Clause.Chaining.InterclauseRelation.manner}
• Korean.Converb.myeon.relations = {Clause.Chaining.InterclauseRelation.conditional}
• Korean.Converb.jiman.relations = {Clause.Chaining.InterclauseRelation.concessive}
• Korean.Converb.na.relations = {Clause.Chaining.InterclauseRelation.concessive}
• Korean.Converb.eodo.relations = {Clause.Chaining.InterclauseRelation.concessive}
• Korean.Converb.dorok.relations = {Clause.Chaining.InterclauseRelation.purpose}
• Korean.Converb.ryeo.relations = {Clause.Chaining.InterclauseRelation.purpose}
• Korean.Converb.reo.relations = {Clause.Chaining.InterclauseRelation.purpose}
• Korean.Converb.nikka.relations = {Clause.Chaining.InterclauseRelation.causal}
• Korean.Converb.ni.relations = {Clause.Chaining.InterclauseRelation.causal, Clause.Chaining.InterclauseRelation.sequential}
• Korean.Converb.neunde.relations = {Clause.Chaining.InterclauseRelation.additive, Clause.Chaining.InterclauseRelation.concessive}
• Korean.Converb.daga.relations = {Clause.Chaining.InterclauseRelation.sequential, Clause.Chaining.InterclauseRelation.simultaneous}
• Korean.Converb.jamaja.relations = {Clause.Chaining.InterclauseRelation.sequential}
• Korean.Converb.geona.relations = ∅
• Korean.Converb.deunji.relations = ∅

def Korean.Converb.AllowsTense (c : Converb) : Prop

The past or perfect may be marked on the medial verb before the converb; before -myeonseo only in its concessive reading.

Equations

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

@[instance_reducible]

instance Korean.Converb.instDecidablePredAllowsTense : DecidablePred AllowsTense

Equations

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

def Korean.Converb.AllowsModal (c : Converb) : Prop

The modal -gess may be marked on the medial verb before the converb; before -myeonseo only in its concessive reading.

Equations

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

@[instance_reducible]

instance Korean.Converb.instDecidablePredAllowsModal : DecidablePred AllowsModal

Equations

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

theorem Korean.Converb.allowsModal_imp_allowsTense (c : Converb) : c.AllowsModal → c.AllowsTense

A converb admitting the modal admits the past, since the clauses that exclude the past exclude every mood suffix.

def Korean.Converb.verbForm : Converb → UD.VerbForm

The verb form of a converb.

Equations

• x✝.verbForm = UD.VerbForm.Conv

@[instance_reducible]

instance Korean.Converb.instMedialForm : Clause.Chaining.MedialForm Converb

The converbs as medial forms, neutral to switch-reference, encoding their relations, and never indexing the subject.

Equations

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