Filip (2012): Lexical aspect

This file formalizes the mereological core of [Fil12]'s survey of lexical aspect. The telic/atelic distinction is diagnosed by temporal adverbials — in an hour with telic and for an hour with atelic predicates (1) — and, following [Kri98], telic predicates are taken as quantized (23) and atelic ones as cumulative (24), the substrate's QUA and CUM. Aspectual composition (25)–(27) is [Kri89]'s: the predicate an incremental verb forms with its object is quantized or cumulative as the object is, the substrate's vp_qua and vp_cum for a strictly incremental relation, while a verb without the incremental mapping, like watch, is atelic whatever its object (26). Hence the three classes of (28): telic verbs, whose eventualities have no proper parts in the relation (Quantized, telic_of_quantized); atelic verbs, whose relation persists to the parts of an eventuality, the subinterval property (19) (Persistent, not_telic_of_persistent); and incremental verbs, lexically unmarked for telicity because their non-degeneracy provides both a quantized and a cumulative object (incremental_underspecified). Incrementality and telicity are independent (29): a quantized verb is not strictly incremental (not_sinc_of_quantized), and an incremental verb with a cumulative object is atelic. The diagnostic data (1), (25), (26), (31), (37) are rows of Data/Examples/Filip2012.json, and rows_test checks the adverbial judgments against the telicity the classification assigns.

Implementation notes

• Telicity is identified with quantization "for the purposes of this summary" (§7), so the telic/atelic contrast is the substrate's QUA/CUM and the atelic verbs' persistence is stated with ≤ on eventualities.
• The verb classes of the rows are the chapter's: recover and reach telic, swim and watch atelic, eat and prove incremental; Row.Telic states the classification's verdict, whose semantic content is the theorems above.
• The chapter's surveys of Vendler's and Dowty's classifications (§§3–6) and of degree-based approaches (§8) summarize other authors' analyses and are not formalized here.

References

• [Fil12]
• [Kri89]
• [Kri98]
• [BP72]
• [Ven57]
• [Dow79]

Telic and atelic predicates (23)–(24)

@[reducible, inline]

abbrev Filip2012.Telic {β : Type u_2} [SemilatticeSup β] (P : β → Prop) : Prop

(23): a telic predicate is quantized.

Equations

• Filip2012.Telic P = Mereology.QUA P

@[reducible, inline]

abbrev Filip2012.Atelic {β : Type u_2} [SemilatticeSup β] (P : β → Prop) : Prop

(24): an atelic predicate is cumulative.

Equations

• Filip2012.Atelic P = Mereology.CUM P

theorem Filip2012.isTelic_of_telic {β : Type u_2} [SemilatticeSup β] {precedes : β → β → Prop} (h : Aspect.NoPartPrecedes precedes) {P : β → Prop} (hP : Telic P) : Aspect.IsTelic precedes P

A predicate telic in this sense is telic in the initial and final part sense of [Kri98], where parts of an event neither precede nor follow it.

The three classes of verbs (28)

def Filip2012.Quantized {α : Type u_1} {β : Type u_2} [SemilatticeSup β] (θ : α → β → Prop) : Prop

A telic verb (28i): no eventuality in its relation has a proper part in it — recover, arrive, burst.

Equations

• Filip2012.Quantized θ = ∀ (x : α) (e : β), θ x e → ∀ (y : α), ∀ e' < e, ¬θ y e'

def Filip2012.Persistent {α : Type u_1} {β : Type u_2} [SemilatticeSup β] (θ : α → β → Prop) : Prop

An atelic verb (28ii): its relation persists to the parts of an eventuality, the subinterval property (19) — run, watch, believe.

Equations

• Filip2012.Persistent θ = ∀ (x : α) (e : β), θ x e → ∀ e' ≤ e, θ x e'

theorem Filip2012.telic_of_quantized {α : Type u_1} {β : Type u_2} [SemilatticeSup β] {θ : α → β → Prop} (h : Quantized θ) (OBJ : α → Prop) : Telic (Aspect.VP θ OBJ)

A telic verb forms a telic predicate with any object.

theorem Filip2012.not_telic_of_persistent {α : Type u_1} {β : Type u_2} [SemilatticeSup β] {θ : α → β → Prop} (h : Persistent θ) (OBJ : α → Prop) {e e' : β} (hlt : e' < e) (he : Aspect.VP θ OBJ e) : ¬Telic (Aspect.VP θ OBJ)

(26): an atelic verb forms no telic predicate whatever its object: a proper part of one of its eventualities is one too.

theorem Filip2012.atelic_of_persistent {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (hθ : Mereology.SUM θ) {OBJ : α → Prop} (hObj : Mereology.CUM OBJ) : Atelic (Aspect.VP θ OBJ)

An atelic verb with a cumulative object forms a cumulative predicate.

theorem Filip2012.incremental_underspecified {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : Aspect.SINC θ) (hU : Mereology.UP θ) (hs : Mereology.SUM θ) : (∃ (OBJ : α → Prop), Mereology.QUA OBJ ∧ Telic (Aspect.VP θ OBJ) ∧ ∃ (e : β), Aspect.VP θ OBJ e) ∧ ∃ (OBJ : α → Prop), Mereology.CUM OBJ ∧ Atelic (Aspect.VP θ OBJ) ∧ ¬Telic (Aspect.VP θ OBJ)

(27), (28iii), (29ii): an incremental verb is lexically unmarked for telicity — its non-degeneracy provides a quantized object with which its predicate is telic and a cumulative one with which it is atelic and not telic.

theorem Filip2012.not_sinc_of_quantized {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : Quantized θ) : ¬Aspect.SINC θ

(29i): telicity does not require incrementality — a quantized verb is not strictly incremental, its eventualities having no proper parts in the relation.

The adverbial diagnostic (1) over the chapter's data

inductive Filip2012.VerbClass : Type

The verb classes of (28).

• telic : VerbClass
• atelic : VerbClass
• incremental : VerbClass

@[instance_reducible]

instance Filip2012.instDecidableEqVerbClass : DecidableEq VerbClass

Equations

• Filip2012.instDecidableEqVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Filip2012.instReprVerbClass.repr : VerbClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Filip2012.instReprVerbClass.repr Filip2012.VerbClass.telic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.VerbClass.telic")).group prec✝
• Filip2012.instReprVerbClass.repr Filip2012.VerbClass.atelic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.VerbClass.atelic")).group prec✝

@[instance_reducible]

instance Filip2012.instReprVerbClass : Repr VerbClass

Equations

• Filip2012.instReprVerbClass = { reprPrec := Filip2012.instReprVerbClass.repr }

inductive Filip2012.Object : Type

The object's reference: quantized, cumulative, or absent.

• quantized : Object
• cumulative : Object
• none : Object

@[instance_reducible]

instance Filip2012.instDecidableEqObject : DecidableEq Object

Equations

• Filip2012.instDecidableEqObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Filip2012.instReprObject : Repr Object

Equations

• Filip2012.instReprObject = { reprPrec := Filip2012.instReprObject.repr }

def Filip2012.instReprObject.repr : Object → ℕ → Std.Format

Equations

• Filip2012.instReprObject.repr Filip2012.Object.quantized prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.Object.quantized")).group prec✝
• Filip2012.instReprObject.repr Filip2012.Object.cumulative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.Object.cumulative")).group prec✝
• Filip2012.instReprObject.repr Filip2012.Object.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.Object.none")).group prec✝

inductive Filip2012.Adverbial : Type

The temporal adverbials of (1).

• inNP : Adverbial
• forNP : Adverbial

@[instance_reducible]

instance Filip2012.instDecidableEqAdverbial : DecidableEq Adverbial

Equations

• Filip2012.instDecidableEqAdverbial x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Filip2012.instReprAdverbial.repr : Adverbial → ℕ → Std.Format

Equations

• Filip2012.instReprAdverbial.repr Filip2012.Adverbial.inNP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.Adverbial.inNP")).group prec✝
• Filip2012.instReprAdverbial.repr Filip2012.Adverbial.forNP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Filip2012.Adverbial.forNP")).group prec✝

@[instance_reducible]

instance Filip2012.instReprAdverbial : Repr Adverbial

Equations

• Filip2012.instReprAdverbial = { reprPrec := Filip2012.instReprAdverbial.repr }

structure Filip2012.Row : Type

A sentence of the diagnostic with its verb's class, its object's reference, its adverbial, and the chapter's judgment.

• cls : VerbClass
• obj : Object
• adverbial : Adverbial
• judgment : Judgment

@[instance_reducible]

instance Filip2012.instDecidableEqRow : DecidableEq Row

Equations

• Filip2012.instDecidableEqRow = Filip2012.instDecidableEqRow.decEq

def Filip2012.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Filip2012.instReprRow : Repr Row

Equations

• Filip2012.instReprRow = { reprPrec := Filip2012.instReprRow.repr }

def Filip2012.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Filip2012.Row.Telic (r : Row) : Prop

The telicity the classification assigns: telic verbs form telic predicates (telic_of_quantized), atelic verbs never do (not_telic_of_persistent), and incremental verbs follow their object ((27): vp_qua, vp_cum).

Equations

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

@[instance_reducible]

instance Filip2012.instDecidableTelic (r : Row) : Decidable r.Telic

Equations

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

def Filip2012.classTable : List (String × VerbClass)

Equations

• Filip2012.classTable = [("telic", Filip2012.VerbClass.telic), ("atelic", Filip2012.VerbClass.atelic), ("incremental", Filip2012.VerbClass.incremental)]

def Filip2012.objectTable : List (String × Object)

Equations

• Filip2012.objectTable = [("quantized", Filip2012.Object.quantized), ("cumulative", Filip2012.Object.cumulative), ("none", Filip2012.Object.none)]

def Filip2012.adverbialTable : List (String × Adverbial)

Equations

• Filip2012.adverbialTable = [("in", Filip2012.Adverbial.inNP), ("for", Filip2012.Adverbial.forNP)]

def Filip2012.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem Filip2012.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def Filip2012.rows : List Row

Equations

• Filip2012.rows = List.filterMap Filip2012.Row.ofDatum Filip2012.Examples.all

theorem Filip2012.rows_test (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ (r.adverbial = Adverbial.inNP ↔ r.Telic))

(1): the in adverbial is acceptable exactly with the telic predicates and the for adverbial exactly with the atelic ones, across (1), (25), (26), (31), (37).