Aspectual boundedness

@cite{smith-1997}

SituationBoundedness classifies a situation as bounded (telic/perfective/closed) or unbounded (atelic/imperfective/open). It cross-cuts Vendler classes and aspectual viewpoint, and is consumed by event semantics, aspect theory, and temporal discourse interpretation.

The bridge to Core.Scale.MereoTag (bounded ↔ quantized; unbounded ↔ cumulative) lets the licensing pipeline classify boundedness uniformly with other scale-style properties.

inductive Core.Time.SituationBoundedness : Type

Aspectual boundedness of a situation.

Whether a situation is conceptualized as having inherent boundaries:

• bounded: telic / perfective / closed (achievements, accomplishments)
• unbounded: atelic / imperfective / open (activities, states)

Cross-cuts Vendler classes and aspectual viewpoint. Used by event semantics (telicity), aspect theory (perfective/imperfective), and temporal discourse interpretation (sequential vs. simultaneous default readings).

• bounded : SituationBoundedness
• unbounded : SituationBoundedness

@[implicit_reducible]

instance Core.Time.instDecidableEqSituationBoundedness : DecidableEq SituationBoundedness

Equations

• Core.Time.instDecidableEqSituationBoundedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Time.instReprSituationBoundedness : Repr SituationBoundedness

Equations

• Core.Time.instReprSituationBoundedness = { reprPrec := Core.Time.instReprSituationBoundedness.repr }

def Core.Time.instReprSituationBoundedness.repr : SituationBoundedness → ℕ → Std.Format

Equations

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

def Core.Time.SituationBoundedness.toMereoTag : SituationBoundedness → Scale.MereoTag

SituationBoundedness → MereoTag: bounded = quantized, unbounded = cumulative. Bounded situations (telic/perfective) are mereologically quantized; unbounded situations (atelic/imperfective) are cumulative.

Equations

• Core.Time.SituationBoundedness.bounded.toMereoTag = Core.Scale.MereoTag.qua
• Core.Time.SituationBoundedness.unbounded.toMereoTag = Core.Scale.MereoTag.cum

@[implicit_reducible]

instance Core.Time.instLicensingPipelineSituationBoundedness : Scale.LicensingPipeline SituationBoundedness

Equations

• Core.Time.instLicensingPipelineSituationBoundedness = { toBoundedness := fun (s : Core.Time.SituationBoundedness) => s.toMereoTag.toBoundedness }

theorem Core.Time.bounded_licensed : Scale.LicensingPipeline.isLicensed SituationBoundedness.bounded = true

theorem Core.Time.unbounded_blocked : Scale.LicensingPipeline.isLicensed SituationBoundedness.unbounded = false