German tense forms

This file describes the tense forms of German, following Durrell's reference grammar. German has six tenses. Two are simple, the present kauft and the past kaufte, and four are compound. The perfect hat gekauft and the pluperfect hatte gekauft put the past participle under the present and the past of haben or sein, and the future wird kaufen and the future perfect wird gekauft haben put an infinitive under the present of werden. German has no progressive forms. A verb forms its perfect with sein when it is an intransitive verb of motion or of change of state, and with haben otherwise; the auxiliaries sein and haben each form their own perfect with themselves.

The past and the perfect overlap in meaning, and the choice between them is largely one of register: narration is in the past in written German and in the perfect in speech. In South Germany, Austria and Switzerland the past is practically never used in everyday speech, and the pluperfect is there commonly formed with the perfect of the auxiliary, the double perfect hat gesehen gehabt, which is colloquial and not accepted as standard.

Main declarations

• German.PrincipalParts: the infinitive, third person singular present and past, and past participle of a verb, with its perfect auxiliary.
• German.haben, German.sein, German.werden: the tense auxiliaries.
• German.perfectAuxiliary: the auxiliary of the perfect of a verb on a frame, by the rule of §12.3.2.
• German.periphrasis, German.PrincipalParts.tenseForm: the means by which German builds its tense forms, and the words of a tense form of a verb, finite verb first.
• German.tenseForms, German.southernTenseForms: the forms of the standard language and of southern speech.
• German.register: the register of a form as a narrative tense.

Implementation notes

PrincipalParts.tenseForm gives the third person singular, the finite verb first and the nonfinite verbs in their clause-final order, the lexical verb before the auxiliaries it stands under. The perfect auxiliary follows from the meaning of the verb on a frame, as Durrell's rule has it, not from the verb alone: an accusative object, a path of motion, the continuation of a state and a change the subject undergoes are what the rule reads. So rennen 'run' takes sein as a verb of motion although it is not unaccusative, tanzen 'dance' takes sein only with a directional phrase (German.perfect_withPath_intransitive), and impersonal frieren, es hat gefroren 'there was a frost', takes haben, its subject an expletive that undergoes nothing. A change of state is read off the entry's aspect, telic or along a scale. The compounds of gehen and werden that take sein with an accusative object (die Strecke abgegangen) are exceptions the rule does not cover.

References

• [Dur11]

structure German.PrincipalPartsextends German.Conjugation.Stem : Type

The principal parts of a verb are its stem, the infinitive, the third person singular present and past and the past participle, with the auxiliary of its perfect.

• infinitive : String
• present : String
• past : String
• participle : String
• prefixGe : Bool
• perfectAuxiliary : Verb.PerfectAuxiliary

  The auxiliary of the perfect.

@[instance_reducible]

instance German.instDecidableEqPrincipalParts : DecidableEq PrincipalParts

Equations

• German.instDecidableEqPrincipalParts = German.instDecidableEqPrincipalParts.decEq

def German.instDecidableEqPrincipalParts.decEq (x✝ x✝¹ : PrincipalParts) : Decidable (x✝ = x✝¹)

Equations

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

def German.instReprPrincipalParts.repr : PrincipalParts → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance German.instReprPrincipalParts : Repr PrincipalParts

Equations

• German.instReprPrincipalParts = { reprPrec := German.instReprPrincipalParts.repr }

def German.haben : PrincipalParts

The auxiliary haben forms the perfect of most verbs, and its own.

Equations

• German.haben = { toStem := German.Conjugation.strong "haben" "hat" "hatte" "gehabt", perfectAuxiliary := Verb.PerfectAuxiliary.have }

def German.sein : PrincipalParts

The auxiliary sein forms the perfect of intransitive verbs of motion and change of state, and its own.

Equations

• German.sein = { toStem := German.Conjugation.strong "sein" "ist" "war" "gewesen", perfectAuxiliary := Verb.PerfectAuxiliary.be }

def German.werden : PrincipalParts

The auxiliary werden forms the future with the infinitive.

Equations

• German.werden = { toStem := German.Conjugation.strong "werden" "wird" "wurde" "geworden", perfectAuxiliary := Verb.PerfectAuxiliary.be }

def German.PrincipalParts.perfectVerb (v : PrincipalParts) : PrincipalParts

The auxiliary verb a perfect is formed with.

Equations

• v.perfectVerb = match v.perfectAuxiliary with | Verb.PerfectAuxiliary.be => German.sein | Verb.PerfectAuxiliary.have => German.haben

def German.perfectAuxiliary (v : Verb) (fr : ArgumentFrame) : Verb.PerfectAuxiliary

The auxiliary of the perfect of v on the frame fr ([Dur11] §12.3.2): haben on a frame with an accusative object (b.i); sein for a verb of motion and for the continuation of a state, bleiben (a.i, a.iv), and for an intransitive verb whose subject undergoes a change of state or to which something happens, to an endpoint or along a scale (a.ii, a.iii); and haben otherwise (b.iii–v).

Equations

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

theorem German.perfect_withPath_intransitive (v : Verb) {p : Adposition.SpatialReading} (hv : v.TakesSpatial) (hp : p.direction ≠ Spatial.Path.Direction.place) : perfectAuxiliary (v.withPath p) ArgumentFrame.intransitive = Verb.PerfectAuxiliary.be

A directional phrase gives an intransitive verb sein: the verbs of motion that name the activity as such, tanzen 'dance' and segeln 'sail', take sein when they express movement from one place to another (§12.3.2c).

theorem German.takesSpatial_of_direction_eq_place (v : Verb) : v ∈ Verbs.allVerbs → v.direction = some Spatial.Path.Direction.place → v.TakesSpatial

The verbs of manner of motion select a directional phrase: every entry that displaces its subject with no direction takes a spatial complement (§12.3.2c).

def German.Verb.principalParts (v : Verb) (fr : ArgumentFrame := v.valency.frames.headD ArgumentFrame.intransitive) : PrincipalParts

The principal parts of a verb entry on a frame, its basic frame by default, are its stem with the auxiliary of its perfect there.

Equations

• v.principalParts fr = { toStem := v.stem, perfectAuxiliary := German.perfectAuxiliary v fr }

def German.periphrasis : Tense.Periphrasis PrincipalParts

German builds its tense forms with the past participle under the verb's perfect auxiliary and the infinitive under werden. It has no future inflection and no form with a present participle.

Equations

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

def German.PrincipalParts.tenseForm (v : PrincipalParts) (f : Tense.Form) : Option (List String)

v.tenseForm f gives the words of the tense form f of v in the third person singular, the finite verb first and then the nonfinite verbs in their clause-final order, the lexical verb before the auxiliaries it stands under.

Equations

• v.tenseForm f = Option.map (fun (x : String × List String) => x.1 :: x.2) (German.periphrasis.realize v f)

theorem German.PrincipalParts.length_of_mem_tenseForm {v : PrincipalParts} {f : Tense.Form} {ws : List String} (h : ws ∈ v.tenseForm f) : ws.length = f.nonfinite.length + 1

A realized tense form has one word for its finite verb and one for each nonfinite form.

def German.tenseForms : List Tense.Form

Standard German has the present, the past, the perfect, the pluperfect, the future and the future perfect.

Equations

• German.tenseForms = [Tense.Form.simplePresent, Tense.Form.simplePast, Tense.Form.presentPerfect, Tense.Form.pastPerfect, Tense.Form.future, Tense.Form.futurePerfect]

def German.southernTenseForms : List Tense.Form

Southern speech lacks the past, and with it the standard pluperfect, and has the double perfect.

Equations

• German.southernTenseForms = [Tense.Form.simplePresent, Tense.Form.presentPerfect, Tense.Form.doublePerfect, Tense.Form.future, Tense.Form.futurePerfect]

theorem German.PrincipalParts.tenseForm_isSome (v : PrincipalParts) {f : Tense.Form} (hf : f ∈ tenseForms ∨ f ∈ southernTenseForms) : (v.tenseForm f).isSome = true

Every tense form of either variety is realized for every verb.

def German.register (f : Tense.Form) : SocialMeaning.Register

As a narrative tense the past belongs to written German and the double perfect to colloquial speech, and the other forms are unmarked.

Equations

• German.register f = if f = Tense.Form.simplePast then SocialMeaning.Register.formal else if f = Tense.Form.doublePerfect then SocialMeaning.Register.informal else SocialMeaning.Register.neutral

theorem German.perfectAuxiliary_mem (v : Verb) : v ∈ Verbs.allVerbs → v.perfectAuxiliaries.Nonempty → perfectAuxiliary v (v.valency.frames.headD ArgumentFrame.intransitive) ∈ v.perfectAuxiliaries

The rule gives every entry on its basic frame an auxiliary its perfect takes: sein for the verbs of motion rennen, laufen and ankommen, for frieren as a change of state and for bleiben, and haben for arbeiten and tanzen, which denote an activity as such, and for the state liegen.