Champollion 2017: distributivity as a bridge between aspect and measurement

Champollion's Parts of a Whole unifies predicative distributivity, atelicity and pseudopartitive measurement under one property, stratified reference: a predicate applies to an event that divides exhaustively into parts the predicate also applies to, along some dimension. The dimension varies, thematic roles for distributivity, run time for the for-adverbial and a measure for the pseudopartitive, while the property is defined once. Lexical cumulativity, which the book assumes throughout, entails Krifka's cumulativity, and atelicity along the run time is a Schwarzschild cover into parts with properly smaller run times. Against Krifka's subregion account of for-adverbials, the book's back-and-forth scenario has stratified reference and violates the subregion presupposition. The per-verb distributivity facts are meaning postulates, stated over the Fragment verbs' denotations.

Main definitions

• StratifiedReference: an event divides into parts the predicate applies to, whose images along a dimension stand in a granularity relation to the event's.
• DistributiveReference: stratified reference along a thematic role with atomic granularity.
• SubintervalReference: stratified reference along the run time with proper subintervals.
• MeasurementReference: stratified reference along a measure with smaller values.
• Verb.StratifiesOver: a verb's denotation has distributive reference along a role.
• LexicallyCumulative: a predicate is a fixed point of algebraic closure.
• ChampollionPostulates: the per-verb distributivity postulates.

Main results

• lexicallyCumulative_imp_cum: lexical cumulativity entails Krifka's CUM.
• subintervalReference_iff_cover: atelicity is a finite cover into proper-subinterval parts.
• stratifiedReference_of_divisiveness: on a temporally separable event, Krifka's divisiveness clause gives stratified reference along the run time.
• pushCarts_stratified: the back-and-forth event of Figure 6.2 has stratified reference.
• pushCarts_not_subregion: that event fails the subregion presupposition.

Implementation notes

• Vendler classes are not among the book's primitives; its atelicity diagnostic is the subinterval-reference test.
• The granularity is a binary relation between the image of a part and the image of the whole, where the book has a unary predicate built from the whole, so that the three specializations are instances of one definition.
• Stratified reference along the runtime neither entails nor follows from Krifka's CUM: the book takes every verb to be cumulative, telic ones included, and a predicate of events of bounded length has stratified reference over dense time without being closed under sums.
• The runtime dimension of chapter 6 is any monotone map into a part order of times, so the stratified reference in play is the generic StratifiedReference τ (· < ·) rather than the interval-runtime SubintervalReference; runtimes of back-and-forth events are discontinuous (the chapter's footnote on the scenario), and the finite model takes them to be sets of instants.
• The presupposition (28) is stated as the chapter states it, with the universal clause over the temporal parts of the event; the reflexive case is the predicate at the event itself.

References

• [Cha17]

Stratified reference ([Cha17] eq. 16/17)

def Champollion2017.StratifiedReference {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (d : α → β) (γ : β → β → Prop) (P : α → Prop) (x : α) : Prop

StratifiedReference d γ P x holds when x is a sum of P-parts whose images under the dimension d stand in the granularity relation γ to the image of x, the stratified reference of [Cha17] eq. (16) with the granularity of eq. (17) made binary.

Equations

• Champollion2017.StratifiedReference d γ P x = Mereology.AlgClosure (fun (y : α) => P y ∧ γ (d y) (d x)) x

Universal stratified reference

def Champollion2017.StratifiedReferenceUniv {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (d : α → β) (γ : β → β → Prop) (P : α → Prop) : Prop

P has universal stratified reference along d at granularity γ when every P-entity has stratified reference.

Equations

• Champollion2017.StratifiedReferenceUniv d γ P = ∀ (x : α), P x → Champollion2017.StratifiedReference d γ P x

Atomic granularity (shared γ)

def Champollion2017.AtomicGranularity {β : Type u_1} [PartialOrder β] : β → β → Prop

Atomic granularity holds when the inner image is an atom of the dimension, the granularity of distributive reference along a thematic role.

Equations

• Champollion2017.AtomicGranularity inner _outer = Mereology.Atom inner

Stratified Distributive StratifiedReference ([Cha17] eq. 24)

def Champollion2017.DistributiveReference {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] (θ : α → β) (P : α → Prop) (x : α) : Prop

Stratified distributive reference is stratified reference whose dimension is a thematic role θ and whose granularity is Atom on the inner image, the outer being unused since atomicity is an absolute property ([Cha17] eq. (24)). It captures distributivity, as "The boys each saw a movie" distributes over atomic agents.

Equations

• Champollion2017.DistributiveReference θ P x = Champollion2017.StratifiedReference θ Champollion2017.AtomicGranularity P x

def Champollion2017.DistributiveReferenceUniv {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] (θ : α → β) (P : α → Prop) : Prop

P has universal distributive reference when every P-entity distributes along θ.

Equations

• Champollion2017.DistributiveReferenceUniv θ P = ∀ (x : α), P x → Champollion2017.DistributiveReference θ P x

Relational distributive reference (neo-Davidsonian roles)

Champollion's DistributiveReference takes a functional thematic role θ : α → Entity (the unique role-filler). linglib's neo-Davidsonian roles are relational, Entity → Event → Prop, Agent(a, e) — with thematic uniqueness available as Mereology.UP. RelationalDistributiveReference is the relational form, so the distributivity property composes directly with a ThematicFrame / Verb.denote without picking a role function. It coincides with the functional form on a role's graph (relationalDistributiveReference_graph).

def Champollion2017.RelationalDistributiveReference {Entity : Type u_1} {α : Type u_2} [PartialOrder Entity] [SemilatticeSup α] (R : Entity → α → Prop) (P : α → Prop) (x : α) : Prop

Relational distributive reference takes the role to be a neo-Davidsonian relation R and counts a part when it has an atomic R-filler.

Equations

• Champollion2017.RelationalDistributiveReference R P x = Mereology.AlgClosure (fun (y : α) => P y ∧ ∃ (a : Entity), R a y ∧ Mereology.Atom a) x

def Champollion2017.RelationalDistributiveReferenceUniv {Entity : Type u_1} {α : Type u_2} [PartialOrder Entity] [SemilatticeSup α] (R : Entity → α → Prop) (P : α → Prop) : Prop

P has universal relational distributive reference when every P-element distributes along R.

Equations

• Champollion2017.RelationalDistributiveReferenceUniv R P = ∀ (x : α), P x → Champollion2017.RelationalDistributiveReference R P x

theorem Champollion2017.relationalDistributiveReference_mono {Entity : Type u_1} {α : Type u_2} [PartialOrder Entity] [SemilatticeSup α] {R : Entity → α → Prop} {P Q : α → Prop} (h : ∀ (x : α), P x → Q x) (x : α) : RelationalDistributiveReference R P x → RelationalDistributiveReference R Q x

Relational distributive reference is monotone in the predicate.

theorem Champollion2017.relationalDistributiveReference_graph {Entity : Type u_1} {α : Type u_2} [PartialOrder Entity] [SemilatticeSup α] {θ : α → Entity} {P : α → Prop} {x : α} : RelationalDistributiveReference (fun (a : Entity) (y : α) => θ y = a) P x ↔ DistributiveReference θ P x

Along the graph of a functional role, relational distributive reference is the functional DistributiveReference.

Stratified Subinterval StratifiedReference ([Cha17] eq. 38)

def Champollion2017.SubintervalGranularity {T : Type u_1} [LinearOrder T] (inner outer : NonemptyInterval T) : Prop

Proper-subinterval granularity holds when the inner run time is a proper subinterval of the outer one.

Equations

• Champollion2017.SubintervalGranularity inner outer = (inner < outer)

def Champollion2017.SubintervalReference {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] (P : E → Prop) (e : E) : Prop

Stratified subinterval reference is stratified reference whose dimension is the runtime τ and whose granularity is proper subinterval, so SubintervalReference P e holds iff e can be built from P-parts with runtimes properly included in τ e ([Cha17] eq. (38)). It captures atelicity, the predicates compatible with for-adverbials having subinterval reference.

Equations

• Champollion2017.SubintervalReference P e = Champollion2017.StratifiedReference Event.τ Champollion2017.SubintervalGranularity P e

def Champollion2017.SubintervalReferenceUniv {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] (P : E → Prop) : Prop

P has universal subinterval reference when every P-event has subinterval reference.

Equations

• Champollion2017.SubintervalReferenceUniv P = ∀ (e : E), P e → Champollion2017.SubintervalReference P e

Stratified Measurement StratifiedReference

MeasurementReference is [Cha17]'s stratified measurement reference (his named property and abbreviation): Def 61 in the Ch 4 §4.6 unification, with final universal/restricted forms Defs 52–53 in Ch 7 §7.4, written as SR_{μ, λd.d < μ(x)} (thirty liters of water, five feet of snow, two degrees Celsius of global warming).

The strict-less-than granularity is Champollion's faithful translation
of [schwarzschild-2006]'s monotonic measure-function predicate
(Ch 7 eq. 8: `μ` is monotonic iff `a < b → μ(a) < μ(b)`), with the
extensive/intensive measure-function distinction ([krifka-1998])
reduced to whether the resulting measurement-reference presupposition
is satisfiable on the given substance noun.

def Champollion2017.MeasurementReference {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [Preorder β] (μ : α → β) (P : α → Prop) (x : α) : Prop

Stratified measurement reference is stratified reference whose dimension is a measure function μ and whose granularity is strict less-than on the scale, so MeasurementReference μ P x holds iff x can be decomposed into P-parts with strictly smaller μ-values.

Equations

• Champollion2017.MeasurementReference μ P x = Champollion2017.StratifiedReference μ (fun (x1 x2 : β) => x1 < x2) P x

def Champollion2017.MeasurementReferenceUniv {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [Preorder β] (μ : α → β) (P : α → Prop) : Prop

P has universal measurement reference when every P-entity has measurement reference along μ.

Equations

• Champollion2017.MeasurementReferenceUniv μ P = ∀ (x : α), P x → Champollion2017.MeasurementReference μ P x

Distributivity Constraint

@[reducible, inline]

abbrev Champollion2017.DistributivityConstraint {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (Map : α → β) (gran : β → β → Prop) (Share : α → Prop) (x : α) : Prop

The Distributivity Constraint of [Cha17] accepts a distributive construction with share Share, map Map and granularity gran describing x exactly when the share has stratified reference along the map at that granularity. Adverbial each, for-adverbials and pseudopartitives differ only in the three parameters.

Equations

• Champollion2017.DistributivityConstraint Map gran Share x = Champollion2017.StratifiedReference Map gran Share x

Construction Instances

@[reducible, inline]

abbrev Champollion2017.eachConstr {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] (θ : α → β) (Share : α → Prop) (x : α) : Prop

Adverbial each requires distributive reference along a thematic role.

Equations

• Champollion2017.eachConstr θ Share x = Champollion2017.DistributiveReference θ Share x

@[reducible, inline]

abbrev Champollion2017.forConstr {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] (Share : E → Prop) (e : E) : Prop

A for-adverbial requires its predicate to have subinterval reference.

Equations

• Champollion2017.forConstr Share e = Champollion2017.SubintervalReference Share e

Key Theorems

theorem Champollion2017.stratifiedReferenceUniv_entails_restricted {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {d : α → β} {γ : β → β → Prop} {P : α → Prop} (h : StratifiedReferenceUniv d γ P) {x : α} (hx : P x) : StratifiedReference d γ P x

StratifiedReferenceUniv entails StratifiedReference for any specific element.

theorem Champollion2017.stratifiedReference_trivial_granularity {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {d : α → β} {P : α → Prop} : StratifiedReferenceUniv d (fun (x x_1 : β) => True) P

Predicates have stratified reference for trivial granularity, since every P x is its own base-case stratum when γ is vacuously true.

theorem Champollion2017.distributiveReference_mono {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [PartialOrder β] {θ : α → β} {P Q : α → Prop} (h : ∀ (x : α), P x → Q x) (x : α) : DistributiveReference θ P x → DistributiveReference θ Q x

Distributive reference is monotone in the predicate.

theorem Champollion2017.stratifiedReference_mono {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {d : α → β} {γ : β → β → Prop} {P Q : α → Prop} (h : ∀ (x : α), P x → Q x) (x : α) : StratifiedReference d γ P x → StratifiedReference d γ Q x

Stratified reference is monotone in the predicate, for any dimension and granularity.

theorem Champollion2017.stratifiedReference_of_refl_granularity {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {d : α → β} {γ : β → β → Prop} (hRefl : ∀ (b : β), γ b b) {P : α → Prop} {x : α} (hx : P x) : StratifiedReference d γ P x

Under a reflexive granularity every P-element has stratified reference, by the base case.

theorem Champollion2017.stratifiedReference_join {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (d : SupHom α β) {γ : β → β → Prop} (hMono : ∀ (a b₁ b₂ : β), γ a b₁ → b₁ ≤ b₂ → γ a b₂) {P : α → Prop} {x y : α} (hx : StratifiedReference (⇑d) γ P x) (hy : StratifiedReference (⇑d) γ P y) : StratifiedReference (⇑d) γ P (x ⊔ y)

Stratified reference is closed under join when the dimension preserves sums and the granularity is monotone in its outer argument.

Aspect Bridge (subinterval reference ↔ atelicity)

theorem Champollion2017.forAdverbial_requires_subintervalReference {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] {P : E → Prop} (h_for_ok : SubintervalReferenceUniv P) (e : E) : P e → SubintervalReference P e

A for-adverbial requires subinterval reference, so John ran for an hour is felicitous and John arrived for an hour is not.

theorem Champollion2017.qua_incompatible_with_subintervalReference {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] {P : E → Prop} (hQua : Mereology.QUA P) {e : E} (he : P e) (hSub : SubintervalReference P e) : False

Quantization and subinterval reference are incompatible, since an event with subinterval reference has a proper part in the predicate.

for-Adverbial Compatibility

def Champollion2017.forAdverbialMeaning {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] (V : E → Prop) (duration : NonemptyInterval T) (e : E) : Prop

V for δ holds of an event of V whose run time is δ and at which V has subinterval reference, [Cha17]'s entry for the for-adverbial, eq. (72).

Equations

• Champollion2017.forAdverbialMeaning V duration e = (V e ∧ Event.τ e = duration ∧ Champollion2017.SubintervalReference V e)

theorem Champollion2017.in_adverbial_incompatible_with_subintervalReference {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] {P : E → Prop} (hQua : Mereology.QUA P) {e₁ e₂ : E} (he₁ : P e₁) (_he₂ : P e₂) (_hne : e₁ ≠ e₂) : ¬SubintervalReferenceUniv P

An in-adverbial, which requires quantization, is incompatible with subinterval reference.

Verb distributivity

Whether a verb distributes over the atomic fillers of a thematic role is a property of its event denotation, not a feature it carries.

def Verb.StratifiesOver {Entity : Type u_1} {E : Type u_2} [PartialOrder Entity] [SemilatticeSup E] (v : Verb) (V : Verb → E → Prop) (R : Entity → E → Prop) : Prop

A verb stratifies over the atomic fillers of role R when the event predicate that the interpretation V assigns it has relational stratified distributive reference along R.

Equations

• v.StratifiesOver V R = Champollion2017.RelationalDistributiveReferenceUniv R (V v)

§2.7.2 algebraic substrate

def Champollion2017.LexicallyCumulative {α : Type u_1} [SemilatticeSup α] (P : α → Prop) : Prop

A predicate is lexically cumulative when it is a fixed point of the algebraic closure operator.

Equations

• Champollion2017.LexicallyCumulative P = ∀ (x : α), Mereology.AlgClosure P x ↔ P x

theorem Champollion2017.lexicallyCumulative_imp_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (h : LexicallyCumulative P) : Mereology.CUM P

Lexical cumulativity entails Krifka's CUM (closure under binary join).

Distributivity as meaning postulates

The book's per-verb distributivity facts are lexical meaning postulates in Hoeksema's sense, not theorems; they are stated here over the Fragment verbs' denotations.

structure Champollion2017.ChampollionPostulates {Entity : Type u_1} {E : Type u_2} [PartialOrder Entity] [SemilatticeSup E] (V : Verb → E → Prop) (agentRole themeRole : Entity → E → Prop) : Prop

ChampollionPostulates records the book's postulates on the distributivity of verbs, over an interpretation V of the fragment's verbs as event predicates and the agent and theme roles. See distributes on both roles and kill on its theme only, since a member of the posse need not have killed anyone, and meet does not distribute on its agent.

• see_distributes_agent : English.Verbs.see.StratifiesOver V agentRole
• see_distributes_theme : English.Verbs.see.StratifiesOver V themeRole
• kill_distributes_theme : English.Verbs.kill.StratifiesOver V themeRole
• kill_not_distributes_agent : ¬English.Verbs.kill.StratifiesOver V agentRole
• meet_not_distributes_agent : ¬English.Verbs.meet.StratifiesOver V agentRole

Atelicity as a Schwarzschild cover (§5.4)

theorem Champollion2017.subintervalReference_iff_cover {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [SemilatticeSup E] {P : E → Prop} {e : E} : SubintervalReference P e ↔ ∃ (parts : Finset E) (hne : parts.Nonempty), (∀ p ∈ parts, P p ∧ Event.τ p < Event.τ e) ∧ parts.sup' hne id = e

A predicate P has stratified subinterval reference at e iff e is the sum of a finite Schwarzschild cover into proper-subinterval P-parts, the book's theorem at the runtime dimension.

Aspect and space: the subregion and strata approaches (§6.3–6.4)

def Champollion2017.SubregionPresup {α : Type u_1} {T : Type u_2} [SemilatticeSup α] [PartialOrder T] (τ : α → T) (P : α → Prop) (e : α) : Prop

The subregion presupposition (28), which the chapter attributes to [Kri98]'s for-adverbial, holds when the event has a temporal part and every temporal part of it falls under the predicate.

Equations

• Champollion2017.SubregionPresup τ P e = ((∃ (e' : α), Krifka1998.IsTemporalPart τ e' e) ∧ ∀ (e' : α), Krifka1998.IsTemporalPart τ e' e → P e')

theorem Champollion2017.stratifiedReference_of_divisiveness {α : Type u_1} {T : Type u_2} [SemilatticeSup α] [PartialOrder T] {τ : α → T} {P : α → Prop} (hτ : Monotone τ) {a b : α} (hov : ¬Mereology.Overlap (τ a) (τ b)) (ha : ¬IsBot (τ a)) (hb : ¬IsBot (τ b)) (hdiv : ∀ (e' : α), Krifka1998.IsTemporalPart τ e' (a ⊔ b) → P e') : StratifiedReference τ (fun (x1 x2 : T) => x1 < x2) P (a ⊔ b)

On an event that splits into two parts with non-overlapping, non-null runtimes, the divisiveness clause of the subregion presupposition yields stratified reference along the runtime: the two parts are each other's temporal siblings, so both fall under the predicate, and each has a properly smaller runtime.

@[reducible, inline]

abbrev Champollion2017.Leg : Type

The back-and-forth scenario has four trips of two legs each, a leg at each instant, the even legs from the lot halfway to the store and the odd legs on to the store. An event is a set of legs and its runtime the set of their instants.

Equations

• Champollion2017.Leg = Fin 8

def Champollion2017.PushCartsToStore (e : Finset Leg) : Prop

push carts all the way to the store holds of a nonempty event whose path reaches the store, that is, one containing a leg on to the store.

Equations

• Champollion2017.PushCartsToStore e = (e.Nonempty ∧ ∃ k ∈ e, ↑k % 2 = 1)

@[instance_reducible]

instance Champollion2017.instDecidablePredFinsetLegPushCartsToStore : DecidablePred PushCartsToStore

Equations

• Champollion2017.instDecidablePredFinsetLegPushCartsToStore x✝ = id inferInstance

theorem Champollion2017.pushCarts_stratified : StratifiedReference id (fun (x1 x2 : Finset Leg) => x1 ⊂ x2) PushCartsToStore Finset.univ

The fifty-minute event divides along time into its four trips, each of which reaches the store within a proper part of the runtime: the strata-based account admits the for-adverbial (Figure 6.2a).

theorem Champollion2017.pushCarts_not_subregion : ¬SubregionPresup id PushCartsToStore Finset.univ

The halfway legs form a temporal part of the event that does not reach the store, the offending event of §6.4.1, so the subregion presupposition fails (Figure 6.2b).