Variable Agentivity: Polysemy or Underspecification?

[RHL24]

A formalization of Rappaport Hovav & Levin's 2024 Glossa paper on the English verb sweep and the wiping-verbs class. The paper argues that the variable agentivity of sweep — Matt swept the walk (agentive) vs the branch of the tree swept the window (non-agentive) — is the joint effect of two mechanisms, not one.

Main claims

1. basic-sweep is unspecified for agentivity. Its event structure ([RHL24] p.17, eq.42) is a complex activity with two grammatically relevant predicates: motion and force-transmission through contact. Either predicate can determine argument realization per-frame, yielding the simple transitive, transitive+PP, and unaccusative+PP frames attested in COCA.

2. broom-sweep is obligatorily agentive. It is derived from basic-sweep by lexicalization of the moving entity as a broom ([Kip97] on canonical-use of denominal verbs). The broom's instrument status forces an agent who manipulates it; the broom's design purpose underlies the routine-activity narrowing that licenses the unspecified-object frame ([Gla22], [Bri94], [Mit05]). The two senses constitute motivated polysemy (distinct from regular polysemy à la Apresjan; zeugma test eq.35).

3. The motion-and-sustained-contact event structure generalizes to the wiping-verbs class ([Lev93] 10.4): sweep, rub, scrape, wipe. Force-dynamic primitives follow [Tal88], [Cro12], [CH15], [GZ16].

4. Counterexample to the resultative restriction. [Sch12a]'s and [FH08]'s claim that non-agentive external arguments require a result phrase fails for basic-sweep (eq.92: A breeze moved the willows, the tips of their branches sweeping the ground).

Main declarations

• MotionContactES: the two-predicate complex-activity event structure for the wiping-verbs class. basicSweep and broomSweep are instances.
• ForceRole and Effector: force-dynamic primitives following [Tal88], [Cro12], [CH15].
• DeterminingPredicate (motion / contact): per-frame parameter to the argument-realization principles.
• Frame: the five syntactic frames attested for basic-sweep and broom-sweep (p.5, §2.2).
• realizeFrame: applies argument-realization principles (43)-(45) to produce the predicted frame from an event structure and a determining predicate.
• WipingVerb: the [Lev93] class 10.4 (sweep / rub / scrape / wipe) sharing the basic-sweep event structure.

Implementation notes

This file does not add a fifth case to Semantics.Lexical.EventStructure.Template. RHL 2024's contribution is an enrichment of the internal structure of the activity template for one manner subclass — two grammatically relevant predicates instead of one — and a per-frame choice of which predicate determines argument realization. The current Template.motionContact case in Features/EventStructure.lean is a misformalization of the 2024 paper and is queued for removal.

Footnote 31 of the paper explicitly disclaims the asymmetric "x moves... while x imparts..." formulation: the subordination is prose-only. Footnote 32 generalizes the mechanism beyond sweep to locative alternation ([RHL98] 1c–d), substance-emission verbs ([LK19]), and drown.

Todo

• Bridge broomSweep to the instrument-subclass template Features.LevinClassProfiles.wipeInstrument (Levin 10.4.2), whose subject profile is the fragment's sweep_instr entry value.
• Formalize the lexicon-uniformity blocker for some causative-alternation pairs ([RH14] on direct-causation requirement).
• Engage [Ram08]'s first-phase syntax and [Bor05] as syntactic rivals to the lexical-projection account this paper inherits from [RHL98].

Force-dynamic primitives

inductive RappaportHovavLevin2024.ForceRole : Type

Role in a force-transmission sub-event ([Tal88], [Cro12], [GZ16]).

In basic-sweep's event structure (p.17, eq.42), x is the force-bearer (it imparts the force) and y is the force-recipient (the surface receiving the force throughout the contact).

• bearer : ForceRole

  Force-bearer: imparts force via motion-induced contact (x in eq.42).

• recipient : ForceRole

  Force-recipient: receives force throughout the contact (y; the surface).

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableEqForceRole : DecidableEq ForceRole

Equations

• RappaportHovavLevin2024.instDecidableEqForceRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RappaportHovavLevin2024.instReprForceRole.repr : ForceRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprForceRole : Repr ForceRole

Equations

• RappaportHovavLevin2024.instReprForceRole = { reprPrec := RappaportHovavLevin2024.instReprForceRole.repr }

inductive RappaportHovavLevin2024.Effector : Type

The ontological types of entity that can occupy the basic-sweep subject position. The paper restricts the moving entity to entities capable of motion across a surface (p.5).

naturalPhenomenon and projectile together qualify as effectors in the strict sense (p.25): self-energetic. Agents are effectors via intentional control. Instruments and body parts qualify as force-bearers only under agent control (footnote 9, p.7).

• agent : Effector

  Volitional, intentional human or animal participant ([Cru73], [VVW96], p.7).

• naturalPhenomenon : Effector

  Wind, fire, water, storms — inherently self-energetic (p.25).

• projectile : Effector

  Physical objects with kinetic energy imparted by an unmentioned causer; can transmit that energy through contact ([Kea00] on projectiles; p.23).

• machine : Effector

  Self-propelled artifact (footnote 9, p.7); patterns with agents grammatically but not in the strict animate-intentional sense.

• instrument : Effector

  Instrument or body part. Cannot be a force-bearer without an agent providing the energy (p.21, p.25).

• displacedEntity : Effector

  Displaced entity moved along the surface (basic-sweep with transitive+PP frame; p.21).

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableEqEffector : DecidableEq Effector

Equations

• RappaportHovavLevin2024.instDecidableEqEffector x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprEffector : Repr Effector

Equations

• RappaportHovavLevin2024.instReprEffector = { reprPrec := RappaportHovavLevin2024.instReprEffector.repr }

def RappaportHovavLevin2024.instReprEffector.repr : Effector → ℕ → Std.Format

Equations

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

def RappaportHovavLevin2024.Effector.IsSelfEnergetic : Effector → Prop

Self-energetic force-bearers that qualify as effectors in the strict sense (p.25). These are the kinds of subjects basic-sweep allows in the non-agentive simple transitive frame.

Equations

• RappaportHovavLevin2024.Effector.agent.IsSelfEnergetic = True
• RappaportHovavLevin2024.Effector.naturalPhenomenon.IsSelfEnergetic = True
• RappaportHovavLevin2024.Effector.projectile.IsSelfEnergetic = True
• RappaportHovavLevin2024.Effector.machine.IsSelfEnergetic = True
• RappaportHovavLevin2024.Effector.instrument.IsSelfEnergetic = False
• RappaportHovavLevin2024.Effector.displacedEntity.IsSelfEnergetic = False

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableIsSelfEnergetic (e : Effector) : Decidable e.IsSelfEnergetic

Equations

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

@[reducible, inline]

abbrev RappaportHovavLevin2024.Effector.QualifiesAsSimpleTransitiveSubject : Effector → Prop

An effector qualifies as a basic-sweep simple-transitive subject under the contact-determines-AR derivation (p.24-25) iff it is self-energetic.

Equations

• RappaportHovavLevin2024.Effector.QualifiesAsSimpleTransitiveSubject = RappaportHovavLevin2024.Effector.IsSelfEnergetic

def RappaportHovavLevin2024.Effector.CanManipulateInstrument : Effector → Prop

An effector can intentionally manipulate an instrument ([RHL24] p.7, footnote 9). Only agents and self-propelled machines pattern this way; machines pattern with agents grammatically but are not animate-intentional. Natural phenomena and projectiles, despite being self-energetic, do not manipulate instruments.

Equations

• RappaportHovavLevin2024.Effector.agent.CanManipulateInstrument = True
• RappaportHovavLevin2024.Effector.machine.CanManipulateInstrument = True
• x✝.CanManipulateInstrument = False

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableCanManipulateInstrument (e : Effector) : Decidable e.CanManipulateInstrument

Equations

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

The basic-sweep event structure (eq. 42)

The grammatically relevant meaning components of sweep and other verbs in the wiping-verbs class. Encoded as a structure type so that broom-sweep (with the moving entity lexicalized) is derived by field-level minimal adjustment per [RHL24] §3.5 (eq.76).

structure RappaportHovavLevin2024.MotionContactES : Type

The motion-and-sustained-contact event structure ([RHL24] p.17, eq.42):

x moves across a surface y while x imparts a force to y through contact

Two grammatically relevant predicates: a motion predicate and a force-transmission predicate, sharing the moving entity x. Footnote 31 disclaims the "while" subordination — there is no theoretical significance to which predicate is "main"; the two are equipotent in determining argument realization.

The movingEntityLexicalization field carries broom-sweep's lexical saturation (eq.76: x_broom); none is basic-sweep.

• movingEntityLexicalization : Option String

  Lexicalization status of the moving entity x. none = unsaturated (basic-sweep); some "broom" = basic-sweep's moving-entity variable saturated by broom (broom-sweep). Other instrument-lexicalizations in English ([HH07]): comb, funnel, hoe, mop, plow, rake, saw, shovel, staple, towel, whip (paper eq.77).

def RappaportHovavLevin2024.instDecidableEqMotionContactES.decEq (x✝ x✝¹ : MotionContactES) : Decidable (x✝ = x✝¹)

Equations

• RappaportHovavLevin2024.instDecidableEqMotionContactES.decEq { movingEntityLexicalization := a } { movingEntityLexicalization := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableEqMotionContactES : DecidableEq MotionContactES

Equations

• RappaportHovavLevin2024.instDecidableEqMotionContactES = RappaportHovavLevin2024.instDecidableEqMotionContactES.decEq

def RappaportHovavLevin2024.instReprMotionContactES.repr : MotionContactES → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprMotionContactES : Repr MotionContactES

Equations

• RappaportHovavLevin2024.instReprMotionContactES = { reprPrec := RappaportHovavLevin2024.instReprMotionContactES.repr }

def RappaportHovavLevin2024.basicSweep : MotionContactES

basic-sweep: the underspecified base sense. Moving entity x is unsaturated; subject can be agent, natural phenomenon, projectile, or displaced entity depending on the frame and which predicate determines argument realization.

Equations

• RappaportHovavLevin2024.basicSweep = { }

def RappaportHovavLevin2024.broomSweep : MotionContactES

broom-sweep: the specialized agentive sense (eq.76). Moving entity x is lexically saturated as a broom; the broom's instrument status forces an agent.

Equations

• RappaportHovavLevin2024.broomSweep = { movingEntityLexicalization := some "broom" }

def RappaportHovavLevin2024.MotionContactES.IsLexicallySaturated (es : MotionContactES) : Prop

An event structure is lexically saturated iff its moving entity variable is fixed.

Equations

• es.IsLexicallySaturated = match es.movingEntityLexicalization with | none => False | some val => True

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableIsLexicallySaturated (es : MotionContactES) : Decidable es.IsLexicallySaturated

Equations

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

@[simp]

theorem RappaportHovavLevin2024.broomSweep_saturated : broomSweep.IsLexicallySaturated

@[simp]

theorem RappaportHovavLevin2024.basicSweep_not_saturated : ¬basicSweep.IsLexicallySaturated

Argument-realization principles ((43)-(45))

inductive RappaportHovavLevin2024.DeterminingPredicate : Type

Per-frame choice of which predicate in the event structure [RHL24] (eq.42) determines argument realization.

"When an event structure includes two grammatically relevant predicates, the argument realization principles are applied with respect to only one" (p.18, after eq.47).

The choice is per-frame, not per-verb: basic-sweep admits both motion-determines and contact-determines derivations of distinct frames from the same lexical entry.

• motion : DeterminingPredicate

  Motion determines: principle (43) applies, yielding a small-clause realization where the moving entity is the small-clause subject and a path PP is the predicate. Yields unaccusative+PP and transitive+PP frames.

• contact : DeterminingPredicate

  Contact determines: principles (44)-(45) apply, force-recipient → internal argument, effector → external argument. Yields simple transitive and unspecified-object frames.

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableEqDeterminingPredicate : DecidableEq DeterminingPredicate

Equations

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

def RappaportHovavLevin2024.instReprDeterminingPredicate.repr : DeterminingPredicate → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprDeterminingPredicate : Repr DeterminingPredicate

Equations

• RappaportHovavLevin2024.instReprDeterminingPredicate = { reprPrec := RappaportHovavLevin2024.instReprDeterminingPredicate.repr }

Syntactic frames

inductive RappaportHovavLevin2024.Frame : Type

The five syntactic frames attested for the wiping-verbs class ([RHL24] §2, p.5-13).

• simpleTransitive : Frame

  the branch of the tree swept the window: contact determines AR from basic-sweep. Subject is force-bearer/effector; surface is direct object.

• transitivePP : Frame

  the wind swept the fires through the top growth: motion determines AR; CAUSE applied on top (eq.50, causativized counterpart of eq.47). Subject is causer; moving entity is direct object; path is PP.

• unaccusativePP : Frame

  the fires swept through the top growth: motion determines AR without external causer (eq.46, eq.47); unaccusative+PP frame from basic-sweep's underlying event structure.

• unspecifiedObject : Frame

  Yesterday I swept in the morning: contact determines AR from broom-sweep; surface omitted under routine-activity narrowing ([Gla22], [Bri94], [Mit05]).

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableEqFrame : DecidableEq Frame

Equations

• RappaportHovavLevin2024.instDecidableEqFrame x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprFrame : Repr Frame

Equations

• RappaportHovavLevin2024.instReprFrame = { reprPrec := RappaportHovavLevin2024.instReprFrame.repr }

def RappaportHovavLevin2024.instReprFrame.repr : Frame → ℕ → Std.Format

Equations

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

def RappaportHovavLevin2024.realizeFrame (es : MotionContactES) (dp : DeterminingPredicate) (hasCauser : Bool) : Option Frame

Argument-realization principles (eqs. 43-45) applied to an event structure with a given determining-predicate choice. Outputs the predicted frame, or none when the derivation is blocked.

• (43a) An entity in motion along a path is the subject of a small clause. Requires the moving entity variable to be available for syntactic expression — fails if x is lexically saturated (p.30, after eq.86).
• (43b) A path is the predicate of a small clause.
• (44) A force recipient is an internal argument.
• (45) An effector is an external argument.

The hasCauser parameter encodes whether an external z is added (eq.50: z causes x to move across y while x imparts a force to y); without it, the motion-determined frame is unaccusative+PP.

Equations

• One or more equations did not get rendered due to their size.
• RappaportHovavLevin2024.realizeFrame es RappaportHovavLevin2024.DeterminingPredicate.contact hasCauser = some RappaportHovavLevin2024.Frame.simpleTransitive

Variable agentivity in basic-sweep

theorem RappaportHovavLevin2024.basicSweep_simple_transitive_admits_natural_force (e : Effector) (h : e = Effector.naturalPhenomenon ∨ e = Effector.projectile) : e.QualifiesAsSimpleTransitiveSubject

basic-sweep's simple transitive frame admits non-agentive subjects provided the subject is a self-energetic effector (p.25). This is the variable agentivity of basic-sweep.

theorem RappaportHovavLevin2024.basicSweep_simple_transitive_admits_agent : Effector.agent.QualifiesAsSimpleTransitiveSubject

basic-sweep admits an agentive subject in the simple transitive frame, but only with a with phrase specifying body part or instrument to provide a force-bearer (p.25 on The harpist swept the strings of her instrument ??(with a bow)). The agent qualifies as effector by (45); the body part / instrument is the force-bearer.

This is captured at the type level: an agent Effector qualifies as a simple-transitive subject because it's self-energetic via intentional control. The with-phrase requirement is a separate condition on the syntactic frame, not on the effector classification.

[RvPM22]: body parts as instrument-like extensions of the subject.

theorem RappaportHovavLevin2024.basicSweep_rejects_bare_instrument : ¬Effector.instrument.QualifiesAsSimpleTransitiveSubject

An instrument or body part by itself cannot be a basic-sweep simple transitive subject (p.21: body part and instrument options are not found without an agent). They are not self-energetic.

Obligatory agentivity in broom-sweep

theorem RappaportHovavLevin2024.broomSweep_obligatorily_agentive (e : Effector) (h : e.CanManipulateInstrument) : e = Effector.agent ∨ e = Effector.machine

broom-sweep's lexically saturated moving entity is a broom — an artifact-noun-derived instrument ([Kip97] on canonical-use). Brooms require intentional manipulation (paper footnote 9, p.7); therefore the external argument of broom-sweep must be capable of intentional instrument manipulation: agent or machine.

This is the obligatory agentivity of broom-sweep.

The proof factors through Effector.canManipulateInstrument: only agent and machine qualify, matching the disjunction in the conclusion.

broom-sweep lacks the causative alternation

theorem RappaportHovavLevin2024.broomSweep_no_motion_determined_frame (hc : Bool) : realizeFrame broomSweep DeterminingPredicate.motion hc = none

broom-sweep is obligatorily agentive (above), and lacks the causative alternation: Danny swept the floor / *The floor swept (p.12, eq.31).

At the level of the event-structure-to-frame mapping: motion-determines AR is unavailable for broom-sweep because x_broom is lexically saturated and cannot serve as the small-clause subject required by principle (43a) (p.30, after eq.86). The realizeFrame function encodes this: motion-determines on a saturated event structure returns none.

theorem RappaportHovavLevin2024.broomSweep_contact_yields_simple_transitive (hc : Bool) : realizeFrame broomSweep DeterminingPredicate.contact hc = some Frame.simpleTransitive

Conversely, broom-sweep can still derive a frame via the contact predicate: the simple transitive frame I swept the floor. The unspecified-object frame Yesterday I swept in the morning is a distinct realization licensed by routine-activity narrowing (separate from realizeFrame which folds it into simpleTransitive; see LicensesUnspecifiedObject below).

Counterexample to the resultative restriction

theorem RappaportHovavLevin2024.resultative_restriction_falsified : realizeFrame basicSweep DeterminingPredicate.contact false = some Frame.simpleTransitive ∧ Effector.naturalPhenomenon.IsSelfEnergetic ∧ ¬basicSweep.IsLexicallySaturated

[Sch12a]'s resultative restriction: non-agentive external arguments require a result phrase in the VP (or imply one). [FH08] refined this to external arguments lacking teleological capability.

basic-sweep with the contact-determines derivation falsifies both: A breeze moved the willows, the tips of their branches sweeping the ground (eq.92) — inanimate, non-teleological external argument, no explicit or implied result.

This is the paper's central empirical departure from the literature on external-argument licensing.

Routine-activity narrowing

def RappaportHovavLevin2024.LicensesUnspecifiedObject (es : MotionContactES) : Prop

broom-sweep's unspecified-object frame is licensed by routine-activity narrowing ([Gla22], [Bri94], [Mit05]): denominal-like verbs derived via lexicalization of artifacts come to refer to culturally-recognized routine activities for which the canonical-purpose object can be omitted.

Parallel cases (p.28-29):

• mop (denominal from mop, the canonical activity is floor-mopping)
• bake (non-denominal but specialized to baked-goods preparation in the unspecified-object frame: I baked this morning ≠ baking potatoes)
• clean ([LRH14])
• wash (Alexiadou et al. 2017 from the references)

basic-sweep does NOT license the unspecified-object frame (p.13: in the basic-sweep sense the verb is never found with unspecified objects in any syntactic frame).

Equations

• RappaportHovavLevin2024.LicensesUnspecifiedObject es = es.IsLexicallySaturated

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableLicensesUnspecifiedObject (es : MotionContactES) : Decidable (LicensesUnspecifiedObject es)

Equations

• RappaportHovavLevin2024.instDecidableLicensesUnspecifiedObject es = RappaportHovavLevin2024.instDecidableLicensesUnspecifiedObject._aux_1 es

@[simp]

theorem RappaportHovavLevin2024.broomSweep_licenses_unspecified : LicensesUnspecifiedObject broomSweep

@[simp]

theorem RappaportHovavLevin2024.basicSweep_no_unspecified : ¬LicensesUnspecifiedObject basicSweep

Motivated polysemy

The paper distinguishes its analysis of sweep's two senses from "regular polysemy" ([Apr73], Pustejovsky 1995, 1998, [Nun95], [Cru95], [Dol14]) by two diagnostics:

1. Zeugma test (Zwicky & Sadock 1975, Cruse 1986, Asher 2011 §3-4; p.13 eq.35): co-predication of the two senses is odd. #The sailor swept the deck and so did the rain. Regular polysemy (e.g., book = text/object) allows co-predication; broom-sweep/basic-sweep do not.

2. Idiosyncratic lexicalization: broom-sweep lexicalizes broom as the moving entity, but this is an idiosyncratic fact about English — there is no general process making instrument-lexicalized senses of all motion-contact verbs (p.28: English exceptionally lacks denominal broom, with sweep blocking it).

structure RappaportHovavLevin2024.MotivatedPolysemy : Type

Motivated polysemy: two related senses sharing a root and overlapping event structure, but not co-predicable (failing the zeugma test).

• basicSense : MotionContactES

  The basic sense, structurally simpler.

• specializedSense : MotionContactES

  The specialized sense, derived from basic by lexicalization.

• specializedIsSaturationOfBasic : ¬self.basicSense.IsLexicallySaturated ∧ self.specializedSense.IsLexicallySaturated

  The specialized sense is derived from the basic sense by saturating the moving-entity variable.

def RappaportHovavLevin2024.instReprMotivatedPolysemy.repr : MotivatedPolysemy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprMotivatedPolysemy : Repr MotivatedPolysemy

Equations

• RappaportHovavLevin2024.instReprMotivatedPolysemy = { reprPrec := RappaportHovavLevin2024.instReprMotivatedPolysemy.repr }

def RappaportHovavLevin2024.sweepPolysemy : MotivatedPolysemy

sweep's two senses constitute motivated polysemy.

Equations

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

Wiping-verbs class generalization

inductive RappaportHovavLevin2024.WipingVerb : Type

The motion-and-sustained-contact event structure generalizes to the [Lev93] class 10.4 (wiping verbs): sweep, rub, scrape, wipe. The paper establishes generalization in §2.3-2.4 (p.13-14): rub and scrape show the same constellation of syntactic frames as basic-sweep, supporting the contention that basic-sweep's event structure is shared by the class. wipe itself is not explicitly worked through but is assumed to pattern with the class ([LRH91]).

These verbs differ in lexicalized manner (the type of motion-with-contact):

• sweep: extended movement across a planar surface, contact during trajectory ([McNS22]).
• rub: contact with pressure, back-and-forth or circular movement.
• scrape: similar to sweep but with a harder contact and removal affordance.
• wipe: similar to sweep, often with a cloth-like instrument.

• sweep : WipingVerb
• rub : WipingVerb
• scrape : WipingVerb
• wipe : WipingVerb

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableEqWipingVerb : DecidableEq WipingVerb

Equations

• RappaportHovavLevin2024.instDecidableEqWipingVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RappaportHovavLevin2024.instReprWipingVerb : Repr WipingVerb

Equations

• RappaportHovavLevin2024.instReprWipingVerb = { reprPrec := RappaportHovavLevin2024.instReprWipingVerb.repr }

def RappaportHovavLevin2024.instReprWipingVerb.repr : WipingVerb → ℕ → Std.Format

Equations

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

def RappaportHovavLevin2024.WipingVerb.basicEventStructure : WipingVerb → MotionContactES

Every wiping verb has basic-sweep's event structure as its basic sense (§2.3-2.4).

Equations

• x✝.basicEventStructure = RappaportHovavLevin2024.basicSweep

def RappaportHovavLevin2024.WipingVerb.HasSpecializedSense : WipingVerb → Prop

Only sweep has an attested broom-sense in English (p.13-14, p.28). rub and scrape lack a specialized agentive sub-sense.

Equations

• RappaportHovavLevin2024.WipingVerb.sweep.HasSpecializedSense = True
• x✝.HasSpecializedSense = False

@[implicit_reducible]

instance RappaportHovavLevin2024.instDecidableHasSpecializedSense (v : WipingVerb) : Decidable v.HasSpecializedSense

Equations

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

Bridge to existing substrate

The wiping-verbs class corresponds to [Lev93] class 10.4, encoded as LevinClass.wipe in Linglib/Semantics/Lexical/LevinClass.lean. Verbs in this class share the basic-sweep event structure.

def RappaportHovavLevin2024.wipingLevinClass : Semantics.Lexical.LevinClass

[Lev93] 10.4 — the wiping-verbs Levin class.

Equations

• RappaportHovavLevin2024.wipingLevinClass = Semantics.Lexical.LevinClass.wipe

def RappaportHovavLevin2024.WipingVerb.levinClass : WipingVerb → Semantics.Lexical.LevinClass

All WipingVerb instances belong to LevinClass.wipe.

Equations

• x✝.levinClass = RappaportHovavLevin2024.wipingLevinClass

@[simp]

theorem RappaportHovavLevin2024.WipingVerb.all_in_wipe (v : WipingVerb) : v.levinClass = Semantics.Lexical.LevinClass.wipe