Documentation

Linglib.Features.Aktionsart

Features.Aktionsart #

[Ven57] [Smi97]

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 / [Smi97] (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 Semantics/Events/CEM.lean — that is the substrate; the Telicity here is the Smith-flavored derived label.

Sibling formalizations of competitor lexical-aspect frameworks: [Bac86]; the event-token sort is this Dynamicity feature (Event.sort); [Kri89]/[Kri98] CUM/QUA/DIV in Semantics/Events/CEM.lean; [Dow79] SIP in Semantics/Aspect/SubintervalProperty.lean; [Fil12] three-way refutation of binary telicity in Studies/Filip2012.lean.

inductive Features.Telicity :

Telicity: whether an event has a natural endpoint.

telic : Telicity
atelic : Telicity

Instances For

@[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 :

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✝

Instances For

@[implicit_reducible]

instance Features.instInhabitedTelicity :

Inhabited Telicity

Equations

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

inductive Features.Duration :

Duration: whether an event takes time or is instantaneous.

durative : Duration
punctual : Duration

Instances For

@[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 :

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✝

Instances For

@[implicit_reducible]

instance Features.instInhabitedDuration :

Inhabited Duration

Equations

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

inductive Features.Dynamicity :

Dynamicity: whether the event involves change.

dynamic : Dynamicity
stative : Dynamicity

Instances For

@[implicit_reducible]

instance Features.instDecidableEqDynamicity :

DecidableEq Dynamicity

Equations

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

@[implicit_reducible]

instance Features.instReprDynamicity :

Repr Dynamicity

Equations

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

def Features.instReprDynamicity.repr :

Dynamicity → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instInhabitedDynamicity :

Inhabited Dynamicity

Equations

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

def Features.Telicity.toMereoTag :

Telicity → Core.Order.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

Instances For

inductive Features.VendlerClass :

Five-way situation type classification ([Smi97]). Three binary features [±dynamic, ±durative, ±telic] yield five classes. The name VendlerClass is retained for compatibility; [Ven57] identified the first four, [Smi97] added semelfactives.

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

Instances For

@[implicit_reducible]

instance Features.instDecidableEqVendlerClass :

DecidableEq VendlerClass

Equations

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

@[implicit_reducible]

instance Features.instReprVendlerClass :

Repr VendlerClass

Equations

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

def Features.instReprVendlerClass.repr :

VendlerClass → ℕ → Std.Format

Equations

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

Instances For

@[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

Instances For

def Features.VendlerClass.duration :

VendlerClass → Duration

Get the duration of a Vendler class.

Equations

Instances For

def Features.VendlerClass.dynamicity :

VendlerClass → Dynamicity

Get the dynamicity of a Vendler class.

Equations

Instances For

@[implicit_reducible]

instance Features.instLicensingPipelineTelicity :

Core.Order.LicensingPipeline Telicity

Equations

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

@[implicit_reducible]

instance Features.instLicensingPipelineVendlerClass :

Core.Order.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.

def Features.VendlerClass.HasInternalStages (c : VendlerClass) :

A Vendler class has internal stages iff it is both dynamic and durative. [Smi97] Ch. 4: the progressive focuses internal stages, so classes without them (states, punctuals) resist the progressive.

Equations

c.HasInternalStages = (c.dynamicity = Features.Dynamicity.dynamic ∧ c.duration = Features.Duration.durative)

Instances For

@[implicit_reducible]

instance Features.VendlerClass.instDecidableHasInternalStages (c : VendlerClass) :

Decidable c.HasInternalStages

Equations

c.instDecidableHasInternalStages = Features.VendlerClass.instDecidableHasInternalStages._aux_1 c

structure Features.AspectualProfile :

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

Instances For

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Features.instDecidableEqAspectualProfile :

DecidableEq AspectualProfile

Equations

Features.instDecidableEqAspectualProfile = Features.instDecidableEqAspectualProfile.decEq

def Features.instReprAspectualProfile.repr :

AspectualProfile → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instReprAspectualProfile :

Repr AspectualProfile

Equations

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

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

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.

Instances For

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 }

Instances For

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 }

Instances For

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 }

Instances For

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 }

Instances For

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 }

Instances For

def Features.stateProfile :

AspectualProfile

Canonical profile for states.

Equations

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

Instances For

def Features.activityProfile :

AspectualProfile

Canonical profile for activities.

Equations

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

Instances For

def Features.achievementProfile :

AspectualProfile

Canonical profile for achievements.

Equations

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

Instances For

def Features.accomplishmentProfile :

AspectualProfile

Canonical profile for accomplishments.

Equations

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

Instances For

def Features.semelfactiveProfile :

AspectualProfile

Canonical profile for semelfactives.

Equations

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

Instances For

@[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.

Aspectual diagnostics #

[Ven57] [Dow79]

The textbook test battery: for-X and in-X adverbials, the progressive, stop V-ing, and the imperative. Each prediction is a function of VendlerClass, and the derivation theorems show the predictions are consequences of the three-feature decomposition (telicity, duration, dynamicity), not independent stipulations.

inductive Features.DiagnosticResult :

Result of applying an aspectual diagnostic: felicitous, infelicitous, degraded, or acceptable only under a meaning shift.

Instances For

@[implicit_reducible]

instance Features.instDecidableEqDiagnosticResult :

DecidableEq DiagnosticResult

Equations

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

def Features.instReprDiagnosticResult.repr :

DiagnosticResult → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instReprDiagnosticResult :

Repr DiagnosticResult

Equations

Features.instReprDiagnosticResult = { reprPrec := Features.instReprDiagnosticResult.repr }

def Features.forXPrediction :

VendlerClass → DiagnosticResult

for-X adverbial: measures the duration of an atelic eventuality ("ran for an hour" ✓, *"arrived for an hour"; "built houses for a year" coerces to repetition, "coughed for an hour" to iteration).

Equations

Instances For

def Features.inXPrediction :

VendlerClass → DiagnosticResult

in-X adverbial: measures time to a culmination point ("built the house in a year" ✓, *"ran in an hour").

Equations

Instances For

def Features.progressivePrediction :

VendlerClass → DiagnosticResult

Progressive: requires ongoing, dynamic eventualities ("is running" ✓, *"is knowing French"; "is arriving" marginal via preliminary stages, "is coughing" coerces to iteration).

Equations

Instances For

def Features.stopVingPrediction :

VendlerClass → DiagnosticResult

stop V-ing: presupposes an ongoing eventuality that ceases ("stopped running" ✓; "stopped loving her" needs an inchoative reading, "stopped recognizing" an iterative one).

Equations

Instances For

def Features.imperativePrediction :

VendlerClass → DiagnosticResult

Imperative: requires agentive control ("Run!" ✓, *"Know French!"; "Cough!" ✓).

Equations

Instances For

theorem Features.inX_identifies_telic (c : VendlerClass) :

inXPrediction c = DiagnosticResult.accept ↔ c.telicity = Telicity.telic

in-X acceptance is exactly telicity: the diagnostic follows from the telicity feature.

theorem Features.forX_from_features (c : VendlerClass) :

forXPrediction c = DiagnosticResult.accept ↔ c.telicity = Telicity.atelic ∧ c.duration = Duration.durative

for-X acceptance is exactly atelicity plus duration: semelfactives are atelic but punctual, so they only accept for-X with iterative coercion.

theorem Features.forX_semelfactive_coercion :

forXPrediction VendlerClass.semelfactive = DiagnosticResult.coerced ∧ VendlerClass.semelfactive.telicity = Telicity.atelic ∧ VendlerClass.semelfactive.duration = Duration.punctual

Semelfactive coercion under for-X derives from being atelic but punctual: atelicity licenses temporal modification, punctuality forces iterative reinterpretation.

theorem Features.progressive_accepts_durative_dynamic (c : VendlerClass) :

progressivePrediction c = DiagnosticResult.accept ↔ c.duration = Duration.durative ∧ c.dynamicity = Dynamicity.dynamic

Progressive acceptance is exactly duration plus dynamicity: states fail (not dynamic), achievements and semelfactives fail (not durative).