@[reducible, inline]

abbrev Semantics.Tense.TemporalAdverbials.PTSConstraint (Time : Type u_3) [LinearOrder Time] : Type u_3

A constraint on the Perfect Time Span. Adverbials restrict which PTS intervals are admissible.

Equations

• Semantics.Tense.TemporalAdverbials.PTSConstraint Time = (Core.Time.Interval Time → Prop)

inductive Semantics.Tense.TemporalAdverbials.AdverbialType : Type

@cite{iatridou-anagnostopoulou-izvorski-2001} adverbial type classification.

• durative: specifies the left boundary (e.g., "since Monday")
• inclusive: does not specify the left boundary (e.g., "before Monday")

• durative : AdverbialType
• inclusive : AdverbialType

@[implicit_reducible]

instance Semantics.Tense.TemporalAdverbials.instDecidableEqAdverbialType : DecidableEq AdverbialType

Equations

• Semantics.Tense.TemporalAdverbials.instDecidableEqAdverbialType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Tense.TemporalAdverbials.instReprAdverbialType : Repr AdverbialType

Equations

• Semantics.Tense.TemporalAdverbials.instReprAdverbialType = { reprPrec := Semantics.Tense.TemporalAdverbials.instReprAdverbialType.repr }

def Semantics.Tense.TemporalAdverbials.instReprAdverbialType.repr : AdverbialType → ℕ → Std.Format

Equations

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

def Semantics.Tense.TemporalAdverbials.everSince {Time : Type u_2} [LinearOrder Time] (t₀ : Time) : PTSConstraint Time

"ever since t₀": PTS must start at t₀. E.g., "has been running since Monday" → PTS.start = Monday.

Equations

• Semantics.Tense.TemporalAdverbials.everSince t₀ pts = (pts.start = t₀)

def Semantics.Tense.TemporalAdverbials.forDurationFrom {Time : Type u_2} [LinearOrder Time] (tStart : Time) : PTSConstraint Time

"for (duration) from tStart": PTS must start at tStart. Simplified duration adverbial — the duration is implicit in the interval length [tStart, RB].

Equations

• Semantics.Tense.TemporalAdverbials.forDurationFrom tStart pts = (pts.start = tStart)

def Semantics.Tense.TemporalAdverbials.always {Time : Type u_2} [LinearOrder Time] : PTSConstraint Time

"always" / no temporal adverbial: no constraint on PTS.

Equations

• Semantics.Tense.TemporalAdverbials.always x✝ = True

def Semantics.Tense.TemporalAdverbials.before {Time : Type u_2} [LinearOrder Time] : PTSConstraint Time

"before t" (inclusive adverbial): no constraint on PTS start. The adverbial constrains the event location, not the PTS boundary.

Equations

• Semantics.Tense.TemporalAdverbials.before x✝ = True

def Semantics.Tense.TemporalAdverbials.PTSConstraint.toLBDomain {Time : Type u_2} [LinearOrder Time] (adv : PTSConstraint Time) (tc : Time) : Set Time

Convert a PTS constraint to a domain of compatible LB values, given that the right boundary is fixed at tc.

For a constraint C, the compatible LBs are those tLB ≤ tc such that C holds of the interval [tLB, tc].

Equations

• adv.toLBDomain tc = {tLB : Time | tLB ≤ tc ∧ ∀ (h : tLB ≤ tc), adv { start := tLB, finish := tc, valid := h }}

def Semantics.Tense.TemporalAdverbials.PERF_ADV {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Aspect.Core.IntervalPred W Time) (adv : PTSConstraint Time) : Aspect.Core.PointPred W Time

Perfect with adverbial constraint: PERF_ADV(p, adv). Combines PERF with an adverbial constraint on the PTS. Equivalent to PERF_XN with the adverbial's derived LB domain.

Equations

• Semantics.Tense.TemporalAdverbials.PERF_ADV p adv s = ∃ (pts : Core.Time.Interval Time), Semantics.Aspect.Core.RB pts s.time ∧ adv pts ∧ p s.world pts

def Semantics.Tense.TemporalAdverbials.AdverbialType.specifiesLB : AdverbialType → Bool

Does this adverbial type specify the left boundary? Durative adverbials pin the LB; inclusive adverbials leave it free.

Equations

• Semantics.Tense.TemporalAdverbials.AdverbialType.durative.specifiesLB = true
• Semantics.Tense.TemporalAdverbials.AdverbialType.inclusive.specifiesLB = false

theorem Semantics.Tense.TemporalAdverbials.perf_adv_eq_perf_xn {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Aspect.Core.IntervalPred W Time) (adv : PTSConstraint Time) (tc : Time) (w : W) : PERF_ADV p adv { world := w, time := tc } ↔ Aspect.Core.PERF_XN p (adv.toLBDomain tc) { world := w, time := tc }

PERF_ADV is equivalent to PERF_XN with the adverbial's derived LB domain.

Proof sketch: Both existentially quantify over a PTS with RB = tc. PERF_ADV requires adv(PTS); PERF_XN requires LB(tLB, PTS) with tLB ∈ toLBDomain(adv, tc). These are equivalent by definition of toLBDomain: tLB ∈ toLBDomain ↔ tLB ≤ tc ∧ adv([tLB, tc]).

theorem Semantics.Tense.TemporalAdverbials.everSince_specifies_lb {Time : Type u_2} [LinearOrder Time] (t₀ tc : Time) (h : t₀ ≤ tc) : (everSince t₀).toLBDomain tc = {t₀}

"ever since t₀" specifies the LB domain to exactly {t₀} (assuming t₀ ≤ tc).

Proof sketch: toLBDomain(everSince t₀, tc) = {tLB | tLB ≤ tc ∧ tLB = t₀} = {t₀} when t₀ ≤ tc.

theorem Semantics.Tense.TemporalAdverbials.before_no_lb_constraint {Time : Type u_2} [LinearOrder Time] (tc : Time) : before.toLBDomain tc = {tLB : Time | tLB ≤ tc}

"before" imposes no LB constraint: all tLB ≤ tc are compatible.

Proof sketch: toLBDomain(before, tc) = {tLB | tLB ≤ tc ∧ True} = {tLB | tLB ≤ tc}.

theorem Semantics.Tense.TemporalAdverbials.durative_licenses_u_perfect {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : Events.EventPred W Time) (t₀ tc : Time) (w : W) (_h : t₀ ≤ tc) : TenseAspectComposition.presPerfProgXN V {t₀} tc w → TenseAspectComposition.simplePresent V tc w

Durative adverbials (specified LB) license U-perf → simple present.

When the LB is pinned (durative adverbial), the U-perf reading entails the simple present via u_perf_entails_simple_present.

theorem Semantics.Tense.TemporalAdverbials.inclusive_no_u_license {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : Events.EventPred W Time) (tc : Time) (w : W) : TenseAspectComposition.presPerfProgXN V Set.univ tc w ↔ TenseAspectComposition.simplePresent V tc w

Inclusive adverbials (unspecified LB) yield U-perf ↔ simple present when the LB domain is maximal.

With no LB constraint, the domain is {tLB | tLB ≤ tc}. Under IMPF (subinterval property), this is close to Set.univ for the relevant range, so U-perf ↔ simple present by broad_focus_equiv's argument.