[Zwa05] Prepositional Aspect and the Algebra of Paths

Directional-PP denotations are sets of paths; what distinguishes telic PPs (to the house) from atelic PPs (towards the house) is closure under the partial concatenation operation: atelic PPs are cumulative, telic PPs are not (21). The paper's Appendix A path algebra — Spatial.Path with Path.IsConcat (67) and the subpath order (68) — lives in Semantics/Events/Path.lean; this file formalizes the aspectual system built on it.

Main definitions

• Cumulative (17b, with the existence clause of fn. 7), Bounded (21) — stated over any ternary concatenation relation, since Appendix A pairs the path algebra with an event algebra of the same shape.
• weakTo (30c), toPP/fromPP (endpoint content of the strict (36)), towardsPP (45), awayFromPP (48), loops, Star (58).
• IsTraceHom, vpp (25) — §3.2 aspect transfer from PP to VP.

Main statements

• weakTo_cumulative vs toPP_bounded — the §4.1.1 argument: the weak goal-PP denotation is cumulative (wrong aspect), the strict one bounded.
• fromPP_bounded — source PPs are bounded like goal PPs: no aspectual source/goal asymmetry (12a), grounding the telic marking of source-directionality PPs (Spatial.Path.Directionality).
• towardsPP_concat_closed, awayFromPP_concat_closed, towardsPP_cumulative — the comparative definitions (45)/(48) are cumulative, grounding .unbounded ↦ .atelic.
• toPP_not_quantized — bounded PPs are not quantized (23)–(24): a to x path has proper to x subpaths, so Mereology.QUA fails.
• quantized_telicK, loops_telicK, loops_cumulative — quantization implies Krifka-telicity (22b), but the round-and-round loop set is (22b)-telic yet cumulative, so neither Krifka notion characterizes boundedness (§3.1).
• star_cumulative — the plural closure (58) is cumulative.
• vpp_concat_closed, vpp_bounded_of_no_pairs, toPP_no_pairs — §3.2: a trace homomorphism transfers PP closure to VP closure, and walk to the house is bounded because no two to the house traces concatenate.

TODO

• The full single-phase strict definitions (35)–(36), (39)–(40) and the minimality/grinder operators (63)–(64).
• Reconciling Spatial.Trace's IsSumHom law with this study's trace homomorphism: Zwarts (§3.2) follows Rothstein in using partial event concatenation, not the unrestricted mereological sum.

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

(17b): a set is cumulative iff some concatenation exists within it (fn. 7's non-vacuity clause) 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

(21): bounded = non-cumulative. This, not quantization, is what characterizes telic PPs.

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

(22b): Krifka-style telicity for path sets — 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 Krifka-telic (§3.1: "Being quantized implies being telic").

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

The round and round the block set: non-constant loops at a fixed location.

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 Krifka-telic: 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-telicity (22b) does not characterize boundedness (§3.1: round and round the block is telic in Krifka's sense but behaves unboundedly).

Goal and source prepositions (§4.1.1)

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

(30c): the weak goal-PP denotation — 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/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 PP (36): the path 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 PP (36): the path 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: the first ends at x, the second never starts there (§3.1).

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

Strict goal PPs are bounded (21): to the house is telic.

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

Strict source PPs are bounded, exactly like goal PPs — there is no aspectual source/goal asymmetry (12a). Grounds the telic marking of source-directionality PPs (Spatial.Path.Directionality).

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)

(45): towards x — the path 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)

(48): away from x — the path 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

(45) is closed under concatenation: 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

(48) is closed under concatenation, mirroring (45).

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

On the rational line with the reference object at the origin, towards is fully cumulative (45): closure plus a concrete concatenable pair.

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

Bounded PPs are not quantized (23)–(24): a to x path has proper subpaths that are also to x, so Mereology.QUA fails — against the [Kri98] characterization of telicity, and against this library's earlier docstring folklore.

Plural PPs: the star operator (§4.2.2)

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

(58): closure of a path set under concatenations — prepositional plurality (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}

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

Aspect transfer to the VP (§3.2)

def Zwarts2005.IsTraceHom {Loc : Type u_1} {E : Type u_3} (C : E → E → E → Prop) (tr : E → Spatial.Path Loc) : Prop

§3.2: the trace function is a homomorphism for concatenation — the trace of a fused event is the concatenation of the traces. Zwarts follows Rothstein's partial event concatenation, not the unrestricted mereological sum.

Equations

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

def Zwarts2005.vpp {Loc : Type u_1} {E : Type u_3} (tr : E → Spatial.Path Loc) (V : Set E) (X : Set (Spatial.Path Loc)) : Set E

(25): ⟦V PP⟧ — the verb's events whose trace lies in the PP denotation.

Equations

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

theorem Zwarts2005.vpp_concat_closed {Loc : Type u_1} {E : Type u_3} (C : E → E → E → Prop) (tr : E → Spatial.Path Loc) (hhom : IsTraceHom C tr) {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 tr V X → ∀ e' ∈ vpp tr V X, ∀ (f : E), C e e' f → f ∈ vpp tr V X

§3.2 transfer, positive half: closure of the verb and of the PP denotation transfers to the VP (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} (C : E → E → E → Prop) (tr : E → Spatial.Path Loc) (hhom : IsTraceHom C tr) {V : Set E} {X : Set (Spatial.Path Loc)} (hX : ¬∃ p ∈ X, ∃ q ∈ X, ∃ (r : Spatial.Path Loc), p.IsConcat q r) : Bounded C (vpp tr V X)

§3.2 transfer, negative half: if no two PP paths concatenate, no two VP events fuse — 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} (C : E → E → E → Prop) (tr : E → Spatial.Path Loc) (hhom : IsTraceHom C tr) {V : Set E} (x : Loc) : Bounded C (vpp tr V (toPP x))

Walk to the house is bounded (26), (§3.2): instantiates the negative transfer at the strict goal PP.