Documentation

Linglib.Theories.Morphology.ReversalRestitution

Verb-Root-Outcomes: Reversal and Restitution #

@cite{bhadra-2024}

Bhadra, D. (2024). Verb roots encode outcomes: argument structure and lexical semantics of reversal and restitution. Linguistics and Philosophy 47: 557–610.

Core contribution #

Every verb root is lexically equipped with a set of outcomes — the possible states of the direct object after the verb's force is applied. The cardinality of this set determines compatibility with the reversative prefix un- and the restitutive prefix re-:

PFC (potential-for-change): multi-membered outcome sets (fold, wrap, coil) → compatible with both un- and re-
IE (impingement-effecting): singleton outcomes, surface only (hit, scrub) → incompatible with both
COS (change-of-state): singleton outcomes, integral change (break, destroy) → incompatible with un-, partially compatible with re-

Boundary state operators #

res(e)(x) and pre(e)(x) yield the state of object x at the right and left boundaries of event e. These are NOT temporal operators — they yield property bundles (lifespan points). Reversative un- requires inverse equivalence of boundary states across events; restitutive re- requires result-state equivalence.

Bridges #

ForceTransmissionClass refines AffectednessDegree.potential into PFC vs IE
LevinClass.forceTransmissionClass bridges @cite{levin-1993} classes to @cite{bhadra-2024}
RootType.result roots have singleton outcomes; RootType.propertyConcept is orthogonal
Template.hasResultState is necessary but not sufficient for un-/re- (must also check outcome cardinality)

inductive OutcomeCardinality :

Cardinality of a verb root's outcome set — the possible states of the object after force transmission.

multi-membered sets (PFC) > singleton sets (IE, COS) > empty sets

Instances For

instance instDecidableEqOutcomeCardinality :

DecidableEq OutcomeCardinality

Equations

instDecidableEqOutcomeCardinality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqOutcomeCardinality :

BEq OutcomeCardinality

Equations

instBEqOutcomeCardinality = { beq := instBEqOutcomeCardinality.beq }

def instBEqOutcomeCardinality.beq :

OutcomeCardinality → OutcomeCardinality → Bool

Equations

instBEqOutcomeCardinality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def instReprOutcomeCardinality.repr :

OutcomeCardinality → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
instReprOutcomeCardinality.repr OutcomeCardinality.multi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OutcomeCardinality.multi")).group prec✝
instReprOutcomeCardinality.repr OutcomeCardinality.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OutcomeCardinality.empty")).group prec✝

Instances For

instance instReprOutcomeCardinality :

Repr OutcomeCardinality

Equations

instReprOutcomeCardinality = { reprPrec := instReprOutcomeCardinality.repr }

inductive ForceTransmissionClass :

Classification of force-transmitting verbs by impact type.

Table 1: the three classes are distinguished by whether force transmission occurs, whether integral change is entailed, and whether surface impingement is effected.

Class	Force	Integral change	Impingement
PFC	✓	not entailed	✗
IE	✓	not entailed	✓
COS	✓	entailed	✓/✗

This refines AffectednessDegree.potential (which lumps PFC and IE).

potentialForChange : ForceTransmissionClass
impingementEffecting : ForceTransmissionClass
integralChange : ForceTransmissionClass
noForceTransmission : ForceTransmissionClass

Instances For

instance instDecidableEqForceTransmissionClass :

DecidableEq ForceTransmissionClass

Equations

instDecidableEqForceTransmissionClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instBEqForceTransmissionClass.beq :

ForceTransmissionClass → ForceTransmissionClass → Bool

Equations

instBEqForceTransmissionClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance instBEqForceTransmissionClass :

BEq ForceTransmissionClass

Equations

instBEqForceTransmissionClass = { beq := instBEqForceTransmissionClass.beq }

def instReprForceTransmissionClass.repr :

ForceTransmissionClass → ℕ → Std.Format

Equations

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

Instances For

instance instReprForceTransmissionClass :

Repr ForceTransmissionClass

Equations

instReprForceTransmissionClass = { reprPrec := instReprForceTransmissionClass.repr }

def ForceTransmissionClass.outcomeCardinality :

ForceTransmissionClass → OutcomeCardinality

Outcome set cardinality for each force transmission class.

PFC verbs have multi-membered sets because their actions produce one of many possible discrete outcome states (slightly bent, halfway bent, etc.). COS and IE verbs have singleton sets (specific result). No-force verbs have empty sets (no object-state change).

Equations

Instances For

structure BoundaryStates (S : Type) :

Boundary states of an event's impact on an object.

pre = state at left boundary (pre-state, eq. 65) res = state at right boundary (result state, eq. 64)

These are NOT temporal operators — they yield property bundles (lifespan points) at event boundaries, enabling equivalence comparisons across events.

pre : S
State of the object at the left boundary of the event
res : S
State of the object at the right boundary of the event

Instances For

instance instBEqBoundaryStates {S : Type} [BEq S] :

BEq (BoundaryStates S)

Equations

instBEqBoundaryStates = { beq := fun (a b : BoundaryStates S) => a.pre == b.pre && a.res == b.res }

def reversible {S : Type} [BEq S] (base affixed : BoundaryStates S) :

Reversibility condition (eq. 49): the result state of the base event equals the pre-state of the affixed event, and vice versa.

Captures the "inverseness" at the heart of un-.

Equations

reversible base affixed = (base.res == affixed.pre && affixed.res == base.pre)

Instances For

def restitutive {S : Type} [BEq S] (base affixed : BoundaryStates S) :

Restitution condition (eq. 50): the result state of the affixed event equals the result state of the base event.

Captures the "same result achieved again" at the heart of re-.

Equations

restitutive base affixed = (affixed.res == base.res)

Instances For

def ForceTransmissionClass.unCompatible :

ForceTransmissionClass → Bool

un- compatibility (eq. 67): requires multi-membered outcome set (reversibility) AND the possibility of inverse equivalence between boundary states. Only PFC verbs satisfy both conditions.

Equations

Instances For

def ForceTransmissionClass.reCompatible :

ForceTransmissionClass → Bool

re- compatibility (eq. 72): requires a result state that can be re-achieved without a blocking threshold. PFC verbs always qualify. COS verbs qualify when the outcome is not permanently destructive (verb-specific; see LevinClass.reCompatible).

Equations

Instances For

def LevinClass.forceTransmissionClass :

LevinClass → ForceTransmissionClass

Map @cite{levin-1993} classes to force transmission classes.

NOTE: reclassifies some traditionally COS classes as PFC. The bend class (45.2) has changeOfState = true per @cite{levin-1993} but receives multi-membered outcomes per: fold can yield many different states (slightly creased, halfway bent, tightly folded, etc.). This is a refinement, not a contradiction — Bhadra's VRO framework captures finer-grained distinctions within COS.

Equations

Instances For

def LevinClass.reCompatible :

LevinClass → Bool

re- compatibility at the Levin class level.

Within COS, re- is blocked when the outcome permanently eliminates or irreversibly transforms the object. Consumption verbs (*redestroy, *reeat) and killing verbs (*remurder) block re-. Physical property, creation, and degree achievement verbs allow re- (repaint, rebuild, refill).

Equations

Instances For

theorem un_requires_multi (ftc : ForceTransmissionClass) :

ftc.unCompatible = true → ftc.outcomeCardinality = OutcomeCardinality.multi

Only PFC has multi-membered outcomes.

theorem pfc_unique_overlap :

ForceTransmissionClass.potentialForChange.unCompatible = true ∧ ForceTransmissionClass.potentialForChange.reCompatible = true

PFC is the unique class compatible with both un- and re-.

theorem ie_disallows_both :

ForceTransmissionClass.impingementEffecting.unCompatible = false ∧ ForceTransmissionClass.impingementEffecting.reCompatible = false

IE is incompatible with both affixes.

theorem cos_un_blocked_re_available :

ForceTransmissionClass.integralChange.unCompatible = false ∧ ForceTransmissionClass.integralChange.reCompatible = true

COS is un-incompatible but re-compatible (class-level; verb-specific blocking handled by LevinClass.reCompatible).

theorem noforce_disallows_both :

ForceTransmissionClass.noForceTransmission.unCompatible = false ∧ ForceTransmissionClass.noForceTransmission.reCompatible = false

No-force verbs are incompatible with both.

PFC classification is orthogonal to the template-level hasResultState property. Bend (45.2) has a result state (accomplishment template) but coil (9.6) does not (putting template lacks BECOME). Both are PFC — outcome cardinality captures a different dimension than template shape.

theorem bend_cos_per_levin_pfc_per_bhadra :

LevinClass.bend.meaningComponents.changeOfState = true ∧ LevinClass.bend.forceTransmissionClass = ForceTransmissionClass.potentialForChange

reclassifies bend (45.2) from COS to PFC despite Levin's CoS=true meaning components. This is the central refinement.

theorem ie_templates :

LevinClass.wipe.eventTemplate = Semantics.Lexical.Verb.EventStructure.Template.motionContact ∧ LevinClass.hit.eventTemplate = Semantics.Lexical.Verb.EventStructure.Template.activity

IE verbs map to the motionContact template (for wipe class) or activity template (for hit class).

theorem affectedness_bridge_pfc :

Semantics.Lexical.Verb.Affectedness.profileToDegree { volition := false, sentience := false, causation := false, movement := false, independentExistence := false, changeOfState := false, incrementalTheme := false, causallyAffected := true, stationary := true, dependentExistence := false } = Semantics.Lexical.Verb.Affectedness.AffectednessDegree.potential

PFC/IE distinction refines @cite{beavers-2010}'s potential degree. Both PFC and IE objects have causallyAffected without changeOfState, mapping to AffectednessDegree.potential. But they differ in outcome cardinality: PFC → multi (reversible), IE → singleton (irreversible impingement).

The kick object profile (canonical IE) maps to .nonquantized because it has CoS=true; the prototypical PFC profile (CA+St, no CoS) maps to .potential.

theorem affectedness_bridge_ie_kick :

Semantics.Lexical.Verb.Affectedness.profileToDegree Semantics.Lexical.Verb.EntailmentProfile.kickObjectProfile = Semantics.Lexical.Verb.Affectedness.AffectednessDegree.nonquantized

theorem result_roots_singleton_outcomes :

RootType.result.entailsChange = true ∧ RootType.result.allowsRestitutiveAgain = false

Result roots (@cite{beavers-etal-2021}) lexically entail change and thus have singleton outcome sets — the entailed result IS the single outcome. PC roots do not entail change, so their outcome cardinality depends on their force transmission class (COS vs PFC).

theorem pc_roots_allow_restitutive_again :

RootType.propertyConcept.allowsRestitutiveAgain = true ∧ RootType.propertyConcept.entailsChange = false

PC roots allow restitutive 'again' (@cite{beavers-etal-2021}), which aligns with prediction: verbs with multi-membered outcome sets (PFC verbs) can return to a prior state. Result roots cannot, because their singleton outcome is deterministically entailed.

@[reducible, inline]

abbrev StateFunction (Entity : Type u_4) (State : Type u_5) (Time : Type u_6) :

Type (max (max u_4 u_5) u_6)

A state function maps a time point to a lifespan point (property bundle) of an entity (eq. 53).

A lifespan point l(x) is a bundle of properties that an entity x has at a point in its lifespan. The state function connects time to properties via lifespan indexing.

Equations

StateFunction Entity State Time = (Time → Entity → State)

Instances For

@[reducible, inline]

abbrev Applies (Entity : Type u_4) (Time : Type u_5) [LE Time] :

Type (max u_4 u_5)

The APPLIES meta-predicate (eq. 59): the force associated with event e is being exerted on entity x.

This ensures the verb denotes a dynamic process that happened to x, filtering out stative verbs (which have no force transmission).

Equations

Applies Entity Time = (Entity → Semantics.Events.Ev Time → Prop)

Instances For

structure VerbRootVRO (Entity : Type u_4) (State : Type u_5) (Time : Type u_6) [LE Time] :

Type (max (max u_4 u_5) u_6)

Verb-Root-Outcomes: the compositional bundle for a dynamic transitive verb root (eq. 60).

Each verb root is lexically equipped with:

verb: the verb's denotation (entity × event predicate)
outcomes: the set of possible result states after force transmission
thresholds: the set of contextually determined pre-states

For PFC verbs, outcomes is multi-membered (fold can yield slightly bent, halfway bent, tightly folded, etc.). For COS verbs, outcomes is a singleton. For IE verbs, outcomes is a singleton (surface alteration). For no-force verbs, outcomes is empty.

verb : Entity → Semantics.Events.Ev Time → Prop
The verb's truth-conditional predicate: verb(e)(x)
applies : Entity → Semantics.Events.Ev Time → Prop
APPLIES: force transmission predicate
outcomes : Set State
Set of outcomes: possible result states of the object (eq. 56a)
thresholds : Set State
Set of thresholds: possible pre-states of the object (eq. 56b)

Instances For

def resState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (e : Semantics.Events.Ev Time) (x : Entity) :

State

Result state: the state of entity x at the right boundary of event e (eq. 64).

res(e)(x) := stateAt(RB(τ(e)))(x) — the property bundle of x at the temporal right boundary of event e. This is NOT a temporal operator; it yields a lifespan point (state).

Equations

resState stateAt e x = stateAt e.τ.finish x

Instances For

def preState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (e : Semantics.Events.Ev Time) (x : Entity) :

State

Pre-state: the state of entity x at the left boundary of event e (eq. 65).

pre(e)(x) := stateAt(LB(τ(e)))(x) — the property bundle of x at the temporal left boundary of event e.

Equations

preState stateAt e x = stateAt e.τ.start x

Instances For

def Set.multiMembered {State : Type u_2} (s : Set State) :

Multi-membered outcome set: there exist at least two distinct outcomes. This is the |O_e'| > 1 condition in eq. 66.

Equations

s.multiMembered = ∃ (s₁ : State) (s₂ : State), s₁ ∈ s ∧ s₂ ∈ s ∧ s₁ ≠ s₂

Instances For

def unSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (x : Entity) (e : Semantics.Events.Ev Time) :

Full semantics of reversative un- (eq. 66).

⟦un-⟧ᵍ := λP.λx.λe. [∃e': P(e')(x) ∧ APPLIES(e')(x) ∧ τ(e') ≪ τ(e) ∧ res(e')(x) = pre(e)(x) ∧ |O| > 1] ∧ res(e)(x) = pre(e')(x)

The APPLIES condition ensures force was exerted on x in the base event.

Equations

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

Instances For

def rePresupposition {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (x : Entity) (e : Semantics.Events.Ev Time) :

Presupposition of restitutive re- (eq. 68, first line).

There exists a prior event e' such that:

The base verb P holds of e' and x
APPLIES(e')(x) — force was exerted on x in the prior event
The prior event temporally precedes the re-event: τ(e') ≪ τ(e)
Result-state equivalence: res(e)(x) = res(e')(x)

Equations

rePresupposition stateAt vro x e = ∃ (e' : Semantics.Events.Ev Time), vro.verb x e' ∧ vro.applies x e' ∧ e'.τ.precedes e.τ ∧ resState stateAt e x = resState stateAt e' x

Instances For

def reSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (x : Entity) (e : Semantics.Events.Ev Time) :

Full semantics of restitutive re- (eq. 68).

⟦re-⟧ᵍ := λP.λx.λe. [∃e': P(e')(x) ∧ APPLIES(e')(x) ∧ τ(e') ≪ τ(e) ∧ res(e)(x) = res(e')(x)] ∧ APPLIES(e)(x) ∧ P(e)(x)

The APPLIES conditions ensure force transmission in both the prior and re-events. This is what compositionally blocks re-destroy: after destruction, APPLIES fails for the re-event because force cannot be exerted on a non-existent object.

Equations

reSem stateAt vro x e = (rePresupposition stateAt vro x e ∧ vro.applies x e ∧ vro.verb x e)

Instances For

theorem singleton_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (h_single : ∃ (s : State), vro.outcomes = {s}) (x : Entity) (e : Semantics.Events.Ev Time) :

¬unSem stateAt vro x e

Singleton outcome sets cannot satisfy the multi-membered presupposition of un-. If a verb's outcome set has exactly one member, unSem is unsatisfiable (because multiMembered requires two distinct elements).

This derives the distributional prediction: COS and IE verbs block un- because their singleton outcome sets fail the |O| > 1 presupposition.

theorem empty_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (h_empty : vro.outcomes = ∅) (x : Entity) (e : Semantics.Events.Ev Time) :

¬unSem stateAt vro x e

Empty outcome sets also block un-. If a verb exerts no force (no outcomes), the multi-membered presupposition trivially fails.