English tense forms

This file describes the tense forms of English, following Huddleston's chapter on the verb in the Cambridge grammar. English marks one tense contrast by inflection, the present takes against the preterite took, and the rest by auxiliaries. The perfect, a secondary past tense, puts the past participle under have, as in has taken, and the progressive aspect puts the gerund-participle under be, as in is taking. The auxiliaries come in a fixed order, the perfect before the progressive, so that has been taking is a form and is having taken is not, and neither auxiliary combines with itself. The eight tense forms are therefore the present and the preterite of the simple, progressive, perfect and perfect progressive constructions. The grammar treats will as a modal auxiliary, a marker of mood, so will take is not among the tense forms.

Main declarations

• English.Tense.TenseVerb: a lexical verb or one of the tense auxiliaries have and be.
• English.Tense.periphrasis, English.Verbs.Verb.tenseForm: the means by which English builds its tense forms, and the words of a tense form of a verb, finite verb first.
• English.Tense.tenseForms: the eight tense forms; Verb.tenseForm_isSome_iff shows that they are exactly the forms that English realizes.

Implementation notes

Verb.tenseForm gives the third person singular. The fixed order of the auxiliaries is not stipulated on forms: it follows from which auxiliary may govern which verb, have governing a lexical verb or be, and be governing a lexical verb only.

References

• [HP02]

inductive English.Tense.TenseVerb : Type

A verb in a tense form is a lexical verb or one of the tense auxiliaries have and be.

• lexical (v : Verbs.Verb) : TenseVerb
• have : TenseVerb
• be : TenseVerb

def English.Tense.periphrasis : Tense.Periphrasis TenseVerb

English builds its tense forms with the past participle under have and the present participle under be. The auxiliary have governs a lexical verb or be, the auxiliary be governs a lexical verb only, and no tense auxiliary governs an infinitive.

Equations

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

def English.Tense.tenseForms : List Tense.Form

English has the present and the preterite of the simple, progressive, perfect and perfect progressive constructions.

Equations

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

theorem English.Tense.chain_eq_some {v : Verbs.Verb} {ns : List Tense.Form.Nonfinite} {ws : List String} {u : TenseVerb} : periphrasis.chain (TenseVerb.lexical v) ns = some (ws, u) → ns = [] ∧ u = TenseVerb.lexical v ∨ ns = [Tense.Form.Nonfinite.pastParticiple] ∧ u = TenseVerb.have ∨ ns = [Tense.Form.Nonfinite.presentParticiple] ∧ u = TenseVerb.be ∨ ns = [Tense.Form.Nonfinite.pastParticiple, Tense.Form.Nonfinite.presentParticiple] ∧ u = TenseVerb.have

The chains English builds over a lexical verb are the empty one, the perfect, the progressive, and the perfect of the progressive, and each leaves the lexical verb, have, be and have to be inflected.

def English.Verbs.Verb.tenseForm (v : Verb) (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, the lexical verb last.

Equations

• v.tenseForm f = Option.map (fun (x : String × List String) => x.1 :: x.2.reverse) (English.Tense.periphrasis.realize (English.Tense.TenseVerb.lexical v) f)

theorem English.Verbs.Verb.tenseForm_isSome_iff (v : Verb) (f : Tense.Form) : (v.tenseForm f).isSome = true ↔ f ∈ Tense.tenseForms

The tense forms are exactly the forms that English realizes.