Norwegian conjugation

This file defines the stem of a Norwegian verb and builds it from the infinitive by the weak classes of Faarlund, Lie and Vannebo's reference grammar, in either written standard. A stem is the infinitive, the present, the preterite and the past participle. The classes differ in the preterite and the participle, and the grammar draws the line between them there. A weak verb of the first class, the largest and the productive one, has one form for both: in Bokmål -et on the root, kaste, kaster, kastet, kastet, with -a as a rarer written variant, and in Nynorsk -a, with the present in -ar, kaste, kastar, kasta, kasta. A weak verb of the second class has a dental in both, and the dental of the participle is that of the preterite, in both standards alike: -te and -t after most stems, reiste, reist, -de and -d after a stem in a voiced -d, -g or -v or in the diphthongs -ei and -øy, levde, levd, and -dde and -dd after a stem in a single stressed vowel, rodde, rodd. The present of a second-class verb, and of a Bokmål first-class verb, is the infinitive with -r: -er on the root of an infinitive in -e, -r on a stem in a stressed vowel. A double consonant at the end of the stem is written single before the dental endings, kjenne, kjente, bygge, bygde. A strong verb, or a weak verb with a vowel change such as sette, satte, satt, is given by its four forms.

Main definitions

• Norwegian.Standard: the written standards, Bokmål and Nynorsk.
• Norwegian.Conjugation.Stem: the infinitive, present, preterite and past participle.
• Norwegian.Conjugation.weak1, dental, weak2a, weak2b, weak2c: the stem of a weak verb of each class, from its infinitive, the first class by standard.

Main results

• Norwegian.Conjugation.weak1_preterite_eq_participle, dental_preterite, weak2c_preterite: the first class has one form for the preterite and the participle, and the second class the participle with -e.
• Norwegian.Conjugation.weak1_present, dental_present: the present is -er on the root.

Implementation notes

The rules read the spelling. The -a variant of the Bokmål first class, the Nynorsk side forms of the second class with -t in the participle, the Nynorsk fourth subclass with a bare present and a vowel change, telje, tel, talde, talt, and the agreement of a Nynorsk participle after vere and verte are not covered. A verb whose stressed vowel is e, as kle, is a second-class verb in -dde by weak2c, which does not take the final -e for an infinitive ending.

References

• [FLV97]

inductive Norwegian.Standard : Type

The written standards of Norwegian.

• bokmaal : Standard
• nynorsk : Standard

@[instance_reducible]

instance Norwegian.instDecidableEqStandard : DecidableEq Standard

Equations

• Norwegian.instDecidableEqStandard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Norwegian.instReprStandard.repr : Standard → ℕ → Std.Format

Equations

• Norwegian.instReprStandard.repr Norwegian.Standard.bokmaal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Norwegian.Standard.bokmaal")).group prec✝
• Norwegian.instReprStandard.repr Norwegian.Standard.nynorsk prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Norwegian.Standard.nynorsk")).group prec✝

@[instance_reducible]

instance Norwegian.instReprStandard : Repr Standard

Equations

• Norwegian.instReprStandard = { reprPrec := Norwegian.instReprStandard.repr }

@[instance_reducible]

instance Norwegian.instFintypeStandard : Fintype Standard

Equations

• Norwegian.instFintypeStandard = { elems := { val := ↑Norwegian.Standard.enumList, nodup := Norwegian.Standard.enumList_nodup }, complete := Norwegian.instFintypeStandard._proof_1 }

structure Norwegian.Conjugation.Stem : Type

The stem of a verb is its infinitive, its present, its preterite and its past participle.

• infinitive : String

  The infinitive.

• present : String

  The present.

• preterite : String

  The preterite.

• participle : String

  The past participle.

def Norwegian.Conjugation.instDecidableEqStem.decEq (x✝ x✝¹ : Stem) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Norwegian.Conjugation.instDecidableEqStem : DecidableEq Stem

Equations

• Norwegian.Conjugation.instDecidableEqStem = Norwegian.Conjugation.instDecidableEqStem.decEq

@[instance_reducible]

instance Norwegian.Conjugation.instReprStem : Repr Stem

Equations

• Norwegian.Conjugation.instReprStem = { reprPrec := Norwegian.Conjugation.instReprStem.repr }

def Norwegian.Conjugation.instReprStem.repr : Stem → ℕ → Std.Format

Equations

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

def Norwegian.Conjugation.root (inf : String) : String

root inf is the root of the infinitive inf, the infinitive less a final -e.

Equations

• Norwegian.Conjugation.root inf = match inf.toList.reverse with | 'e' :: r => String.ofList r.reverse | x => inf

@[simp]

theorem Norwegian.Conjugation.root_append_e (s : String) : root (s ++ "e") = s

def Norwegian.Conjugation.dentalStem (inf : String) : String

dentalStem inf is the root of inf with a final double consonant written single, the stem the dental endings of the second class attach to, kjenn to kjen.

Equations

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

def Norwegian.Conjugation.weak1 : Standard → String → Stem

weak1 s inf is the stem of a weak verb of the first class in the standard s, with one form for the preterite and the participle: in Bokmål -et on the root, kaste, kaster, kastet, kastet, in Nynorsk -a, with the present in -ar, kaste, kastar, kasta, kasta.

Equations

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

def Norwegian.Conjugation.dental (d inf : String) : Stem

dental d inf is the stem of a weak verb of the second class with the dental d, the preterite in d with -e and the participle in d, on the stem written with a single final consonant.

Equations

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

@[reducible, inline]

abbrev Norwegian.Conjugation.weak2a : String → Stem

weak2a inf is the stem of a weak verb of the second class with the preterite in -te and the participle in -t, as reise, reiser, reiste, reist.

Equations

• Norwegian.Conjugation.weak2a = Norwegian.Conjugation.dental "t"

@[reducible, inline]

abbrev Norwegian.Conjugation.weak2b : String → Stem

weak2b inf is the stem of a weak verb of the second class with the preterite in -de and the participle in -d, as leve, lever, levde, levd.

Equations

• Norwegian.Conjugation.weak2b = Norwegian.Conjugation.dental "d"

def Norwegian.Conjugation.weak2c (inf : String) : Stem

weak2c inf is the stem of a weak verb of the second class whose stem is the infinitive, ending in a single stressed vowel, with -dde and -dd, as ro, ror, rodde, rodd.

Equations

• Norwegian.Conjugation.weak2c inf = { infinitive := inf, present := inf ++ "r", preterite := inf ++ "dde", participle := inf ++ "dd" }

The forms across the classes

theorem Norwegian.Conjugation.weak1_preterite_eq_participle (s : Standard) (inf : String) : (weak1 s inf).preterite = (weak1 s inf).participle

The verbs of the first class have the same form in the preterite and the participle, in both standards.

theorem Norwegian.Conjugation.dental_preterite (d inf : String) : (dental d inf).preterite = (dental d inf).participle ++ "e"

In the second class the dental of the participle is that of the preterite.

theorem Norwegian.Conjugation.weak2c_preterite (inf : String) : (weak2c inf).preterite = (weak2c inf).participle ++ "e"

theorem Norwegian.Conjugation.weak1_present (s : String) : (weak1 Standard.bokmaal (s ++ "e")).present = s ++ "er"

The present of a Bokmål first-class verb is -er on its root.

theorem Norwegian.Conjugation.dental_present (d s : String) : (dental d (s ++ "e")).present = s ++ "er"

The present of a second-class verb with an infinitive in -e is -er on its root.