inductive Semantics.Events.EventStructure.Primitive : Type

Primitive event structure operators. ACT, CAUSE, BECOME, STATE are from @cite{rappaport-hovav-levin-1998}. MOVE and CONTACT are from @cite{rappaport-hovav-levin-2024}, decomposing manner verbs more finely than the original ACT-based templates.

• ACT : Primitive
• CAUSE : Primitive
• BECOME : Primitive
• STATE : Primitive
• MOVE : Primitive
• CONTACT : Primitive

instance Semantics.Events.EventStructure.instDecidableEqPrimitive : DecidableEq Primitive

Equations

• Semantics.Events.EventStructure.instDecidableEqPrimitive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Events.EventStructure.instReprPrimitive : Repr Primitive

Equations

• Semantics.Events.EventStructure.instReprPrimitive = { reprPrec := Semantics.Events.EventStructure.instReprPrimitive.repr }

def Semantics.Events.EventStructure.instReprPrimitive.repr : Primitive → ℕ → Std.Format

Equations

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

instance Semantics.Events.EventStructure.instBEqPrimitive : BEq Primitive

Equations

• Semantics.Events.EventStructure.instBEqPrimitive = { beq := Semantics.Events.EventStructure.instBEqPrimitive.beq }

def Semantics.Events.EventStructure.instBEqPrimitive.beq : Primitive → Primitive → Bool

Equations

• Semantics.Events.EventStructure.instBEqPrimitive.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Semantics.Events.EventStructure.Template : Type

Canonical event structure templates. The first four are from @cite{rappaport-hovav-levin-1998}. motionContact is from @cite{rappaport-hovav-levin-2024} for the sweep/rub/scrape class: [x MOVE y] WHILE [x CONTACT y].

• state : Template
• activity : Template
• achievement : Template
• accomplishment : Template
• motionContact : Template

instance Semantics.Events.EventStructure.instDecidableEqTemplate : DecidableEq Template

Equations

• Semantics.Events.EventStructure.instDecidableEqTemplate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Events.EventStructure.instReprTemplate.repr : Template → ℕ → Std.Format

Equations

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

instance Semantics.Events.EventStructure.instReprTemplate : Repr Template

Equations

• Semantics.Events.EventStructure.instReprTemplate = { reprPrec := Semantics.Events.EventStructure.instReprTemplate.repr }

def Semantics.Events.EventStructure.instBEqTemplate.beq : Template → Template → Bool

Equations

• Semantics.Events.EventStructure.instBEqTemplate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Events.EventStructure.instBEqTemplate : BEq Template

Equations

• Semantics.Events.EventStructure.instBEqTemplate = { beq := Semantics.Events.EventStructure.instBEqTemplate.beq }

def Semantics.Events.EventStructure.Template.hasCause : Template → Bool

Does the template involve CAUSE?

Equations

• Semantics.Events.EventStructure.Template.accomplishment.hasCause = true
• x✝.hasCause = false

def Semantics.Events.EventStructure.Template.hasExternalCauser : Template → Bool

Does the template have an external causer position?

Equations

• Semantics.Events.EventStructure.Template.accomplishment.hasExternalCauser = true
• x✝.hasExternalCauser = false

def Semantics.Events.EventStructure.Template.predicateCount : Template → ℕ

How many grammatically relevant predicates?

Equations

• Semantics.Events.EventStructure.Template.state.predicateCount = 1
• Semantics.Events.EventStructure.Template.activity.predicateCount = 1
• Semantics.Events.EventStructure.Template.achievement.predicateCount = 1
• Semantics.Events.EventStructure.Template.accomplishment.predicateCount = 2
• Semantics.Events.EventStructure.Template.motionContact.predicateCount = 2

def Semantics.Events.EventStructure.Template.toAspectualProfile : Template → Tense.Aspect.LexicalAspect.AspectualProfile

Predicted aspectual profile for each template.

Equations

• Semantics.Events.EventStructure.Template.state.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.stateProfile
• Semantics.Events.EventStructure.Template.activity.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.activityProfile
• Semantics.Events.EventStructure.Template.achievement.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.achievementProfile
• Semantics.Events.EventStructure.Template.accomplishment.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile
• Semantics.Events.EventStructure.Template.motionContact.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.activityProfile

def Semantics.Events.EventStructure.Template.vendlerClass (t : Template) : Tense.Aspect.LexicalAspect.VendlerClass

Predicted Vendler class for each template (derived from profile).

Equations

• t.vendlerClass = t.toAspectualProfile.toVendlerClass

def Semantics.Events.EventStructure.Template.subjectProfile : Template → ProtoRoles.EntailmentProfile

Predicted subject entailment profile for each template.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Events.EventStructure.Template.motionContact.subjectProfile = Semantics.Events.ProtoRoles.sweepBasicSubjectProfile

def Semantics.Events.EventStructure.Template.objectProfile : Template → Option ProtoRoles.EntailmentProfile

Predicted object entailment profile (if any).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Events.EventStructure.Template.state.objectProfile = none
• Semantics.Events.EventStructure.Template.activity.objectProfile = none
• Semantics.Events.EventStructure.Template.achievement.objectProfile = none

theorem Semantics.Events.EventStructure.accomplishment_subject_is_agent : Template.accomplishment.subjectProfile.pAgentScore = 5

Accomplishment subject is a full agent (5 P-Agent entailments).

theorem Semantics.Events.EventStructure.motionContact_variable_agentivity : Template.motionContact.subjectProfile = ProtoRoles.sweepBasicSubjectProfile

motionContact subject has the same profile as basic sweep (movement + IE, underspecified for agentivity).

inductive Semantics.Events.EventStructure.DeterminingPredicate : Type

For motionContact verbs, which sub-predicate determines argument realization (@cite{rappaport-hovav-levin-2024} §3.3–3.4).

• motion : DeterminingPredicate
• contact : DeterminingPredicate

instance Semantics.Events.EventStructure.instDecidableEqDeterminingPredicate : DecidableEq DeterminingPredicate

Equations

• Semantics.Events.EventStructure.instDecidableEqDeterminingPredicate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Events.EventStructure.instReprDeterminingPredicate : Repr DeterminingPredicate

Equations

• Semantics.Events.EventStructure.instReprDeterminingPredicate = { reprPrec := Semantics.Events.EventStructure.instReprDeterminingPredicate.repr }

def Semantics.Events.EventStructure.instReprDeterminingPredicate.repr : DeterminingPredicate → ℕ → Std.Format

Equations

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

instance Semantics.Events.EventStructure.instBEqDeterminingPredicate : BEq DeterminingPredicate

Equations

• Semantics.Events.EventStructure.instBEqDeterminingPredicate = { beq := Semantics.Events.EventStructure.instBEqDeterminingPredicate.beq }

def Semantics.Events.EventStructure.instBEqDeterminingPredicate.beq : DeterminingPredicate → DeterminingPredicate → Bool

Equations

• Semantics.Events.EventStructure.instBEqDeterminingPredicate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

theorem Semantics.Events.EventStructure.contact_determines_implies_effector_subject : ProtoRoles.isEffector Template.motionContact.subjectProfile = true

When CONTACT determines argument realization, the subject is an effector (movement + IE → external argument). This yields the simple transitive frame: "The wind swept the deck".

theorem Semantics.Events.EventStructure.motionContact_object_is_forceRecipient : ∃ (p : ProtoRoles.EntailmentProfile), Template.motionContact.objectProfile = some p ∧ ProtoRoles.isForceRecipient p = true

The motionContact object profile exists and is a force recipient.

def Semantics.Events.EventStructure.Template.lexicalizeInstrument : Template → ProtoRoles.EntailmentProfile

Instrument lexicalization adds agentivity to a template by restricting the moving entity to a specific instrument, forcing volition + sentience

• causation. The result is the broom-sweep subject profile.

Equations

• Semantics.Events.EventStructure.Template.motionContact.lexicalizeInstrument = Semantics.Events.ProtoRoles.sweepBroomSubjectProfile
• x✝.lexicalizeInstrument = x✝.subjectProfile

theorem Semantics.Events.EventStructure.lexicalize_increases_agentivity : Template.motionContact.lexicalizeInstrument.pAgentScore > Template.motionContact.subjectProfile.pAgentScore

Instrument lexicalization strictly increases agentivity for motionContact templates (@cite{rappaport-hovav-levin-2024} §3.5: broom-sweep is more agentive than basic sweep).

theorem Semantics.Events.EventStructure.lexicalized_is_full_agent : Template.motionContact.lexicalizeInstrument.pAgentScore = 5

Lexicalized motionContact has full proto-agent profile (5 entailments).

Levin classes map to event structure templates via meaning components. The core correspondence (@cite{rappaport-hovav-levin-1998} §3; @cite{rappaport-hovav-levin-2010} §2):

| Meaning component pattern | Template | Example class |
|---|---|---|
| CoS + causation | accomplishment | break (45.1), destroy (44) |
| CoS, no causation | achievement | appear (48.1), calve (28) |
| No CoS, no motion | state | exist (47.1), admire (31.2) |
| Otherwise | activity | hit (18.1), run (51.3) |

The `motionContact` template is specific to the sweep/rub/scrape
class and requires a class-specific override. 

def MeaningComponents.predictedTemplate : MeaningComponents → Semantics.Events.EventStructure.Template

Predicted event structure template from meaning components.

Equations

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

def LevinClass.eventTemplate : LevinClass → Semantics.Events.EventStructure.Template

Predicted template for a Levin class, with class-specific overrides.

Equations

• LevinClass.wipe.eventTemplate = Semantics.Events.EventStructure.Template.motionContact
• x✝.eventTemplate = x✝.meaningComponents.predictedTemplate

Verification: canonical quadruple

theorem Semantics.Events.EventStructure.break_is_accomplishment : LevinClass.break_.eventTemplate = Template.accomplishment

Break → accomplishment (CoS + causation → [ACT CAUSE BECOME]).

theorem Semantics.Events.EventStructure.hit_is_activity : LevinClass.hit.eventTemplate = Template.activity

Hit → activity (contact + motion, no CoS → [ACT]).

theorem Semantics.Events.EventStructure.touch_is_activity : LevinClass.touch.eventTemplate = Template.activity

Touch → activity (contact only, no CoS).

theorem Semantics.Events.EventStructure.cut_is_accomplishment : LevinClass.cut.eventTemplate = Template.accomplishment

Cut → accomplishment (CoS + causation).

Change-of-state classes → accomplishment

theorem Semantics.Events.EventStructure.cos_classes_accomplishment : LevinClass.break_.eventTemplate = Template.accomplishment ∧ LevinClass.bend.eventTemplate = Template.accomplishment ∧ LevinClass.cooking.eventTemplate = Template.accomplishment ∧ LevinClass.otherCoS.eventTemplate = Template.accomplishment ∧ LevinClass.destroy.eventTemplate = Template.accomplishment

All §45 CoS classes map to accomplishment.

Motion classes → activity

theorem Semantics.Events.EventStructure.motion_is_activity : LevinClass.mannerOfMotion.eventTemplate = Template.activity ∧ LevinClass.inherentlyDirectedMotion.eventTemplate = Template.activity

Motion verbs are activities (no CoS, have motion).

Stative classes → state

theorem Semantics.Events.EventStructure.stative_classes_state : LevinClass.exist.eventTemplate = Template.state ∧ LevinClass.admire.eventTemplate = Template.state ∧ LevinClass.want.eventTemplate = Template.state

Perception/psych statives map to state template.

Achievement classes

theorem Semantics.Events.EventStructure.appear_is_achievement : LevinClass.appear.eventTemplate = Template.achievement

Appear (CoS without causation) → achievement.

theorem Semantics.Events.EventStructure.calve_is_achievement : LevinClass.calve.eventTemplate = Template.achievement

Calve (CoS without causation) → achievement.

Special: motionContact

theorem Semantics.Events.EventStructure.wipe_is_motionContact : LevinClass.wipe.eventTemplate = Template.motionContact

Wipe class → motionContact (class-specific override).

Template → aspectual class consistency

theorem Semantics.Events.EventStructure.break_telic : LevinClass.break_.eventTemplate.vendlerClass = Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Accomplishment classes (break, cut) are predicted telic.

theorem Semantics.Events.EventStructure.hit_atelic : LevinClass.hit.eventTemplate.vendlerClass = Tense.Aspect.LexicalAspect.VendlerClass.activity

Activity classes (hit, run) are predicted atelic.

theorem Semantics.Events.EventStructure.exist_stative : LevinClass.exist.eventTemplate.vendlerClass = Tense.Aspect.LexicalAspect.VendlerClass.state

State classes (exist, admire) are predicted stative.