Temporal connectives

This file defines the lexical entry of a temporal connective, a subordinator or preposition that locates the time of its host clause relative to the time of its complement: before, after, when, while, until, since, by and whenever. An entry records the relation the word lexicalizes, drawn from Heinämäki's inventory, and the grammatical mood its complement takes where the language marks one. Whether an until word is a punctual rather than a durative until, Karttunen's two untils, is contested, since Iatridou and Zeijlstra derive both uses from one until, so a study that draws the line classifies the words itself.

An entry carries no truth conditions. What before means is contested, from the quantificational relations of Anscombe and Heinämäki to the branching-time analysis of Beaver and Condoravdi and the scalar one of Rett, so a study assigns denotations to the relations it treats and derives veridicality and polarity licensing from them; a fragment says only which relation a word lexicalizes.

Main declarations

• Tense.Connective: the lexical entry, with its relation and mood.
• Tense.Connective.Relation: the eight relations a connective can lexicalize.

References

• [Hei74]
• [Kar74b]
• [IZ21]
• [Ans64]
• [BC03]
• [Ret20a]

inductive Tense.Connective.Relation : Type

The temporal relations a connective can lexicalize, [Hei74]'s inventory, are that the host precedes or follows the complement, the two coincide or the host lies within the complement, the host persists to or from the complement time, the host is done by it, or the host recurs with the complement.

• before : Relation
• after : Relation
• when_ : Relation
• while_ : Relation
• until_ : Relation
• since : Relation
• by_ : Relation
• whenever : Relation

@[instance_reducible]

instance Tense.Connective.instDecidableEqRelation : DecidableEq Relation

Equations

• Tense.Connective.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tense.Connective.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tense.Connective.instReprRelation : Repr Relation

Equations

• Tense.Connective.instReprRelation = { reprPrec := Tense.Connective.instReprRelation.repr }

structure Tense.Connective : Type

A temporal connective is a subordinator or preposition relating the time of its host clause to that of its complement.

• form : String

  The surface form.

• relation : Relation

  The relation the connective lexicalizes.

• mood : Option Mood.Grammatical

  The grammatical mood of the complement, where the language marks one.