English Temporal Expressions Fragment

@cite{alstott-aravind-2026} @cite{heinamaki-1974} @cite{rett-2020} @cite{karttunen-1974} @cite{ogihara-steinert-threlkeld-2024} @cite{iatridou-anagnostopoulou-izvorski-2001} @cite{vendler-1957}

Lexical entries for English temporal expressions, organised into two sibling structures (mathlib pattern, mirroring QuantifierEntry + NumericalDetEntry in Determiners.lean):

• TemporalExprEntry — ordering expressions: subordinating connectives (before, after, while, when, until, since, till) and ordering modifiers (within, at, by). The complementType field captures the clausal-vs-nominal distinction; semantic fields (order, licensesNPI, complementVeridical) are shared so generalizations like @cite{rett-2020}'s veridicality typology apply uniformly.

• DurationExprEntry — duration / measure adverbials: for, in (telic and NPI-gap readings), ago. These take a measure phrase and yield a modifier whose semantics involves measuring an interval rather than ordering two time points. The schema is consensus-only: surface form, IAI 2001 typological classification, NPI status and strength, perfect / negation requirements, Vendler-class selection. Paper-specific apparatus (Rouillard 2026's E-TIA / G-TIA labels, M = τ vs M = id parameterization, IAI's PTS apparatus) lives in the relevant Theory or Studies file as partial projections from DurationExprEntry, not as fields on it.

inductive Fragments.English.TemporalExpressions.TemporalOrder : Type

Temporal ordering relation encoded by a connective or modifier.

• before : TemporalOrder
• after : TemporalOrder
• while_ : TemporalOrder
• when_ : TemporalOrder
• until_ : TemporalOrder
• since_ : TemporalOrder
• by_ : TemporalOrder
• whenever : TemporalOrder

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instDecidableEqTemporalOrder : DecidableEq TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instDecidableEqTemporalOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instReprTemporalOrder : Repr TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instReprTemporalOrder = { reprPrec := Fragments.English.TemporalExpressions.instReprTemporalOrder.repr }

def Fragments.English.TemporalExpressions.instReprTemporalOrder.repr : TemporalOrder → ℕ → Std.Format

Equations

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

def Fragments.English.TemporalExpressions.instInhabitedTemporalOrder.default : TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instInhabitedTemporalOrder.default = Fragments.English.TemporalExpressions.TemporalOrder.before

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instInhabitedTemporalOrder : Inhabited TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instInhabitedTemporalOrder = { default := Fragments.English.TemporalExpressions.instInhabitedTemporalOrder.default }

inductive Fragments.English.TemporalExpressions.Reading : Type

Available readings for a temporal clause or modified VP. "Start" = initial point of embedded eventuality; "finish" = final point.

• beforeStart : Reading
• beforeFinish : Reading
• afterStart : Reading
• afterFinish : Reading
• durative : Reading

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instDecidableEqReading : DecidableEq Reading

Equations

• Fragments.English.TemporalExpressions.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.TemporalExpressions.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instReprReading : Repr Reading

Equations

• Fragments.English.TemporalExpressions.instReprReading = { reprPrec := Fragments.English.TemporalExpressions.instReprReading.repr }

def Fragments.English.TemporalExpressions.instInhabitedReading.default : Reading

Equations

• Fragments.English.TemporalExpressions.instInhabitedReading.default = Fragments.English.TemporalExpressions.Reading.beforeStart

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instInhabitedReading : Inhabited Reading

Equations

• Fragments.English.TemporalExpressions.instInhabitedReading = { default := Fragments.English.TemporalExpressions.instInhabitedReading.default }

inductive Fragments.English.TemporalExpressions.ComplementType : Type

Syntactic complement type: clausal (before she arrived) vs nominal (by 3pm, within an hour).

• clausal : ComplementType
• nominal : ComplementType

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instDecidableEqComplementType : DecidableEq ComplementType

Equations

• Fragments.English.TemporalExpressions.instDecidableEqComplementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.TemporalExpressions.instReprComplementType.repr : ComplementType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instReprComplementType : Repr ComplementType

Equations

• Fragments.English.TemporalExpressions.instReprComplementType = { reprPrec := Fragments.English.TemporalExpressions.instReprComplementType.repr }

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instInhabitedComplementType : Inhabited ComplementType

Equations

• Fragments.English.TemporalExpressions.instInhabitedComplementType = { default := Fragments.English.TemporalExpressions.instInhabitedComplementType.default }

def Fragments.English.TemporalExpressions.instInhabitedComplementType.default : ComplementType

Equations

• Fragments.English.TemporalExpressions.instInhabitedComplementType.default = Fragments.English.TemporalExpressions.ComplementType.clausal

structure Fragments.English.TemporalExpressions.TemporalExprEntry : Type

Lexical entry for any temporal expression — subordinating connective or adverbial modifier. Unifies the semantic fields (ordering direction, NPI licensing, veridicality) that @cite{heinamaki-1974} shows are shared across both syntactic categories.

The complementType field records the syntactic distinction (clausal vs nominal complement) without splitting the semantic properties into separate types.

• form : String

  Surface form

• complementType : ComplementType

  Syntactic complement type

• order : TemporalOrder

  Temporal ordering direction

• licensesNPI : Bool

  Does this expression license NPIs in its complement?

• defaultReading : Reading

  Reading obtained without coercion (Rett's strong default)

• coercedReading : Option Reading

  Reading requiring aspectual coercion (INCHOAT or COMPLET)

• embeddedTelicityEffect : Bool

  Does telicity of the embedded clause affect interpretation?

• crossLinguisticBasic : Bool

  Attested in all 17 languages of @cite{rett-2020}'s typological survey

• complementVeridical : Bool

  Does the expression entail the truth of its complement? after is veridical: "He left after she arrived" entails she arrived. before is non-veridical: "He left before she arrived" is compatible with her not arriving.

• forcesPunctual : Bool

  Does this expression force a punctual (point-like) reading?

• triggeredCoercion : Option String

  Which coercion operator is mandatorily triggered (if any). some "INCHOAT" or some "COMPLET" for modifiers that force coercion (e.g. within, at). none for connectives like before/after where coercion is optional — those use coercedReading to record the alternative reading available through voluntary coercion.

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instReprTemporalExprEntry : Repr TemporalExprEntry

Equations

• Fragments.English.TemporalExpressions.instReprTemporalExprEntry = { reprPrec := Fragments.English.TemporalExpressions.instReprTemporalExprEntry.repr }

def Fragments.English.TemporalExpressions.instReprTemporalExprEntry.repr : TemporalExprEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instBEqTemporalExprEntry : BEq TemporalExprEntry

Equations

• Fragments.English.TemporalExpressions.instBEqTemporalExprEntry = { beq := Fragments.English.TemporalExpressions.instBEqTemporalExprEntry.beq }

def Fragments.English.TemporalExpressions.instBEqTemporalExprEntry.beq : TemporalExprEntry → TemporalExprEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.TemporalExpressions.instBEqTemporalExprEntry.beq x✝¹ x✝ = false

def Fragments.English.TemporalExpressions.before_ : TemporalExprEntry

before: licenses NPIs; default = before-start; coerced = before-finish (requires COMPLET to extract telos of telic EE).

Equations

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

def Fragments.English.TemporalExpressions.after_ : TemporalExprEntry

after: no NPIs; default = after-finish; coerced = after-start (requires INCHOAT to extract onset of atelic EE).

Equations

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

def Fragments.English.TemporalExpressions.while_conn : TemporalExprEntry

while: durative overlap, no coercion, no telicity sensitivity.

Equations

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

def Fragments.English.TemporalExpressions.until_ : TemporalExprEntry

until: durative persistence up to complement time. Has two uses:

• Durative: "John slept until 3pm" — main clause is stative, until marks minimum extent. Truth-conditionally = temporal overlap.
• Punctual (with negation): "He didn't wake up until 3pm" — logical form = NOT(A BEFORE T). Licenses NPIs in this use.

We encode the durative reading as default, with the punctual reading arising compositionally via negation + the before semantics.

Equations

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

def Fragments.English.TemporalExpressions.when_conn : TemporalExprEntry

when: temporal coincidence, no coercion. Veridical complement. "John arrived when Mary left" — the two events overlap in time. Symmetric: "A when B" ↔ "B when A".

Equations

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

def Fragments.English.TemporalExpressions.since_conn : TemporalExprEntry

since: starting-point connective. Veridical complement. "He's been happy since she arrived" entails she arrived. Requires durative (stative/activity) main clause, like until. Does not license NPIs.

Equations

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

def Fragments.English.TemporalExpressions.till_conn : TemporalExprEntry

till: dialectal variant of until. Identical semantic properties to until. Dialectally restricted: not universal across English varieties.

Equations

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

def Fragments.English.TemporalExpressions.within_ : TemporalExprEntry

within + duration: relevant to INCHOAT debate. Alstott & Aravind Exps 1a, 3: "within an hour" + activity verb. Alstott & Aravind found no INCHOAT cost here.

Equations

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

def Fragments.English.TemporalExpressions.at_punct : TemporalExprEntry

at + time point: relevant to COMPLET debate. Alstott & Aravind Exp 1b: "at 7 o'clock" + accomplishment. Forces punctual reading → COMPLET required for telic events.

Equations

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

def Fragments.English.TemporalExpressions.by_deadline : TemporalExprEntry

by + time point: deadline semantics. "He arrived by 3pm" = at or before 3pm. Weaker than before (allows coincidence). Does not force punctual reading: "He had finished the book by Tuesday" is fine with an accomplishment.

Equations

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

def Fragments.English.TemporalExpressions.asLongAs : TemporalExprEntry

as long as: temporal containment, synonymous with while. "I'll stay as long as you need me." Same ∀-containment semantics as while. Carries an additional conditional flavor in many uses ("As long as it rains, we stay inside"), but truth-conditionally equivalent to while.

Equations

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

def Fragments.English.TemporalExpressions.whenever_conn : TemporalExprEntry

whenever: universally quantified temporal overlap. "Whenever it rains, I carry an umbrella." Every occasion of B has a corresponding occurrence of A. Truth-conditionally ∀t∈B, t∈A (= while with arguments swapped). Implies habitual/generic interpretation. Veridical for both clauses (given nonempty B).

Equations

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

def Fragments.English.TemporalExpressions.asSoonAs : TemporalExprEntry

as soon as: strengthened after with temporal proximity implicature. "He left as soon as she arrived." Truth-conditionally equivalent to after (∃∃ ordering), but pragmatically implies minimal temporal gap between the two events. Veridical complement.

Equations

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

def Fragments.English.TemporalExpressions.allEntries : List TemporalExprEntry

Equations

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

def Fragments.English.TemporalExpressions.allConnectives : List TemporalExprEntry

Connective entries only (clausal complement).

Equations

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

def Fragments.English.TemporalExpressions.allModifiers : List TemporalExprEntry

Modifier entries only (nominal complement).

Equations

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

theorem Fragments.English.TemporalExpressions.before_form_agrees : before_.form = FunctionWords.before.form

theorem Fragments.English.TemporalExpressions.after_form_agrees : after_.form = FunctionWords.after.form

theorem Fragments.English.TemporalExpressions.all_orders_covered : before_.order = TemporalOrder.before ∧ after_.order = TemporalOrder.after ∧ while_conn.order = TemporalOrder.while_ ∧ until_.order = TemporalOrder.until_ ∧ when_conn.order = TemporalOrder.when_ ∧ since_conn.order = TemporalOrder.since_ ∧ by_deadline.order = TemporalOrder.by_ ∧ whenever_conn.order = TemporalOrder.whenever

All eight temporal orders in the enum have corresponding entries.

theorem Fragments.English.TemporalExpressions.only_before_nonveridical : before_.complementVeridical = false ∧ after_.complementVeridical = true ∧ while_conn.complementVeridical = true ∧ until_.complementVeridical = true ∧ when_conn.complementVeridical = true ∧ since_conn.complementVeridical = true ∧ till_conn.complementVeridical = true ∧ asLongAs.complementVeridical = true ∧ whenever_conn.complementVeridical = true ∧ asSoonAs.complementVeridical = true ∧ by_deadline.complementVeridical = true ∧ within_.complementVeridical = true ∧ at_punct.complementVeridical = true

Veridicality pattern: before is the only non-veridical expression. This holds across both connectives and modifiers.

theorem Fragments.English.TemporalExpressions.npi_pattern : before_.licensesNPI = true ∧ until_.licensesNPI = true ∧ till_conn.licensesNPI = true ∧ after_.licensesNPI = false ∧ while_conn.licensesNPI = false ∧ when_conn.licensesNPI = false ∧ since_conn.licensesNPI = false ∧ asLongAs.licensesNPI = false ∧ whenever_conn.licensesNPI = false ∧ asSoonAs.licensesNPI = false ∧ by_deadline.licensesNPI = false ∧ within_.licensesNPI = false ∧ at_punct.licensesNPI = false

NPI licensing pattern: only before, until, and till license NPIs. For before, this follows from downward entailment of the complement. For until/till, this arises in the punctual (not...until) construction, which is truth-conditionally ¬before. No modifiers license NPIs.

theorem Fragments.English.TemporalExpressions.till_matches_until : till_conn.order = until_.order ∧ till_conn.licensesNPI = until_.licensesNPI ∧ till_conn.defaultReading = until_.defaultReading ∧ till_conn.complementVeridical = until_.complementVeridical

Till and until agree on all semantic properties.

theorem Fragments.English.TemporalExpressions.complement_type_classification : before_.complementType = ComplementType.clausal ∧ after_.complementType = ComplementType.clausal ∧ while_conn.complementType = ComplementType.clausal ∧ until_.complementType = ComplementType.clausal ∧ when_conn.complementType = ComplementType.clausal ∧ since_conn.complementType = ComplementType.clausal ∧ till_conn.complementType = ComplementType.clausal ∧ by_deadline.complementType = ComplementType.nominal ∧ within_.complementType = ComplementType.nominal ∧ at_punct.complementType = ComplementType.nominal

The complement-type field correctly classifies all entries.

theorem Fragments.English.TemporalExpressions.asLongAs_matches_while : asLongAs.order = while_conn.order ∧ asLongAs.licensesNPI = while_conn.licensesNPI ∧ asLongAs.defaultReading = while_conn.defaultReading ∧ asLongAs.complementVeridical = while_conn.complementVeridical

As long as agrees with while on all semantic properties.

theorem Fragments.English.TemporalExpressions.asSoonAs_matches_after : asSoonAs.order = after_.order ∧ asSoonAs.licensesNPI = after_.licensesNPI ∧ asSoonAs.defaultReading = after_.defaultReading ∧ asSoonAs.complementVeridical = after_.complementVeridical

As soon as agrees with after on ordering and veridicality.

inductive Fragments.English.TemporalExpressions.DurationKind : Type

Sub-class discriminator for duration adverbials.

The four English duration adverbials carve out distinct semantic profiles even though they share the same schema:

• telicCompletion (in three hours): measures the runtime of a telic event from onset to telos.
• atelicDurative (for three hours): measures the runtime of an atelic event.
• pastOffset (three days ago): postposed deictic offset from the utterance time into the past.
• npiGap (in years under negation+perfect): measures the gap between the right boundary of the perfect time span and the most recent witnessing event. Strong NPI.

• telicCompletion : DurationKind
• atelicDurative : DurationKind
• pastOffset : DurationKind
• npiGap : DurationKind

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instDecidableEqDurationKind : DecidableEq DurationKind

Equations

• Fragments.English.TemporalExpressions.instDecidableEqDurationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instReprDurationKind : Repr DurationKind

Equations

• Fragments.English.TemporalExpressions.instReprDurationKind = { reprPrec := Fragments.English.TemporalExpressions.instReprDurationKind.repr }

def Fragments.English.TemporalExpressions.instReprDurationKind.repr : DurationKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instInhabitedDurationKind : Inhabited DurationKind

Equations

• Fragments.English.TemporalExpressions.instInhabitedDurationKind = { default := Fragments.English.TemporalExpressions.instInhabitedDurationKind.default }

def Fragments.English.TemporalExpressions.instInhabitedDurationKind.default : DurationKind

Equations

• Fragments.English.TemporalExpressions.instInhabitedDurationKind.default = Fragments.English.TemporalExpressions.DurationKind.telicCompletion

structure Fragments.English.TemporalExpressions.DurationExprEntry : Type

Lexical entry for a duration / measure adverbial.

Schema is consensus typological metadata only. Theory-specific machinery (PTS classification, Rouillard's E-TIA / G-TIA labels, Iatridou-Zeijlstra 2021's domain-widening profile) lives as partial projections from this structure in the relevant Theory or Studies file (mathlib-style pattern: same discipline as QuantifierEntry → gqDenotation/ptMeaning/gqtMeaning in Determiners.lean).

Cross-references for in years (the NPI-gap entry):

• Theories/Semantics/Tense/PTS.lean :: inYears — Iatridou-Zeijlstra 2021 boundary-adverbial projection (PTS-tradition apparatus).
• Fragments/English/PolarityItems.lean :: inYears — polarity-theoretic projection (Israel 1996 / 2001 scalar model). Consolidating the three views into a single canonical entry plus derived projections is a follow-up refactor.

• form : String

  Surface form (e.g., "in", "for", "ago")

• kind : DurationKind

  Sub-class of duration adverbial

• isPostposition : Prop

  True for postpositions (ago); most duration adverbials are prepositions.

• vendlerSelection : Option Features.Telicity

  Aspectual class the adverbial selects for at the VP it modifies (Vendler-level consensus; @cite{vendler-1957}). none = no restriction; some .telic = requires accomplishment/achievement; some .atelic = requires state/activity.

• iaiClassification : Option Semantics.Tense.TemporalAdverbials.AdverbialType

  Iatridou-Anagnostopoulou-Izvorski 2001 typological classification. durative = pins the left boundary of the perfect time span; inclusive = leaves the LB free. none for entries that don't participate in the perfect-time-span typology.

• polaritySensitive : Prop

  Is this entry itself a polarity-sensitive item?

• polarityType : Option Typology.PolarityItem.PolarityType

  Polarity-item type if polaritySensitive (Zwarts 1998 strong/weak). Strong NPIs (in years) require anti-additive licensors; weak NPIs require any DE licensor.

• requiresPerfect : Prop

  Distributional licensing flags (theory-neutral surface facts).

• requiresNegation : Prop

@[implicit_reducible]

instance Fragments.English.TemporalExpressions.instReprDurationExprEntry : Repr DurationExprEntry

Equations

• Fragments.English.TemporalExpressions.instReprDurationExprEntry = { reprPrec := Fragments.English.TemporalExpressions.instReprDurationExprEntry.repr }

def Fragments.English.TemporalExpressions.instReprDurationExprEntry.repr : DurationExprEntry → ℕ → Std.Format

Equations

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

def Fragments.English.TemporalExpressions.inTelic : DurationExprEntry

in three days (telic-completion): "Mary wrote a paper in three days". Selects telic VPs (accomplishment / achievement). Not an NPI. IAI 2001 classification: inclusive (leaves PTS LB free).

Equations

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

def Fragments.English.TemporalExpressions.inGap : DurationExprEntry

in years / in days / in months (NPI-gap reading): "Mary hasn't been sick in years". Strong NPI. Requires the perfect and negative polarity. IAI 2001 classification: durative (pins PTS LB).

Same surface preposition as inTelic; the two readings are distinguished by syntactic position and licensing environment.

Equations

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

def Fragments.English.TemporalExpressions.forDur : DurationExprEntry

for three hours (atelic-durative): "Mary was sick for three hours". Selects atelic VPs (state / activity). IAI 2001 classification: durative when combined with the perfect (pins PTS LB by specifying duration).

Equations

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

def Fragments.English.TemporalExpressions.ago : DurationExprEntry

three days ago: postposed deictic past offset. The lone English postposition. Combines with a measure phrase to locate an event a specified duration prior to the utterance time. Not an NPI; does not require the perfect.

Equations

• Fragments.English.TemporalExpressions.ago = { form := "ago", kind := Fragments.English.TemporalExpressions.DurationKind.pastOffset, isPostposition := True }

def Fragments.English.TemporalExpressions.allDurationEntries : List DurationExprEntry

All duration adverbial entries.

Equations

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

theorem Fragments.English.TemporalExpressions.in_readings_share_form : inTelic.form = inGap.form

Both in-readings share the surface preposition.

theorem Fragments.English.TemporalExpressions.in_readings_distinct_kind : inTelic.kind ≠ inGap.kind

The two in-readings are distinguished by kind.

theorem Fragments.English.TemporalExpressions.inTelic_form_agrees : inTelic.form = FunctionWords.in_.form

Surface form of telic in agrees with the canonical preposition entry.

theorem Fragments.English.TemporalExpressions.inGap_form_agrees : inGap.form = FunctionWords.in_.form

Surface form of NPI-gap in agrees with the canonical preposition entry.

theorem Fragments.English.TemporalExpressions.ago_unique_postposition : ago.isPostposition ∧ ¬inTelic.isPostposition ∧ ¬inGap.isPostposition ∧ ¬forDur.isPostposition

Ago is the only postposition among duration adverbials.

theorem Fragments.English.TemporalExpressions.only_inGap_polarity_sensitive : inGap.polaritySensitive ∧ ¬inTelic.polaritySensitive ∧ ¬forDur.polaritySensitive ∧ ¬ago.polaritySensitive

Only the NPI-gap reading is polarity-sensitive.

theorem Fragments.English.TemporalExpressions.vendler_selection_pattern : inTelic.vendlerSelection = some Features.Telicity.telic ∧ forDur.vendlerSelection = some Features.Telicity.atelic ∧ inGap.vendlerSelection = none ∧ ago.vendlerSelection = none

Telicity-selection pattern: telic in selects telic VPs; atelic for selects atelic VPs; the gap reading and ago have no Vendler restriction.

theorem Fragments.English.TemporalExpressions.iai_classification_pattern : inTelic.iaiClassification = some Semantics.Tense.TemporalAdverbials.AdverbialType.inclusive ∧ inGap.iaiClassification = some Semantics.Tense.TemporalAdverbials.AdverbialType.durative ∧ forDur.iaiClassification = some Semantics.Tense.TemporalAdverbials.AdverbialType.durative ∧ ago.iaiClassification = none

IAI 2001 durative-vs-inclusive classification: for and the NPI-gap in pin the PTS left boundary (durative); telic in leaves it free (inclusive); ago is outside the PTS typology entirely.