Zwarts (2005): Prepositional Aspect and the Algebra of Paths

Zwarts analyzes the aspect of directional prepositional phrases, which denote sets of paths. A telic phrase like to the house differs from an atelic one like towards the house in closure under the partial concatenation of paths: an atelic phrase is cumulative and a telic one bounded, that is, not cumulative. Bounded phrases are not quantized, and loops are telic in Krifka's sense yet cumulative, so neither quantization nor that telicity characterizes boundedness. A trace homomorphism for concatenation transfers closure from the phrase to the verb phrase, so walk to the house is bounded because no two to the house paths concatenate. The path algebra is Semantics/Events/Path; closure is stated here over any ternary concatenation relation.

Main definitions

• Cumulative: closure under concatenation.
• Bounded: the absence of cumulativity.
• toPP: the endpoint content of the strict goal phrase.
• towardsPP: towards.
• IsTraceHom: a trace homomorphism for concatenation.

Main results

• toPP_bounded: strict goal phrases are bounded.
• towardsPP_cumulative: towards is cumulative.
• toPP_not_quantized: bounded phrases are not quantized.
• loops_cumulative: loops are cumulative.
• vpp_toPP_bounded: walk to the house is bounded.

Implementation notes

• The strict goal and source denotations enter through their endpoint content only.
• The paper's trace function respects Rothstein's partial event concatenation, not an unrestricted mereological sum.

TODO

• The full single-phase definitions (35), (36), (39) and (40), and the minimality and grinder operators (63) and (64).

References

• [Zwa05]
• [Kri98]

Cumulativity and boundedness (17b), (21)

Stated over an arbitrary ternary concatenation relation: Appendix A pairs the path algebra with an event algebra of the same shape, and §3.2 transfers closure properties along a homomorphism between the two.

def Zwarts2005.Cumulative {α : Type u_2} (C : α → α → α → Prop) (X : Set α) : Prop

A set is cumulative, (17b), when some concatenation exists within it, the non-vacuity clause of fn. 7, and it is closed under concatenation.

Equations

• Zwarts2005.Cumulative C X = ((∃ p ∈ X, ∃ q ∈ X, ∃ (r : α), C p q r) ∧ ∀ p ∈ X, ∀ q ∈ X, ∀ (r : α), C p q r → r ∈ X)

def Zwarts2005.Bounded {α : Type u_2} (C : α → α → α → Prop) (X : Set α) : Prop

A set is bounded, (21), when it is not cumulative.

Equations

• Zwarts2005.Bounded C X = ¬Zwarts2005.Cumulative C X

theorem Zwarts2005.bounded_of_no_pairs {α : Type u_2} {C : α → α → α → Prop} {X : Set α} (h : ¬∃ p ∈ X, ∃ q ∈ X, ∃ (r : α), C p q r) : Bounded C X

A set with no concatenable pairs at all is bounded.

Quantization and Krifka-telicity are the wrong notions (§3.1)

(22) transplants [Kri98]'s quantization and telicity to path sets; Zwarts shows neither characterizes boundedness. Quantization is Mereology.QUA over the subpath order.

def Zwarts2005.TelicK {Loc : Type u_1} (X : Set (Spatial.Path Loc)) : Prop

A path set is telic in Krifka's sense, (22b), when comparable members share both endpoints.

Equations

• Zwarts2005.TelicK X = ∀ p ∈ X, ∀ q ∈ X, p ≤ q → p.source = q.source ∧ p.goal = q.goal

theorem Zwarts2005.quantized_telicK {Loc : Type u_1} {X : Set (Spatial.Path Loc)} (h : Mereology.QUA fun (x : Spatial.Path Loc) => x ∈ X) : TelicK X

Quantized sets are telic in Krifka's sense.

def Zwarts2005.loops {Loc : Type u_1} (A : Loc) : Set (Spatial.Path Loc)

loops x is the round and round the block set of non-constant loops at x.

Equations

• Zwarts2005.loops A = {p : Spatial.Path Loc | p.source = A ∧ p.goal = A ∧ p.steps ≠ []}

theorem Zwarts2005.loops_telicK {Loc : Type u_1} (A : Loc) : TelicK (loops A)

Loop sets are telic in Krifka's sense, since all members share both endpoints.

theorem Zwarts2005.loops_cumulative {Loc : Type u_1} (A : Loc) : Cumulative Spatial.Path.IsConcat (loops A)

Loop sets are cumulative, so Krifka's telicity (22b) does not characterize boundedness.

Goal and source prepositions (§4.1.1)

def Zwarts2005.weakTo {Loc : Type u_1} (x : Loc) : Set (Spatial.Path Loc)

The weak goal-phrase denotation, (30c), holds of the paths ending at the reference object.

Equations

• Zwarts2005.weakTo x = {p : Spatial.Path Loc | p.goal = x}

theorem Zwarts2005.weakTo_cumulative {Loc : Type u_1} (x : Loc) : Cumulative Spatial.Path.IsConcat (weakTo x)

The weak definition (30c) is cumulative, the wrong aspect for telic to and into, which is Zwarts's argument for the strict single-phase definitions (34)–(35).

def Zwarts2005.toPP {Loc : Type u_1} (x : Loc) : Set (Spatial.Path Loc)

The endpoint content of the strict goal phrase, (36), holds of a path that ends at the reference object and does not start there.

Equations

• Zwarts2005.toPP x = {p : Spatial.Path Loc | p.goal = x ∧ p.source ≠ x}

def Zwarts2005.fromPP {Loc : Type u_1} (x : Loc) : Set (Spatial.Path Loc)

The endpoint content of the strict source phrase, (36), holds of a path that starts at the reference object and does not end there.

Equations

• Zwarts2005.fromPP x = {p : Spatial.Path Loc | p.source = x ∧ p.goal ≠ x}

theorem Zwarts2005.toPP_no_pairs {Loc : Type u_1} (x : Loc) : ¬∃ p ∈ toPP x, ∃ q ∈ toPP x, ∃ (r : Spatial.Path Loc), p.IsConcat q r

No two to x paths concatenate, since the first ends at x and the second never starts there.

theorem Zwarts2005.toPP_bounded {Loc : Type u_1} (x : Loc) : Bounded Spatial.Path.IsConcat (toPP x)

Strict goal phrases are bounded, (21), so to the house is telic.

theorem Zwarts2005.fromPP_bounded {Loc : Type u_1} (x : Loc) : Bounded Spatial.Path.IsConcat (fromPP x)

Strict source phrases are bounded like goal phrases, so there is no aspectual asymmetry between source and goal, (12a).

Towards and away from (§4.1.3)

The comparative definitions over a distance measure d to the reference object: cumulative, hence unbounded — grounding the atelic marking of the comparative prepositions in the fragments' directionality × telicity data.

def Zwarts2005.towardsPP {Loc : Type u_1} {α : Type u_2} [Preorder α] (d : Loc → α) : Set (Spatial.Path Loc)

Towards x, (45), holds of a path that ends nearer to the reference object than it starts, measured by d.

Equations

• Zwarts2005.towardsPP d = {p : Spatial.Path Loc | d p.goal < d p.source}

def Zwarts2005.awayFromPP {Loc : Type u_1} {α : Type u_2} [Preorder α] (d : Loc → α) : Set (Spatial.Path Loc)

Away from x, (48), holds of a path that ends further from the reference object than it starts.

Equations

• Zwarts2005.awayFromPP d = {p : Spatial.Path Loc | d p.source < d p.goal}

theorem Zwarts2005.towardsPP_concat_closed {Loc : Type u_1} {α : Type u_2} [Preorder α] (d : Loc → α) (p : Spatial.Path Loc) : p ∈ towardsPP d → ∀ q ∈ towardsPP d, ∀ (r : Spatial.Path Loc), p.IsConcat q r → r ∈ towardsPP d

Towards is closed under concatenation, since distance decreases across each concatenant.

theorem Zwarts2005.awayFromPP_concat_closed {Loc : Type u_1} {α : Type u_2} [Preorder α] (d : Loc → α) (p : Spatial.Path Loc) : p ∈ awayFromPP d → ∀ q ∈ awayFromPP d, ∀ (r : Spatial.Path Loc), p.IsConcat q r → r ∈ awayFromPP d

Away from is closed under concatenation, mirroring towards.

theorem Zwarts2005.towardsPP_cumulative : Cumulative Spatial.Path.IsConcat (towardsPP abs)

On the rational line with the reference object at the origin, towards is cumulative, with a concrete concatenable pair witnessing non-vacuity.

theorem Zwarts2005.toPP_not_quantized : ¬Mereology.QUA fun (x : Spatial.Path ℚ) => x ∈ toPP 0

Bounded phrases are not quantized, (23)–(24), since a to x path has proper subpaths that are also to x, against the [Kri98] characterization of telicity.

Plural PPs: the star operator (§4.2.2)

inductive Zwarts2005.Star {Loc : Type u_1} (X : Set (Spatial.Path Loc)) : Spatial.Path Loc → Prop

The star closure of a path set, (58), closes it under concatenation, the prepositional plurality of round and round the house.

• base {Loc : Type u_1} {X : Set (Spatial.Path Loc)} {p : Spatial.Path Loc} (hp : p ∈ X) : Star X p
• concat {Loc : Type u_1} {X : Set (Spatial.Path Loc)} {p q r : Spatial.Path Loc} (hp : Star X p) (hq : Star X q) (h : p.IsConcat q r) : Star X r

theorem Zwarts2005.star_cumulative {Loc : Type u_1} {X : Set (Spatial.Path Loc)} (h : ∃ p ∈ X, ∃ q ∈ X, ∃ (r : Spatial.Path Loc), p.IsConcat q r) : Cumulative Spatial.Path.IsConcat {p : Spatial.Path Loc | Star X p}

The star closure is cumulative, given any concatenable pair to seed it, (58).

Aspect transfer to the VP (§3.2)

def Zwarts2005.IsTraceHom {Loc : Type u_1} {E : Type u_3} [Event.SpatialTrace E Loc] (C : E → E → E → Prop) : Prop

The spatial trace is a homomorphism for concatenation when the trace of a fused event is the concatenation of the traces.

Equations

• Zwarts2005.IsTraceHom C = ∀ (e e' f : E), C e e' f → (Event.σ e).IsConcat (Event.σ e') (Event.σ f)

def Zwarts2005.vpp {Loc : Type u_1} {E : Type u_3} [Event.SpatialTrace E Loc] (V : Set E) (X : Set (Spatial.Path Loc)) : Set E

⟦V PP⟧, (25), holds of the verb's events whose trace lies in the phrase's denotation.

Equations

• Zwarts2005.vpp V X = {e : E | e ∈ V ∧ Event.σ e ∈ X}

theorem Zwarts2005.vpp_concat_closed {Loc : Type u_1} {E : Type u_3} [Event.SpatialTrace E Loc] {C : E → E → E → Prop} (hhom : IsTraceHom C) {V : Set E} {X : Set (Spatial.Path Loc)} (hV : ∀ e ∈ V, ∀ e' ∈ V, ∀ (f : E), C e e' f → f ∈ V) (hX : ∀ p ∈ X, ∀ q ∈ X, ∀ (r : Spatial.Path Loc), p.IsConcat q r → r ∈ X) (e : E) : e ∈ vpp V X → ∀ e' ∈ vpp V X, ∀ (f : E), C e e' f → f ∈ vpp V X

Closure of the verb and of the phrase transfers to the verb phrase, so walk along the river is cumulative because walk and along the river are.

theorem Zwarts2005.vpp_bounded_of_no_pairs {Loc : Type u_1} {E : Type u_3} [Event.SpatialTrace E Loc] {C : E → E → E → Prop} (hhom : IsTraceHom C) {V : Set E} {X : Set (Spatial.Path Loc)} (hX : ¬∃ p ∈ X, ∃ q ∈ X, ∃ (r : Spatial.Path Loc), p.IsConcat q r) : Bounded C (vpp V X)

If no two paths of the phrase concatenate, no two events of the verb phrase fuse, so walk to the house is bounded because to the house has no concatenable pairs.

theorem Zwarts2005.vpp_toPP_bounded {Loc : Type u_1} {E : Type u_3} [Event.SpatialTrace E Loc] {C : E → E → E → Prop} (hhom : IsTraceHom C) {V : Set E} (x : Loc) : Bounded C (vpp V (toPP x))

Walk to the house is bounded, (26), by the negative transfer at the strict goal phrase.