Norwegian verbs

This file defines the Bokmål verb as a lexical entry, the root Verb with its stem and its formation, simplex or a verb phrase with a verbal particle. Faarlund, Lie and Vannebo's reference grammar calls a preposition without a complement that goes with a verb a verbal particle, kaste bort 'throw away', and describes the relation of such a verb phrase to the compound verb with the same particle as its first member, bortkaste. The past participle takes the compound form more readily than the other forms, and where the verb is otherwise a verb phrase the compound participle is used attributively, en oppgjort sak, and after være and bli, Saka er oppgjort 'the matter is settled', while after ha and få the participle stays a verb phrase, Vi har gjort opp saka 'we have settled the matter'. The entries are the particle verbs whose participles the grammar lists and those of den Dikken's Norwegian examples, with the simplex verbs they are formed on, conjugated by the grammar's classes.

Main definitions

• Norwegian.Verb: the entry, the root Verb with its stem and its formation.
• Norwegian.ParticipleContext, Norwegian.ParticipleContext.IsCompound: where a participle stands, and the contexts that take the compound form.
• Norwegian.Verb.phraseParticiple, Norwegian.Verb.compoundParticiple, Norwegian.Verb.participle: the participle of the verb phrase, the compound participle, and the one a context takes.
• Norwegian.Verb.transitive, Norwegian.Verb.withParticle: the transitive entry of a stem, and the verb phrase formed on an entry with a verbal particle.
• Norwegian.Verbs.allVerbs, Norwegian.Verbs.Nynorsk.sparkeUt: the Bokmål entries and the Nynorsk one.

Main results

• Norwegian.Verb.participle_eq_compoundParticiple, participle_of_simplex: the contexts that take the compound participle, and a simplex verb's one participle.
• Norwegian.Verbs.grammar_compound_participles, Norwegian.Verbs.gjoereOpp_participle: the compound participles the grammar lists come out of the rule, and gjøre opp has the grammar's two participles.

Implementation notes

The entries are Bokmål with the -et forms of the first weak class, and Nynorsk sparke for Åfarli's rows in den Dikken's study. His other Nynorsk verbs have no entry: the grammar's lists do not place klippe, and his kjørt is the Bokmål spelling of Nynorsk køyrt. Which verb phrases also exist as compound verbs in all their forms, the grammar's three groups, is not recorded.

References

• [FLV97]
• [dD95]

inductive Norwegian.Formation : Type

A verb is simplex or a verb phrase formed on a simplex verb with a verbal particle.

• simplex : Formation
• particle (form : String) : Formation

@[instance_reducible]

instance Norwegian.instDecidableEqFormation : DecidableEq Formation

Equations

• Norwegian.instDecidableEqFormation = Norwegian.instDecidableEqFormation.decEq

def Norwegian.instDecidableEqFormation.decEq (x✝ x✝¹ : Formation) : Decidable (x✝ = x✝¹)

Equations

• Norwegian.instDecidableEqFormation.decEq Norwegian.Formation.simplex Norwegian.Formation.simplex = isTrue ⋯
• Norwegian.instDecidableEqFormation.decEq Norwegian.Formation.simplex (Norwegian.Formation.particle form) = isFalse ⋯
• Norwegian.instDecidableEqFormation.decEq (Norwegian.Formation.particle form) Norwegian.Formation.simplex = isFalse ⋯
• Norwegian.instDecidableEqFormation.decEq (Norwegian.Formation.particle a) (Norwegian.Formation.particle b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Norwegian.instReprFormation.repr : Formation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Norwegian.instReprFormation : Repr Formation

Equations

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

inductive Norwegian.ParticipleContext : Type

Where a participle stands: after the perfect auxiliaries ha and få, after være and bli, or attributively.

• perfect : ParticipleContext
• copular : ParticipleContext
• attributive : ParticipleContext

@[instance_reducible]

instance Norwegian.instDecidableEqParticipleContext : DecidableEq ParticipleContext

Equations

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

def Norwegian.instReprParticipleContext.repr : ParticipleContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Norwegian.instReprParticipleContext : Repr ParticipleContext

Equations

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

@[instance_reducible]

instance Norwegian.instFintypeParticipleContext : Fintype ParticipleContext

Equations

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

def Norwegian.ParticipleContext.IsCompound (c : ParticipleContext) : Prop

A context takes the compound participle of a verb phrase when it is attributive or after være and bli; after ha and få the participle stays a verb phrase.

Equations

• c.IsCompound = (c ≠ Norwegian.ParticipleContext.perfect)

@[instance_reducible]

instance Norwegian.instDecidablePredParticipleContextIsCompound : DecidablePred ParticipleContext.IsCompound

Equations

• Norwegian.instDecidablePredParticipleContextIsCompound x✝ = { decide := !decide (x✝ = Norwegian.ParticipleContext.perfect), reflects_decide := ⋯ }

structure Norwegian.Verbextends Verb : Type

A Norwegian verb is the root entry with its stem and its formation.

• valency : Valency
• voiceType : Option VoiceType
• passivizable : Bool
• perfectAuxiliaries : Finset PerfectAuxiliary
• vendlerClass : Option Aspect.VendlerClass
• scaleDimension : Option Degree.ScalarDimension
• scalePolarity : Polarity
• direction : Option Spatial.Path.Direction
• incrementality : Option Aspect.Incrementality
• phasal : Option Aspect.Phasal
• factivity : Option Presupposition.Factivity
• implicative : NaturalLogic.ImplicationSignature
• opaqueContext : Bool
• attitude : Option _root_.Attitude
• readings : List Reading
• complementSig : Option NaturalLogic.Signature
• levinClasses : Finset ArgumentStructure.LevinClass
• levinExcluded : Finset ArgumentStructure.LevinClass
• root : Semantics.Root
• morphs : List Morphology.Morph
• speechActVerb : Bool
• senseTag : SenseTag
• stem : Conjugation.Stem

  The stem of the simplex verb.

• formation : Formation

  The formation.

@[instance_reducible]

instance Norwegian.instBEqVerb : BEq Verb

Equations

• Norwegian.instBEqVerb = { beq := Norwegian.instBEqVerb.beq }

def Norwegian.instBEqVerb.beq : Verb → Verb → Bool

Equations

• Norwegian.instBEqVerb.beq { toVerb := a, stem := a_1, formation := a_2 } { toVerb := b, stem := b_1, formation := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Norwegian.instBEqVerb.beq x✝¹ x✝ = false

def Norwegian.Verb.phraseParticiple (v : Verb) : String

The participle of the verb phrase, the simplex participle followed by its particle, gjort opp.

Equations

• v.phraseParticiple = match v.formation with | Norwegian.Formation.simplex => v.stem.participle | Norwegian.Formation.particle p => v.stem.participle ++ " " ++ p

def Norwegian.Verb.compoundParticiple (v : Verb) : String

The compound participle, the particle prefixed to the simplex participle, oppgjort.

Equations

• v.compoundParticiple = match v.formation with | Norwegian.Formation.simplex => v.stem.participle | Norwegian.Formation.particle p => p ++ v.stem.participle

def Norwegian.Verb.participle (v : Verb) : ParticipleContext → String

The participle a context takes: the compound one attributively and after være and bli, the verb phrase after ha and få.

Equations

• v.participle Norwegian.ParticipleContext.perfect = v.phraseParticiple
• v.participle Norwegian.ParticipleContext.copular = v.compoundParticiple
• v.participle Norwegian.ParticipleContext.attributive = v.compoundParticiple

theorem Norwegian.Verb.participle_perfect {v : Verb} : v.participle ParticipleContext.perfect = v.phraseParticiple

theorem Norwegian.Verb.participle_eq_compoundParticiple {v : Verb} {c : ParticipleContext} (h : c.IsCompound) : v.participle c = v.compoundParticiple

theorem Norwegian.Verb.participle_of_simplex {v : Verb} (h : v.formation = Formation.simplex) (c : ParticipleContext) : v.participle c = v.stem.participle

A simplex verb has one participle in every context.

def Norwegian.Verb.transitive (s : Conjugation.Stem) : Verb

transitive s is the transitive entry with the stem s.

Equations

• Norwegian.Verb.transitive s = { valency := Verb.Valency.ofFrame ArgumentFrame.np, morphs := [Morphology.Morph.root s.infinitive], stem := s }

def Norwegian.Verb.withParticle (v : Verb) (p : String) : Verb

v.withParticle p is the verb phrase formed on v with the verbal particle p.

Equations

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

theorem Norwegian.Verb.compoundParticiple_withParticle (v : Verb) (p : String) : (v.withParticle p).compoundParticiple = p ++ v.stem.participle

The compound participle puts the particle before the participle of the simplex verb.

theorem Norwegian.Verb.phraseParticiple_withParticle (v : Verb) (p : String) : (v.withParticle p).phraseParticiple = v.stem.participle ++ " " ++ p

The participle of a verb phrase is that of the simplex verb followed by the particle.

Simplex verbs

def Norwegian.Verbs.kaste : Verb

kaste 'throw', the paradigm verb of the first weak class.

Equations

• Norwegian.Verbs.kaste = Norwegian.Verb.transitive (Norwegian.Conjugation.weak1 Norwegian.Standard.bokmaal "kaste")

def Norwegian.Verbs.sparke : Verb

sparke 'kick', of the first weak class like the other stems in -rk.

Equations

• Norwegian.Verbs.sparke = Norwegian.Verb.transitive (Norwegian.Conjugation.weak1 Norwegian.Standard.bokmaal "sparke")

def Norwegian.Verbs.klippe : Verb

klippe 'cut', of the first weak class like the other stems in -pp.

Equations

• Norwegian.Verbs.klippe = Norwegian.Verb.transitive (Norwegian.Conjugation.weak1 Norwegian.Standard.bokmaal "klippe")

def Norwegian.Verbs.kjoere : Verb

kjøre 'drive', of the second weak class with -te, a stem in a long vowel and a single consonant.

Equations

• Norwegian.Verbs.kjoere = Norwegian.Verb.transitive (Norwegian.Conjugation.weak2a "kjøre")

def Norwegian.Verbs.sende : Verb

sende 'send', of the second weak class with -te, a stem in -nd.

Equations

• Norwegian.Verbs.sende = Norwegian.Verb.transitive (Norwegian.Conjugation.weak2a "sende")

def Norwegian.Verbs.sette : Verb

sette 'set', of the second weak class with -te and a vowel change, satte, satt.

Equations

• Norwegian.Verbs.sette = Norwegian.Verb.transitive { infinitive := "sette", present := "setter", preterite := "satte", participle := "satt" }

def Norwegian.Verbs.gjoere : Verb

gjøre 'do', of the second weak class with -de and a vowel change, gjør, gjorde, gjort.

Equations

• Norwegian.Verbs.gjoere = Norwegian.Verb.transitive { infinitive := "gjøre", present := "gjør", preterite := "gjorde", participle := "gjort" }

def Norwegian.Verbs.bygge : Verb

bygge 'build', of the second weak class with -de, a stem in -gg.

Equations

• Norwegian.Verbs.bygge = Norwegian.Verb.transitive (Norwegian.Conjugation.weak2b "bygge")

def Norwegian.Verbs.leie : Verb

leie 'rent', of the second weak class with -de, a stem in -ei.

Equations

• Norwegian.Verbs.leie = Norwegian.Verb.transitive (Norwegian.Conjugation.weak2b "leie")

def Norwegian.Verbs.kle : Verb

kle 'dress', of the second weak class with -dde, a stem in a single vowel.

Equations

• Norwegian.Verbs.kle = Norwegian.Verb.transitive (Norwegian.Conjugation.weak2c "kle")

Verb phrases with a verbal particle

def Norwegian.Verbs.kasteBort : Verb

kaste bort 'throw away', bortkastet.

Equations

• Norwegian.Verbs.kasteBort = Norwegian.Verbs.kaste.withParticle "bort"

def Norwegian.Verbs.sparkeUt : Verb

sparke ut 'kick out', utsparket.

Equations

• Norwegian.Verbs.sparkeUt = Norwegian.Verbs.sparke.withParticle "ut"

def Norwegian.Verbs.klippeAv : Verb

klippe av 'cut off', avklippet.

Equations

• Norwegian.Verbs.klippeAv = Norwegian.Verbs.klippe.withParticle "av"

def Norwegian.Verbs.kjoereBort : Verb

kjøre bort 'drive away', bortkjørt.

Equations

• Norwegian.Verbs.kjoereBort = Norwegian.Verbs.kjoere.withParticle "bort"

def Norwegian.Verbs.sendeUt : Verb

sende ut 'send out', utsendt.

Equations

• Norwegian.Verbs.sendeUt = Norwegian.Verbs.sende.withParticle "ut"

def Norwegian.Verbs.setteNed : Verb

sette ned 'set down', nedsatt.

Equations

• Norwegian.Verbs.setteNed = Norwegian.Verbs.sette.withParticle "ned"

def Norwegian.Verbs.setteSammen : Verb

sette sammen 'put together', sammensatt.

Equations

• Norwegian.Verbs.setteSammen = Norwegian.Verbs.sette.withParticle "sammen"

def Norwegian.Verbs.gjoereOpp : Verb

gjøre opp 'settle', oppgjort.

Equations

• Norwegian.Verbs.gjoereOpp = Norwegian.Verbs.gjoere.withParticle "opp"

def Norwegian.Verbs.byggeUt : Verb

bygge ut 'expand', utbygd.

Equations

• Norwegian.Verbs.byggeUt = Norwegian.Verbs.bygge.withParticle "ut"

def Norwegian.Verbs.leieUt : Verb

leie ut 'rent out', utleid.

Equations

• Norwegian.Verbs.leieUt = Norwegian.Verbs.leie.withParticle "ut"

def Norwegian.Verbs.klePaa : Verb

kle på 'dress', påkledd.

Equations

• Norwegian.Verbs.klePaa = Norwegian.Verbs.kle.withParticle "på"

def Norwegian.Verbs.allVerbs : List Verb

The entries.

Equations

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

theorem Norwegian.Verbs.grammar_compound_participles : List.map Verb.compoundParticiple [gjoereOpp, klePaa, setteSammen, byggeUt, leieUt, kasteBort] = ["oppgjort", "påkledd", "sammensatt", "utbygd", "utleid", "bortkastet"]

The compound participles the grammar lists for gjøre opp, kle på, sette sammen, bygge ut, leie ut and kaste bort come out of the rule, the last in the -et form of the grammar's en bortkastet dag.

theorem Norwegian.Verbs.gjoereOpp_participle : gjoereOpp.participle ParticipleContext.perfect = "gjort opp" ∧ gjoereOpp.participle ParticipleContext.copular = "oppgjort"

gjøre opp has the grammar's two participles, Vi har gjort opp saka after ha and Saka er oppgjort after være.

Nynorsk

def Norwegian.Verbs.Nynorsk.sparke : Verb

Nynorsk sparke 'kick', of the first weak class, sparka, as in the grammar's Han vart sparka.

Equations

• Norwegian.Verbs.Nynorsk.sparke = Norwegian.Verb.transitive (Norwegian.Conjugation.weak1 Norwegian.Standard.nynorsk "sparke")

def Norwegian.Verbs.Nynorsk.sparkeUt : Verb

Nynorsk sparke ut 'kick out', Åfarli's sparka ut and utsparka.

Equations

• Norwegian.Verbs.Nynorsk.sparkeUt = Norwegian.Verbs.Nynorsk.sparke.withParticle "ut"