VP-Level Situation Type Composition

@cite{smith-1997}

Compositional rules for deriving the situation type of a verb constellation from its component parts (verb, NP, PP). @cite{smith-1997} Ch. 3 §3.3.

Structure

1. NP/PP feature types — count/mass, directional/locative
2. Basic-level composition — verb + arguments → verb constellation
3. External override — adverbial/viewpoint overrides clashing feature
4. Verification — composition matches hand-checked examples

Key Principle

The verb supplies intrinsic temporal features [±Telic, ±Durative, ±Dynamic]. NP and PP arguments contribute to the composite VP telicity:

• V[-Telic] + NP[+Count] → VCon[-Telic] (atelic verbs stay atelic)
• V[-Telic] + PP[+Dir] → VCon[+Telic] (directional PP telicizes)
• V[+Telic] + NP[+Count] → VCon[+Telic] (telic verbs stay telic)
• V[+Telic] + NP[-Count] → VCon[-Telic] (mass NP atelicizes)

The Principle of External Override (§3.2.5): when an adverbial's temporal feature clashes with the verb constellation's, the adverbial wins.

inductive Semantics.Aspect.Composition.PPType : Type

PP directionality feature. Directional PPs contribute telicity; locative PPs do not. @cite{smith-1997} §3.3.1 (50b).

• directional : PPType
• locative : PPType

@[implicit_reducible]

instance Semantics.Aspect.Composition.instDecidableEqPPType : DecidableEq PPType

Equations

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

@[implicit_reducible]

instance Semantics.Aspect.Composition.instReprPPType : Repr PPType

Equations

• Semantics.Aspect.Composition.instReprPPType = { reprPrec := Semantics.Aspect.Composition.instReprPPType.repr }

def Semantics.Aspect.Composition.instReprPPType.repr : PPType → ℕ → Std.Format

Equations

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

def Semantics.Aspect.Composition.npTelicityContribution (verbTelic : Features.Telicity) (np : MassCount) : Features.Telicity

Telicity contribution of an object NP. Count NPs preserve verb telicity; mass NPs atelicize. @cite{smith-1997} §3.3.1 (50a, 51):

• V[+Telic] + NP[+Count] → VCon[+Telic] ("builds a house")
• V[+Telic] + NP[-Count] → VCon[-Telic] ("builds houses")
• V[-Telic] + NP[+Count] → VCon[-Telic] ("walks the dog")
• V[-Telic] + NP[-Count] → VCon[-Telic] ("drinks water")

Equations

• Semantics.Aspect.Composition.npTelicityContribution Features.Telicity.telic MassCount.count = Features.Telicity.telic
• Semantics.Aspect.Composition.npTelicityContribution verbTelic np = Features.Telicity.atelic

def Semantics.Aspect.Composition.composeWithNP (verb : Features.AspectualProfile) (np : MassCount) : Features.AspectualProfile

Compose a verb's aspectual profile with its NP object. The object's mass/count feature interacts with verb telicity. Duration and dynamicity are inherited from the verb.

Equations

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

def Semantics.Aspect.Composition.composeWithPP (verb : Features.AspectualProfile) (pp : PPType) : Features.AspectualProfile

Compose a verb's aspectual profile with a directional PP. Directional PPs contribute [+Telic]; locative PPs don't change telicity. @cite{smith-1997} §3.3.1 (50b): "child walk to school" → V[-Telic] + PP[Direct'l] → VCon[+Telic].

Equations

• Semantics.Aspect.Composition.composeWithPP verb Semantics.Aspect.Composition.PPType.directional = { telicity := Features.Telicity.telic, duration := verb.duration, dynamicity := verb.dynamicity }
• Semantics.Aspect.Composition.composeWithPP verb Semantics.Aspect.Composition.PPType.locative = verb

def Semantics.Aspect.Composition.overrideTelicity (vcon : Features.AspectualProfile) (ext : Features.Telicity) : Features.AspectualProfile

Principle of External Override (@cite{smith-1997} §3.2.5, rule 53): VCon[a, b, fα] + Adv[fβ] → DVCon[a, b, fβ].

When an external form (adverbial, viewpoint) has a temporal feature that clashes with the verb constellation's, the external feature overrides.

This is formalized as: override a single feature of the VCon profile. The relevant features are telicity and duration; dynamicity is never overridden by adverbials.

Equations

• Semantics.Aspect.Composition.overrideTelicity vcon ext = { telicity := ext, duration := vcon.duration, dynamicity := vcon.dynamicity }

def Semantics.Aspect.Composition.overrideDuration (vcon : Features.AspectualProfile) (ext : Features.Duration) : Features.AspectualProfile

Override the duration feature (e.g., "for an hour" forces [+Dur]).

Equations

• Semantics.Aspect.Composition.overrideDuration vcon ext = { telicity := vcon.telicity, duration := ext, dynamicity := vcon.dynamicity }

Verify the compositional rules against Smith's examples from §3.3.1.

theorem Semantics.Aspect.Composition.walk_the_dog : (composeWithNP Features.activityProfile MassCount.count).toVendlerClass = Features.VendlerClass.activity

(50a) "child walks the dog": V[-Telic] + NP[+Count] → VCon[-Telic]. Activity verb with count NP stays atelic.

theorem Semantics.Aspect.Composition.walk_to_school : (composeWithPP Features.activityProfile PPType.directional).toVendlerClass = Features.VendlerClass.accomplishment

(50b) "child walks to school": V[-Telic] + PP[Dir] → VCon[+Telic]. Activity verb with directional PP becomes telic accomplishment.

theorem Semantics.Aspect.Composition.build_a_house : (composeWithNP Features.accomplishmentProfile MassCount.count).toVendlerClass = Features.VendlerClass.accomplishment

(51a) "child builds a house": V[+Telic] + NP[+Count] → VCon[+Telic]. Accomplishment verb with count NP stays telic.

theorem Semantics.Aspect.Composition.build_houses : (composeWithNP Features.accomplishmentProfile MassCount.mass).toVendlerClass = Features.VendlerClass.activity

(51b) "child builds houses": V[+Telic] + NP[-Count] → VCon[-Telic]. Accomplishment verb with mass/bare NP becomes atelic activity. This is Krifka's classic telicity transfer: QUA NP → telic VP, CUM NP → atelic VP.

theorem Semantics.Aspect.Composition.cough_for_an_hour : (overrideDuration Features.semelfactiveProfile Features.Duration.durative).toVendlerClass = Features.VendlerClass.activity

(52) "Mary coughed for an hour": VCon[+Dyn,-Telic,-Dur] + Adv[+Dur] → DVCon[+Dyn,-Telic,+Dur]. Semelfactive → Activity by duration override.

theorem Semantics.Aspect.Composition.telic_override_to_atelic : (overrideTelicity Features.accomplishmentProfile Features.Telicity.atelic).toVendlerClass = Features.VendlerClass.activity

External override: telic VCon + atelic adverbial → atelic DVCon. "walked to school for an hour" → activity reading.

theorem Semantics.Aspect.Composition.atelic_override_to_telic : (overrideTelicity Features.activityProfile Features.Telicity.telic).toVendlerClass = Features.VendlerClass.accomplishment

External override: atelic VCon + telic adverbial → telic DVCon. "sang in ten minutes" → accomplishment reading.

theorem Semantics.Aspect.Composition.count_np_preserves_telicity (v : Features.AspectualProfile) : (composeWithNP v MassCount.count).telicity = v.telicity

Count NPs preserve the verb's telicity value.

theorem Semantics.Aspect.Composition.mass_np_atelicizes (v : Features.AspectualProfile) : (composeWithNP v MassCount.mass).telicity = Features.Telicity.atelic

Mass NPs always yield atelic VPs, regardless of verb telicity.

theorem Semantics.Aspect.Composition.directional_pp_telicizes (v : Features.AspectualProfile) : (composeWithPP v PPType.directional).telicity = Features.Telicity.telic

Directional PPs always yield telic VPs.

theorem Semantics.Aspect.Composition.locative_pp_preserves (v : Features.AspectualProfile) : composeWithPP v PPType.locative = v

Locative PPs don't change telicity.

theorem Semantics.Aspect.Composition.compose_preserves_other_features (v : Features.AspectualProfile) (np : MassCount) : (composeWithNP v np).duration = v.duration ∧ (composeWithNP v np).dynamicity = v.dynamicity

Composition preserves duration and dynamicity (only telicity changes).

theorem Semantics.Aspect.Composition.override_telicity_idempotent (v : Features.AspectualProfile) (t : Features.Telicity) : overrideTelicity (overrideTelicity v t) t = overrideTelicity v t

Override is idempotent: overriding with the same feature twice is a no-op.

theorem Semantics.Aspect.Composition.override_absorbs_composition (v : Features.AspectualProfile) (np : MassCount) (ext : Features.Telicity) : overrideTelicity (composeWithNP v np) ext = overrideTelicity v ext

External override + composition commute when they target the same feature. Override after composition = override directly (composition is invisible).

@cite{smith-1997} §3.2.2, §3.2.5: semelfactives shift to activities under duration. This is the same shift captured by duratize_semelfactive in Features/Aktionsart.lean, but here derived compositionally via external override of the duration feature.

theorem Semantics.Aspect.Composition.semelfactive_durative_is_activity : (overrideDuration Features.semelfactiveProfile Features.Duration.durative).toVendlerClass = Features.VendlerClass.activity

Semelfactive + durative adverbial → activity (multiple-event reading). "Mary was coughing" / "Guy knocked at the door for 5 minutes". Derived from override: [-Dur] → [+Dur] yields Activity profile.

theorem Semantics.Aspect.Composition.override_agrees_with_shift : (overrideDuration Features.semelfactiveProfile Features.Duration.durative).toVendlerClass = Features.semelfactiveProfile.duratize.toVendlerClass

This matches the existing Features/Aktionsart shift operator.

theorem Semantics.Aspect.Composition.achievement_durative_is_accomplishment : (overrideDuration Features.achievementProfile Features.Duration.durative).toVendlerClass = Features.VendlerClass.accomplishment

Achievement + durative adverbial → accomplishment (process reading). "John was winning the race" presents preliminary stages. @cite{smith-1997} §3.2.4.