Features.Aktionsart

@cite{vendler-1957} @cite{smith-1997}

Per-verb-entry feature taxonomy for lexical aspect: three orthogonal binary features (telicity, duration, dynamicity), the five-way Vendler class projection, the bundled AspectualProfile, and aspectual-shift operations modeling compositional coercion.

Descriptive vocabulary Fragment authors use to label lexical entries (verb.aspectualProfile = activityProfile); predictions about how a labelled verb's denotation behaves live in Theories/ (consequence theorems) or framework-specific Studies/ files.

The 5-way classification follows the Vendler taxonomy as extended by Smith 1991 / @cite{smith-1997} (binary feature decomposition + 5-cell map including semelfactives — both first appear in the 1991 1st ed., not the 1997 2nd ed. cited here). The semelfactive category itself comes from Slavic aspectology (Comrie 1976 Aspect, not in references.bib).

Telicity.toMereoTag projects this file's binary Telicity onto Core.Scales.Scale.MereoTag, the canonical cumulative/quantized tag. The CUM/QUA/DIV algebra over event predicates lives in Theories/Semantics/Events/CEM.lean — that is the substrate; the Telicity here is the Smith-flavored derived label.

Sibling formalizations of competitor lexical-aspect frameworks: @cite{bach-1986} EventSort in Theories/Semantics/Events/Basic.lean; @cite{krifka-1989}/@cite{krifka-1998} CUM/QUA/DIV in Theories/Semantics/Events/CEM.lean; @cite{dowty-1979} SIP in Theories/Semantics/Tense/Aspect/SubintervalProperty.lean; @cite{filip-2012} three-way refutation of binary telicity in Phenomena/TenseAspect/Studies/Filip2012.lean.

inductive Features.Telicity : Type

Telicity: whether an event has a natural endpoint.

• telic : Telicity
• atelic : Telicity

@[implicit_reducible]

instance Features.instDecidableEqTelicity : DecidableEq Telicity

Equations

• Features.instDecidableEqTelicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprTelicity : Repr Telicity

Equations

• Features.instReprTelicity = { reprPrec := Features.instReprTelicity.repr }

def Features.instReprTelicity.repr : Telicity → ℕ → Std.Format

Equations

• Features.instReprTelicity.repr Features.Telicity.telic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Telicity.telic")).group prec✝
• Features.instReprTelicity.repr Features.Telicity.atelic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Telicity.atelic")).group prec✝

def Features.instInhabitedTelicity.default : Telicity

Equations

• Features.instInhabitedTelicity.default = Features.Telicity.telic

@[implicit_reducible]

instance Features.instInhabitedTelicity : Inhabited Telicity

Equations

• Features.instInhabitedTelicity = { default := Features.instInhabitedTelicity.default }

inductive Features.Duration : Type

Duration: whether an event takes time or is instantaneous.

• durative : Duration
• punctual : Duration

@[implicit_reducible]

instance Features.instDecidableEqDuration : DecidableEq Duration

Equations

• Features.instDecidableEqDuration x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprDuration : Repr Duration

Equations

• Features.instReprDuration = { reprPrec := Features.instReprDuration.repr }

def Features.instReprDuration.repr : Duration → ℕ → Std.Format

Equations

• Features.instReprDuration.repr Features.Duration.durative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Duration.durative")).group prec✝
• Features.instReprDuration.repr Features.Duration.punctual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Duration.punctual")).group prec✝

@[implicit_reducible]

instance Features.instInhabitedDuration : Inhabited Duration

Equations

• Features.instInhabitedDuration = { default := Features.instInhabitedDuration.default }

def Features.instInhabitedDuration.default : Duration

Equations

• Features.instInhabitedDuration.default = Features.Duration.durative

inductive Features.Dynamicity : Type

Dynamicity: whether the event involves change.

• dynamic : Dynamicity
• stative : Dynamicity

@[implicit_reducible]

instance Features.instDecidableEqDynamicity : DecidableEq Dynamicity

Equations

• Features.instDecidableEqDynamicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprDynamicity.repr : Dynamicity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprDynamicity : Repr Dynamicity

Equations

• Features.instReprDynamicity = { reprPrec := Features.instReprDynamicity.repr }

def Features.instInhabitedDynamicity.default : Dynamicity

Equations

• Features.instInhabitedDynamicity.default = Features.Dynamicity.dynamic

@[implicit_reducible]

instance Features.instInhabitedDynamicity : Inhabited Dynamicity

Equations

• Features.instInhabitedDynamicity = { default := Features.instInhabitedDynamicity.default }

def Features.Telicity.toMereoTag : Telicity → Core.Scale.MereoTag

Telicity → MereoTag: telic = quantized. Telic predicates are QUA (no proper part of a telic event is telic); atelic predicates are CUM (the sum of two atelic events is atelic).

Equations

• Features.Telicity.telic.toMereoTag = Core.Scale.MereoTag.qua
• Features.Telicity.atelic.toMereoTag = Core.Scale.MereoTag.cum

inductive Features.VendlerClass : Type

Five-way situation type classification (@cite{smith-1997}). Three binary features [±dynamic, ±durative, ±telic] yield five classes. The name VendlerClass is retained for compatibility; @cite{vendler-1957} identified the first four, @cite{smith-1997} added semelfactives.

• state : VendlerClass
• activity : VendlerClass
• achievement : VendlerClass
• accomplishment : VendlerClass
• semelfactive : VendlerClass

@[implicit_reducible]

instance Features.instDecidableEqVendlerClass : DecidableEq VendlerClass

Equations

• Features.instDecidableEqVendlerClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprVendlerClass.repr : VendlerClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprVendlerClass : Repr VendlerClass

Equations

• Features.instReprVendlerClass = { reprPrec := Features.instReprVendlerClass.repr }

def Features.instInhabitedVendlerClass.default : VendlerClass

Equations

• Features.instInhabitedVendlerClass.default = Features.VendlerClass.state

@[implicit_reducible]

instance Features.instInhabitedVendlerClass : Inhabited VendlerClass

Equations

• Features.instInhabitedVendlerClass = { default := Features.instInhabitedVendlerClass.default }

def Features.VendlerClass.telicity : VendlerClass → Telicity

Get the telicity of a Vendler class (states treated as atelic).

Equations

• Features.VendlerClass.state.telicity = Features.Telicity.atelic
• Features.VendlerClass.activity.telicity = Features.Telicity.atelic
• Features.VendlerClass.achievement.telicity = Features.Telicity.telic
• Features.VendlerClass.accomplishment.telicity = Features.Telicity.telic
• Features.VendlerClass.semelfactive.telicity = Features.Telicity.atelic

def Features.VendlerClass.duration : VendlerClass → Duration

Get the duration of a Vendler class.

Equations

• Features.VendlerClass.state.duration = Features.Duration.durative
• Features.VendlerClass.activity.duration = Features.Duration.durative
• Features.VendlerClass.achievement.duration = Features.Duration.punctual
• Features.VendlerClass.accomplishment.duration = Features.Duration.durative
• Features.VendlerClass.semelfactive.duration = Features.Duration.punctual

def Features.VendlerClass.dynamicity : VendlerClass → Dynamicity

Get the dynamicity of a Vendler class.

Equations

• Features.VendlerClass.state.dynamicity = Features.Dynamicity.stative
• Features.VendlerClass.activity.dynamicity = Features.Dynamicity.dynamic
• Features.VendlerClass.achievement.dynamicity = Features.Dynamicity.dynamic
• Features.VendlerClass.accomplishment.dynamicity = Features.Dynamicity.dynamic
• Features.VendlerClass.semelfactive.dynamicity = Features.Dynamicity.dynamic

@[implicit_reducible]

instance Features.instLicensingPipelineTelicity : Core.Scale.LicensingPipeline Telicity

Equations

• Features.instLicensingPipelineTelicity = { toBoundedness := fun (t : Features.Telicity) => t.toMereoTag.toBoundedness }

@[implicit_reducible]

instance Features.instLicensingPipelineVendlerClass : Core.Scale.LicensingPipeline VendlerClass

Equations

• Features.instLicensingPipelineVendlerClass = { toBoundedness := fun (v : Features.VendlerClass) => v.telicity.toMereoTag.toBoundedness }

theorem Features.state_is_stative : VendlerClass.state.dynamicity = Dynamicity.stative

States are stative.

theorem Features.activity_is_atelic : VendlerClass.activity.telicity = Telicity.atelic

Activities are atelic.

theorem Features.activity_is_durative : VendlerClass.activity.duration = Duration.durative

Activities are durative.

theorem Features.achievement_is_punctual : VendlerClass.achievement.duration = Duration.punctual

Achievements are punctual.

theorem Features.achievement_is_telic : VendlerClass.achievement.telicity = Telicity.telic

Achievements are telic.

theorem Features.accomplishment_is_telic : VendlerClass.accomplishment.telicity = Telicity.telic

Accomplishments are telic.

theorem Features.accomplishment_is_durative : VendlerClass.accomplishment.duration = Duration.durative

Accomplishments are durative.

theorem Features.semelfactive_is_atelic : VendlerClass.semelfactive.telicity = Telicity.atelic

Semelfactives are atelic.

theorem Features.semelfactive_is_punctual : VendlerClass.semelfactive.duration = Duration.punctual

Semelfactives are punctual.

theorem Features.semelfactive_is_dynamic : VendlerClass.semelfactive.dynamicity = Dynamicity.dynamic

Semelfactives are dynamic.

theorem Features.dynamic_classes_are_dynamic (c : VendlerClass) : c ≠ VendlerClass.state → c.dynamicity = Dynamicity.dynamic

All dynamic classes involve change.

theorem Features.telic_classes (c : VendlerClass) : c.telicity = Telicity.telic ↔ c = VendlerClass.achievement ∨ c = VendlerClass.accomplishment

All telic classes have endpoints.

structure Features.AspectualProfile : Type

An aspectual profile bundles telicity, duration, and dynamicity.

• telicity : Telicity

  Whether the eventuality has a natural endpoint

• duration : Duration

  Whether the eventuality takes time

• dynamicity : Dynamicity

  Whether the eventuality involves change

@[implicit_reducible]

instance Features.instDecidableEqAspectualProfile : DecidableEq AspectualProfile

Equations

• Features.instDecidableEqAspectualProfile = Features.instDecidableEqAspectualProfile.decEq

def Features.instDecidableEqAspectualProfile.decEq (x✝ x✝¹ : AspectualProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Features.instReprAspectualProfile.repr : AspectualProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprAspectualProfile : Repr AspectualProfile

Equations

• Features.instReprAspectualProfile = { reprPrec := Features.instReprAspectualProfile.repr }

def Features.AspectualProfile.toVendlerClass (p : AspectualProfile) : VendlerClass

Convert an aspectual profile to a situation type. All five [±dynamic, ±durative, ±telic] combinations are distinguished.

Equations

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

def Features.AspectualProfile.telicize (p : AspectualProfile) : AspectualProfile

Telicize: add a natural endpoint to an atelic predicate.

Equations

• p.telicize = { telicity := Features.Telicity.telic, duration := p.duration, dynamicity := p.dynamicity }

def Features.AspectualProfile.atelicize (p : AspectualProfile) : AspectualProfile

Atelicize: remove the natural endpoint (progressive effect).

Equations

• p.atelicize = { telicity := Features.Telicity.atelic, duration := p.duration, dynamicity := p.dynamicity }

def Features.AspectualProfile.duratize (p : AspectualProfile) : AspectualProfile

Duratize: stretch a punctual event over time (iterative).

Equations

• p.duratize = { telicity := p.telicity, duration := Features.Duration.durative, dynamicity := p.dynamicity }

def Features.AspectualProfile.statify (p : AspectualProfile) : AspectualProfile

Statify: convert to a stative reading.

Equations

• p.statify = { telicity := p.telicity, duration := p.duration, dynamicity := Features.Dynamicity.stative }

def Features.VendlerClass.toProfile (c : VendlerClass) : AspectualProfile

Convert a Vendler class to its canonical aspectual profile.

Equations

• c.toProfile = { telicity := c.telicity, duration := c.duration, dynamicity := c.dynamicity }

def Features.stateProfile : AspectualProfile

Canonical profile for states.

Equations

• Features.stateProfile = { telicity := Features.Telicity.atelic, duration := Features.Duration.durative, dynamicity := Features.Dynamicity.stative }

def Features.activityProfile : AspectualProfile

Canonical profile for activities.

Equations

• Features.activityProfile = { telicity := Features.Telicity.atelic, duration := Features.Duration.durative, dynamicity := Features.Dynamicity.dynamic }

def Features.achievementProfile : AspectualProfile

Canonical profile for achievements.

Equations

• Features.achievementProfile = { telicity := Features.Telicity.telic, duration := Features.Duration.punctual, dynamicity := Features.Dynamicity.dynamic }

def Features.accomplishmentProfile : AspectualProfile

Canonical profile for accomplishments.

Equations

• Features.accomplishmentProfile = { telicity := Features.Telicity.telic, duration := Features.Duration.durative, dynamicity := Features.Dynamicity.dynamic }

def Features.semelfactiveProfile : AspectualProfile

Canonical profile for semelfactives.

Equations

• Features.semelfactiveProfile = { telicity := Features.Telicity.atelic, duration := Features.Duration.punctual, dynamicity := Features.Dynamicity.dynamic }

@[simp]

theorem Features.vendler_profile_roundtrip (c : VendlerClass) : c.toProfile.toVendlerClass = c

Converting a situation type to a profile and back is identity.

@[simp]

theorem Features.stateProfile_toClass : stateProfile.toVendlerClass = VendlerClass.state

The canonical state profile maps to the state class.

@[simp]

theorem Features.activityProfile_toClass : activityProfile.toVendlerClass = VendlerClass.activity

The canonical activity profile maps to the activity class.

@[simp]

theorem Features.achievementProfile_toClass : achievementProfile.toVendlerClass = VendlerClass.achievement

The canonical achievement profile maps to the achievement class.

@[simp]

theorem Features.accomplishmentProfile_toClass : accomplishmentProfile.toVendlerClass = VendlerClass.accomplishment

The canonical accomplishment profile maps to the accomplishment class.

@[simp]

theorem Features.semelfactiveProfile_toClass : semelfactiveProfile.toVendlerClass = VendlerClass.semelfactive

The canonical semelfactive profile maps to the semelfactive class.

theorem Features.telicize_activity : activityProfile.telicize.toVendlerClass = VendlerClass.accomplishment

Telicizing an activity yields an accomplishment.

theorem Features.atelicize_accomplishment : accomplishmentProfile.atelicize.toVendlerClass = VendlerClass.activity

Atelicizing an accomplishment yields an activity.

theorem Features.duratize_achievement : achievementProfile.duratize.toVendlerClass = VendlerClass.accomplishment

Duratizing an achievement yields an accomplishment.

theorem Features.duratize_semelfactive : semelfactiveProfile.duratize.toVendlerClass = VendlerClass.activity

Duratizing a semelfactive yields an activity (iterative reading).

theorem Features.telicize_semelfactive : semelfactiveProfile.telicize.toVendlerClass = VendlerClass.achievement

Telicizing a semelfactive yields an achievement.

theorem Features.telicize_idempotent (p : AspectualProfile) : p.telicize.telicize = p.telicize

Telicize is idempotent.

theorem Features.atelicize_idempotent (p : AspectualProfile) : p.atelicize.atelicize = p.atelicize

Atelicize is idempotent.