Aspect: basic definitions

This file defines the classificatory vocabulary of aspect, following the two components of Smith's theory. Situation type classifies an eventuality by three binary features: whether it has a natural endpoint (Telicity), whether it takes time (Duration) and whether it involves change (Dynamicity). The situation types are the four classes of Vendler together with Smith's semelfactives (VendlerClass), each determined by its features (VendlerClass.eq_of_features). The aspectual shifts of compositional coercion change one feature of a situation type (VendlerClass.telicize and its siblings), and Dowty's adverbial and progressive diagnostics are functions of the features (forXPrediction, inXPrediction, progressivePrediction). Viewpoint is the presentation of a situation, Klein's four relations between the topic time and the situation time together with Smith's neutral viewpoint (ViewpointType), and at its coarsest the opposition of perfective and imperfective (Perfectivity). A language's aspect morphemes are entered with the viewpoint each marks in Semantics/Aspect/Marker.lean, and the operators that viewpoints denote are in Semantics/Aspect/Viewpoint.lean.

Main definitions

• Aspect.VendlerClass: the five situation types, with their features and shifts.
• Aspect.Incrementality: the incrementality classes of a verb's theme relation.
• Aspect.DiagnosticResult: the outcome of a diagnostic, with the for-adverbial, in-adverbial and progressive tests as functions of a situation type.
• Aspect.ViewpointType, Aspect.Perfectivity: the viewpoints.

References

• [Smi97]
• [Ven57]
• [Dow79]
• [Kri98]
• [Kle94]

Situation type

inductive Aspect.Telicity : Type

Whether an eventuality has a natural endpoint.

• telic : Telicity
• atelic : Telicity

@[instance_reducible]

instance Aspect.instDecidableEqTelicity : DecidableEq Telicity

Equations

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

@[instance_reducible]

instance Aspect.instReprTelicity : Repr Telicity

Equations

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

def Aspect.instReprTelicity.repr : Telicity → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Aspect.instInhabitedTelicity : Inhabited Telicity

Equations

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

inductive Aspect.Duration : Type

Whether an eventuality takes time or is instantaneous.

• durative : Duration
• punctual : Duration

@[instance_reducible]

instance Aspect.instDecidableEqDuration : DecidableEq Duration

Equations

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

def Aspect.instReprDuration.repr : Duration → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Aspect.instReprDuration : Repr Duration

Equations

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

@[instance_reducible]

instance Aspect.instInhabitedDuration : Inhabited Duration

Equations

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

inductive Aspect.Dynamicity : Type

Whether an eventuality involves change.

• dynamic : Dynamicity
• stative : Dynamicity

@[instance_reducible]

instance Aspect.instDecidableEqDynamicity : DecidableEq Dynamicity

Equations

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

@[instance_reducible]

instance Aspect.instReprDynamicity : Repr Dynamicity

Equations

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

def Aspect.instReprDynamicity.repr : Dynamicity → Nat → Std.Format

Equations

• Aspect.instReprDynamicity.repr Aspect.Dynamicity.dynamic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aspect.Dynamicity.dynamic")).group prec✝
• Aspect.instReprDynamicity.repr Aspect.Dynamicity.stative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aspect.Dynamicity.stative")).group prec✝

@[instance_reducible]

instance Aspect.instInhabitedDynamicity : Inhabited Dynamicity

Equations

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

inductive Aspect.VendlerClass : Type

The five situation types are the four classes of [Ven57] and the semelfactives of [Smi97].

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

@[instance_reducible]

instance Aspect.instDecidableEqVendlerClass : DecidableEq VendlerClass

Equations

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

@[instance_reducible]

instance Aspect.instReprVendlerClass : Repr VendlerClass

Equations

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

def Aspect.instReprVendlerClass.repr : VendlerClass → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Aspect.instReprVendlerClass.repr Aspect.VendlerClass.state prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aspect.VendlerClass.state")).group prec✝

@[instance_reducible]

instance Aspect.instInhabitedVendlerClass : Inhabited VendlerClass

Equations

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

def Aspect.VendlerClass.telicity : VendlerClass → Telicity

The telicity of a situation type.

Equations

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

def Aspect.VendlerClass.duration : VendlerClass → Duration

The duration of a situation type.

Equations

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

def Aspect.VendlerClass.dynamicity : VendlerClass → Dynamicity

The dynamicity of a situation type.

Equations

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

theorem Aspect.VendlerClass.eq_of_features {c d : VendlerClass} (ht : c.telicity = d.telicity) (hd : c.duration = d.duration) (hy : c.dynamicity = d.dynamicity) : c = d

A situation type is determined by its three features.

def Aspect.VendlerClass.telicize : VendlerClass → VendlerClass

Add a natural endpoint, by which an activity becomes an accomplishment and a semelfactive an achievement.

Equations

• Aspect.VendlerClass.activity.telicize = Aspect.VendlerClass.accomplishment
• Aspect.VendlerClass.semelfactive.telicize = Aspect.VendlerClass.achievement
• x✝.telicize = x✝

def Aspect.VendlerClass.atelicize : VendlerClass → VendlerClass

Remove the natural endpoint, the effect of the progressive.

Equations

• Aspect.VendlerClass.accomplishment.atelicize = Aspect.VendlerClass.activity
• Aspect.VendlerClass.achievement.atelicize = Aspect.VendlerClass.semelfactive
• x✝.atelicize = x✝

def Aspect.VendlerClass.duratize : VendlerClass → VendlerClass

Stretch a punctual eventuality over time, the iterative reading.

Equations

• Aspect.VendlerClass.achievement.duratize = Aspect.VendlerClass.accomplishment
• Aspect.VendlerClass.semelfactive.duratize = Aspect.VendlerClass.activity
• x✝.duratize = x✝

theorem Aspect.VendlerClass.telicity_telicize {c : VendlerClass} (h : c.dynamicity = Dynamicity.dynamic) : c.telicize.telicity = Telicity.telic

@[simp]

theorem Aspect.VendlerClass.duration_telicize (c : VendlerClass) : c.telicize.duration = c.duration

@[simp]

theorem Aspect.VendlerClass.dynamicity_telicize (c : VendlerClass) : c.telicize.dynamicity = c.dynamicity

@[simp]

theorem Aspect.VendlerClass.telicity_atelicize (c : VendlerClass) : c.atelicize.telicity = Telicity.atelic

@[simp]

theorem Aspect.VendlerClass.duration_atelicize (c : VendlerClass) : c.atelicize.duration = c.duration

@[simp]

theorem Aspect.VendlerClass.dynamicity_atelicize (c : VendlerClass) : c.atelicize.dynamicity = c.dynamicity

@[simp]

theorem Aspect.VendlerClass.duration_duratize (c : VendlerClass) : c.duratize.duration = Duration.durative

@[simp]

theorem Aspect.VendlerClass.telicity_duratize (c : VendlerClass) : c.duratize.telicity = c.telicity

@[simp]

theorem Aspect.VendlerClass.dynamicity_duratize (c : VendlerClass) : c.duratize.dynamicity = c.dynamicity

inductive Aspect.Incrementality : Type

The incrementality of a verb's theme relation is the strongest of [Kri98]'s properties it has, strictly incremental (eat, draw), incremental (read), or cumulative without incrementality (push, carry).

• strict : Incrementality
• incremental : Incrementality
• cumulative : Incrementality

@[instance_reducible]

instance Aspect.instDecidableEqIncrementality : DecidableEq Incrementality

Equations

• Aspect.instDecidableEqIncrementality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aspect.instReprIncrementality : Repr Incrementality

Equations

• Aspect.instReprIncrementality = { reprPrec := Aspect.instReprIncrementality.repr }

def Aspect.instReprIncrementality.repr : Incrementality → Nat → Std.Format

Equations

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

Diagnostics

The adverbial and progressive tests of [Dow79], as functions of the three features: a for-adverbial measures an atelic durative eventuality and coerces a telic or punctual one into repetition or iteration; an in-adverbial needs a culmination; the progressive needs internal stages, reads an achievement through its preliminary stages and a semelfactive as iterated.

inductive Aspect.DiagnosticResult : Type

The outcome of a diagnostic is acceptable, unacceptable, degraded, or acceptable under a meaning shift.

• accept : DiagnosticResult
• reject : DiagnosticResult
• marginal : DiagnosticResult
• coerced : DiagnosticResult

@[instance_reducible]

instance Aspect.instDecidableEqDiagnosticResult : DecidableEq DiagnosticResult

Equations

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

def Aspect.instReprDiagnosticResult.repr : DiagnosticResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Aspect.instReprDiagnosticResult : Repr DiagnosticResult

Equations

• Aspect.instReprDiagnosticResult = { reprPrec := Aspect.instReprDiagnosticResult.repr }

def Aspect.forXPrediction (c : VendlerClass) : DiagnosticResult

The for-adverbial test.

Equations

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

def Aspect.inXPrediction (c : VendlerClass) : DiagnosticResult

The in-adverbial test.

Equations

• Aspect.inXPrediction c = if c.telicity = Aspect.Telicity.telic then Aspect.DiagnosticResult.accept else Aspect.DiagnosticResult.reject

def Aspect.progressivePrediction (c : VendlerClass) : DiagnosticResult

The progressive test.

Equations

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

theorem Aspect.inXPrediction_eq_accept_iff (c : VendlerClass) : inXPrediction c = DiagnosticResult.accept ↔ c.telicity = Telicity.telic

theorem Aspect.forXPrediction_eq_accept_iff (c : VendlerClass) : forXPrediction c = DiagnosticResult.accept ↔ c.telicity = Telicity.atelic ∧ c.duration = Duration.durative

theorem Aspect.progressivePrediction_eq_accept_iff (c : VendlerClass) : progressivePrediction c = DiagnosticResult.accept ↔ c.duration = Duration.durative ∧ c.dynamicity = Dynamicity.dynamic

Viewpoint

inductive Aspect.ViewpointType : Type

The viewpoints are the four relations of [Kle94] between the topic time and the situation time, and the neutral viewpoint of [Smi97], the default in the absence of aspect morphology.

• imperfective : ViewpointType
• perfective : ViewpointType
• perfect : ViewpointType
• prospective : ViewpointType
• neutral : ViewpointType

@[instance_reducible]

instance Aspect.instDecidableEqViewpointType : DecidableEq ViewpointType

Equations

• Aspect.instDecidableEqViewpointType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aspect.instReprViewpointType : Repr ViewpointType

Equations

• Aspect.instReprViewpointType = { reprPrec := Aspect.instReprViewpointType.repr }

def Aspect.instReprViewpointType.repr : ViewpointType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Aspect.instInhabitedViewpointType : Inhabited ViewpointType

Equations

• Aspect.instInhabitedViewpointType = { default := Aspect.instInhabitedViewpointType.default }

inductive Aspect.Perfectivity : Type

The opposition of perfective and imperfective is viewpoint aspect at its coarsest, the right granularity where the fact at issue is that the perfective requires actualization and the imperfective does not, or where the opposition is lexically encoded, as on a Verb.Stem.

• perfective : Perfectivity
• imperfective : Perfectivity

@[instance_reducible]

instance Aspect.instDecidableEqPerfectivity : DecidableEq Perfectivity

Equations

• Aspect.instDecidableEqPerfectivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aspect.instReprPerfectivity : Repr Perfectivity

Equations

• Aspect.instReprPerfectivity = { reprPrec := Aspect.instReprPerfectivity.repr }

def Aspect.instReprPerfectivity.repr : Perfectivity → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Aspect.instInhabitedPerfectivity : Inhabited Perfectivity

Equations

• Aspect.instInhabitedPerfectivity = { default := Aspect.instInhabitedPerfectivity.default }