Documentation

Linglib.Studies.AlstottAravind2026TemporalConnectives

Aspect × Temporal Connective Interaction Bridge #

[AA26] [MS88] [Kar74] [Ret20]

Connects three layers:

Fragment: TemporalExprEntry fields (embeddedTelicityEffect, defaultReading, coercedReading, triggeredCoercion)
Theory: VendlerClass features, INCHOAT/COMPLET, and MoensSteedmanClass.whenTarget
Data: per-paper rows in Data.Examples.{MoensSteedman1988, Karttunen1974, AlstottAravind2026}

Main declarations #

vendlerOf: adapter reading a row's paperFeatures
coercion_tracks_embedded_telicity: a before/after row records a coercion operator exactly when the connective × embedded-telicity pair demands one (COMPLET for before + telic, INCHOAT for after + atelic)
satisfiesDurativeRestriction, until_acceptable_iff_durative: Karttunen's durative selectional restriction, derived from Vendler features, predicts each until row's acceptability
when_coercion_matches_ms: each when row's coercion annotation is the one MoensSteedmanClass.whenTarget predicts for its Vendler class
inchoat_extracts_onset, complet_extracts_telos: the Fragment's coercion labels grounded in the operators' interval-set behavior

theorem AlstottAravind2026TemporalConnectives.telicity_sensitivity_pattern :

English.TemporalExpressions.before_.embeddedTelicityEffect = true ∧ English.TemporalExpressions.after_.embeddedTelicityEffect = true ∧ English.TemporalExpressions.while_conn.embeddedTelicityEffect = false ∧ English.TemporalExpressions.until_.embeddedTelicityEffect = false ∧ English.TemporalExpressions.when_conn.embeddedTelicityEffect = false ∧ English.TemporalExpressions.since_conn.embeddedTelicityEffect = false ∧ English.TemporalExpressions.till_conn.embeddedTelicityEffect = false

embeddedTelicityEffect = true holds exactly for connectives that reference boundary points (onset/telos) of the embedded clause. These are before and after: their truth conditions change depending on whether the embedded clause is telic or atelic, because:

Telic → natural endpoint exists → COMPLET/INCHOAT not needed
Atelic → no natural endpoint → coercion needed for endpoint reading

theorem AlstottAravind2026TemporalConnectives.telicity_sensitivity_iff_ordering :

(English.TemporalExpressions.before_.order == English.TemporalExpressions.TemporalOrder.before) = English.TemporalExpressions.before_.embeddedTelicityEffect ∧ (English.TemporalExpressions.after_.order == English.TemporalExpressions.TemporalOrder.after) = English.TemporalExpressions.after_.embeddedTelicityEffect ∧ (English.TemporalExpressions.while_conn.order == English.TemporalExpressions.TemporalOrder.before || English.TemporalExpressions.while_conn.order == English.TemporalExpressions.TemporalOrder.after) = English.TemporalExpressions.while_conn.embeddedTelicityEffect ∧ (English.TemporalExpressions.until_.order == English.TemporalExpressions.TemporalOrder.before || English.TemporalExpressions.until_.order == English.TemporalExpressions.TemporalOrder.after) = English.TemporalExpressions.until_.embeddedTelicityEffect ∧ (English.TemporalExpressions.when_conn.order == English.TemporalExpressions.TemporalOrder.before || English.TemporalExpressions.when_conn.order == English.TemporalExpressions.TemporalOrder.after) = English.TemporalExpressions.when_conn.embeddedTelicityEffect

The telicity sensitivity split corresponds to the ordering direction: connectives with order ∈ {before, after} are telicity-sensitive; overlap/persistence connectives are not.

def AlstottAravind2026TemporalConnectives.vendlerOf (row : Data.Examples.LinguisticExample) :

Option Features.VendlerClass

Vendler-class adapter: the row's vendler_class feature.

Equations

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

Instances For

def AlstottAravind2026TemporalConnectives.expectedCoercion (conn : String) (c : Features.VendlerClass) :

Option String

The coercion operator a before/after clause needs for its non-default reading: COMPLET (telos extraction) for before + telic embedded clauses, INCHOAT (onset extraction) for after + atelic embedded clauses; the remaining combinations have only the default reading.

Equations

AlstottAravind2026TemporalConnectives.expectedCoercion "before" c = some "COMPLET"
AlstottAravind2026TemporalConnectives.expectedCoercion "after" c = some "INCHOAT"
AlstottAravind2026TemporalConnectives.expectedCoercion conn✝ c = none

Instances For

theorem AlstottAravind2026TemporalConnectives.coercion_tracks_embedded_telicity (row : Data.Examples.LinguisticExample) :

row ∈ AlstottAravind2026.Examples.all → row.feature? "coercion" = (row.feature? "connective").bind fun (conn : String) => (vendlerOf row).bind fun (c : Features.VendlerClass) => expectedCoercion conn c

Transfer equation over the before/after rows: a row records a coercion operator exactly when its connective × embedded-telicity pair demands one. The two coerced cells are the conditions tested in [AA26]'s Exps 2 (COMPLET) and 4 (INCHOAT).

theorem AlstottAravind2026TemporalConnectives.default_reading_matches_fragment :

English.TemporalExpressions.before_.defaultReading = English.TemporalExpressions.Reading.beforeStart ∧ English.TemporalExpressions.after_.defaultReading = English.TemporalExpressions.Reading.afterFinish ∧ ∀ row ∈ AlstottAravind2026.Examples.all, row.feature? "default_reading" = (row.feature? "connective").bind fun (conn : String) => if conn = "before" then some "before-start" else if conn = "after" then some "after-finish" else none

The rows' recorded default readings are the Fragment's defaults: before-start for before, after-finish for after ([Ret20]'s strong defaults).

theorem AlstottAravind2026TemporalConnectives.coerced_reading_matches_fragment :

English.TemporalExpressions.before_.coercedReading = some English.TemporalExpressions.Reading.beforeFinish ∧ English.TemporalExpressions.after_.coercedReading = some English.TemporalExpressions.Reading.afterStart ∧ ∀ row ∈ AlstottAravind2026.Examples.all, row.feature? "coerced_reading" = (row.feature? "coercion").bind fun (op : String) => if op = "COMPLET" then some "before-finish" else if op = "INCHOAT" then some "after-start" else none

A row records a coerced reading exactly when it records a coercion operator, and the reading is the Fragment's coercedReading: before-finish under COMPLET, after-start under INCHOAT.

def AlstottAravind2026TemporalConnectives.satisfiesDurativeRestriction (c : Features.VendlerClass) :

Bool

[Kar74]'s durative selectional restriction on until/since main clauses, derived from the Vendler feature decomposition: atelic and durative — exactly the subinterval-property (homogeneous) classes.

Equations

AlstottAravind2026TemporalConnectives.satisfiesDurativeRestriction c = (c.telicity == Features.Telicity.atelic && c.duration == Features.Duration.durative)

Instances For

theorem AlstottAravind2026TemporalConnectives.durative_restriction_iff_state_or_activity (c : Features.VendlerClass) :

satisfiesDurativeRestriction c = true ↔ c = Features.VendlerClass.state ∨ c = Features.VendlerClass.activity

The durative restriction picks out exactly states and activities.

theorem AlstottAravind2026TemporalConnectives.until_acceptable_iff_durative (row : Data.Examples.LinguisticExample) :

row ∈ Karttunen1974.Examples.all → (row.judgment = Features.Judgment.acceptable ↔ Option.map satisfiesDurativeRestriction (vendlerOf row) = some true)

Transfer equation over the until main-clause rows: a row is acceptable iff its main clause's Vendler class satisfies the durative restriction.

theorem AlstottAravind2026TemporalConnectives.inchoat_extracts_onset (i : NonemptyInterval ℕ) :

Tense.TemporalConnectives.INCHOAT (Tense.TemporalConnectives.stativeDenotation i) = {j : NonemptyInterval ℕ | j = NonemptyInterval.pure i.toProd.1}

INCHOAT extracts the onset of an atelic/stative denotation. The theory proves this equals the start point — connecting the Fragment's triggeredCoercion = "INCHOAT" to concrete behavior.

theorem AlstottAravind2026TemporalConnectives.complet_extracts_telos (i : NonemptyInterval ℕ) :

Tense.TemporalConnectives.COMPLET (Tense.TemporalConnectives.accomplishmentDenotation i) = {j : NonemptyInterval ℕ | j = NonemptyInterval.pure i.toProd.2}

COMPLET extracts the telos of a telic denotation. The theory proves this equals the finish point — connecting the Fragment's triggeredCoercion = "COMPLET" to concrete behavior.

theorem AlstottAravind2026TemporalConnectives.triggered_coercion_entries :

English.TemporalExpressions.within_.triggeredCoercion = some "INCHOAT" ∧ English.TemporalExpressions.at_punct.triggeredCoercion = some "COMPLET" ∧ English.TemporalExpressions.before_.triggeredCoercion = none ∧ English.TemporalExpressions.after_.triggeredCoercion = none

The Fragment entries that specify triggeredCoercion are exactly those that need aspectual adjustment for their complement type:

within_ triggers INCHOAT (needs onset of duration)
at_punct triggers COMPLET (needs telos of telic event)
before/after have triggeredCoercion = none because they have both default and coerced readings (specified via coercedReading).

def AlstottAravind2026TemporalConnectives.msOf :

Features.VendlerClass → Semantics.Aspect.SubeventStructure.MoensSteedmanClass

Embed Vendler classes into [MS88] event types (achievements as culminations, semelfactives as points; the two M&S atomic types collapse to achievement at Vendler granularity).

Equations

Instances For

def AlstottAravind2026TemporalConnectives.whenCoercionLabel :

Semantics.Aspect.SubeventStructure.WhenTarget → Option String

The coercion a when-clause triggers for each WhenTarget: inception coercion for processes, completion coercion for culminated processes, and none where the event directly supplies a reference point.

Equations

Instances For

theorem AlstottAravind2026TemporalConnectives.when_coercion_matches_ms (row : Data.Examples.LinguisticExample) :

row ∈ MoensSteedman1988.Examples.all → row.feature? "coercion" = (vendlerOf row).bind fun (c : Features.VendlerClass) => whenCoercionLabel (msOf c).whenTarget

Transfer equation over the when rows: each row's coercion annotation is exactly the one MoensSteedmanClass.whenTarget predicts for its Vendler class. States need no coercion (homogeneous overlap), achievements ARE culmination points, activities coerce to their onset, accomplishments to their telos.

theorem AlstottAravind2026TemporalConnectives.when_coercion_targets_achievement (row : Data.Examples.LinguisticExample) :

row ∈ MoensSteedman1988.Examples.all → (row.feature? "coercion").isSome = true → row.feature? "result_class" = some "achievement"

When when coerces, the result is punctual: every coerced when row records achievement as its result class.

theorem AlstottAravind2026TemporalConnectives.add_result_is_telicize :

Features.activityProfile.telicize.toVendlerClass = Features.VendlerClass.accomplishment

[MS88] Fig. 2's "add-result" transition (process → culminated process) is the theory's telicize: adding a natural endpoint to an activity yields an accomplishment.

theorem AlstottAravind2026TemporalConnectives.iterate_is_duratize_atelicize :

Features.achievementProfile.duratize.atelicize.toVendlerClass = Features.VendlerClass.activity

Fig. 2's iteration transition (point → process) at Vendler granularity is duratize followed by atelicize: stretching a punctual event over time and removing the endpoint yields an activity.