Bhadra (2024): Verb roots encode outcomes

This file formalizes Bhadra's account of the reversative prefix un- and the restitutive prefix re-. Every dynamic transitive root lexically carries a set of outcomes, the states its object can be in at the right boundary of the event, while a contextual set of thresholds collects the states an object can be in at the left boundary. Potential-for-change roots such as fold, wrap and coil have several outcomes, change-of-state and impingement-effecting roots such as break, shatter and hit have a single lexically specified outcome, and roots unspecified for change have none. Un- presupposes a prior base event whose result the object is still in and several outcomes, and asserts that the object returns to the base event's initial state. Re- presupposes a prior base event with the same result and requires that the base action not leave the object where that result cannot be restored. Cardinality thus governs un- alone and threshold structure governs re-, so the two prefixes overlap exactly on the potential-for-change class.

The hierarchy of outcome sets cross-classifies Beavers's affectedness hierarchy. Beavers places the impingement-effecting verbs with the potential-for-change verbs, while their single outcome puts them with the change-of-state verbs, whose single outcome may be a quantized or a non-quantized change.

Implementation notes

• Each VerbOutcomes fixes its outcome and threshold sets once per root and object, so the object-dependence the paper locates at the minimal verb phrase is modelled by distinct records for distinct objects.
• The degrees of affectedness are those the paper reports for its classes of verbs, and it reports none for the transformation, movement and creation classes. Its critique of Beavers's definition of potential for change (§6.1) is not formalized.

References

• D. Bhadra, Verb roots encode outcomes: argument structure and lexical semantics of reversal and restitution (2024)
• J. Beavers, On Affectedness (2011)

Outcome cardinality

inductive Bhadra2024.OutcomeCardinality : Type

An outcome cardinality is the tier of an outcome set, ordered empty < singleton < multi (62).

• empty : OutcomeCardinality
• singleton : OutcomeCardinality
• multi : OutcomeCardinality

@[instance_reducible]

instance Bhadra2024.instReprOutcomeCardinality : Repr OutcomeCardinality

Equations

• Bhadra2024.instReprOutcomeCardinality = { reprPrec := Bhadra2024.instReprOutcomeCardinality.repr }

def Bhadra2024.instReprOutcomeCardinality.repr : OutcomeCardinality → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instDecidableEqOutcomeCardinality : DecidableEq OutcomeCardinality

Equations

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

def Bhadra2024.OutcomeCardinality.toNat : OutcomeCardinality → ℕ

c.rank is the rank of the tier c as a natural number.

Equations

• Bhadra2024.OutcomeCardinality.empty.toNat = 0
• Bhadra2024.OutcomeCardinality.singleton.toNat = 1
• Bhadra2024.OutcomeCardinality.multi.toNat = 2

theorem Bhadra2024.OutcomeCardinality.toNat_injective : Function.Injective toNat

@[instance_reducible]

instance Bhadra2024.OutcomeCardinality.instLinearOrder : LinearOrder OutcomeCardinality

Equations

• Bhadra2024.OutcomeCardinality.instLinearOrder = LinearOrder.lift' Bhadra2024.OutcomeCardinality.toNat Bhadra2024.OutcomeCardinality.toNat_injective

theorem Bhadra2024.OutcomeCardinality.empty_lt_singleton : empty < singleton

theorem Bhadra2024.OutcomeCardinality.singleton_lt_multi : singleton < multi

noncomputable def Bhadra2024.OutcomeCardinality.ofSet {State : Type u_1} (O : Set State) : OutcomeCardinality

The tier of an outcome set is multi when it is nontrivial, empty when it is empty, and singleton otherwise.

Equations

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

theorem Bhadra2024.OutcomeCardinality.ofSet_eq_multi {State : Type u_1} {O : Set State} (h : O.Nontrivial) : ofSet O = multi

theorem Bhadra2024.OutcomeCardinality.ofSet_eq_singleton {State : Type u_1} {O : Set State} (hne : O.Nonempty) (hnt : ¬O.Nontrivial) : ofSet O = singleton

theorem Bhadra2024.OutcomeCardinality.ofSet_eq_empty {State : Type u_1} {O : Set State} (h : ¬O.Nonempty) : ofSet O = empty

@[simp]

theorem Bhadra2024.OutcomeCardinality.ofSet_singleton {State : Type u_1} (s : State) : ofSet {s} = singleton

@[simp]

theorem Bhadra2024.OutcomeCardinality.ofSet_empty {State : Type u_1} : ofSet ∅ = empty

inductive Bhadra2024.OutcomeClass : Type

An outcome class classifies dynamic transitive roots by what their outcome sets encode, the potential-for-change class (60) and the classes with a lexically specified result or none (61a–h).

• potentialForChange : OutcomeClass
• physicalProperty : OutcomeClass
• transformation : OutcomeClass
• movement : OutcomeClass
• consumption : OutcomeClass
• creation : OutcomeClass
• degreeAchievement : OutcomeClass
• impingement : OutcomeClass
• noChange : OutcomeClass

@[instance_reducible]

instance Bhadra2024.instDecidableEqOutcomeClass : DecidableEq OutcomeClass

Equations

• Bhadra2024.instDecidableEqOutcomeClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprOutcomeClass.repr : OutcomeClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprOutcomeClass : Repr OutcomeClass

Equations

• Bhadra2024.instReprOutcomeClass = { reprPrec := Bhadra2024.instReprOutcomeClass.repr }

def Bhadra2024.OutcomeClass.tier : OutcomeClass → OutcomeCardinality

The outcome tier of a class is multi-membered for potential-for-change roots, singleton for every root with a lexically specified result, and empty for roots unspecified for change (62).

Equations

• Bhadra2024.OutcomeClass.potentialForChange.tier = Bhadra2024.OutcomeCardinality.multi
• Bhadra2024.OutcomeClass.noChange.tier = Bhadra2024.OutcomeCardinality.empty
• x✝.tier = Bhadra2024.OutcomeCardinality.singleton

theorem Bhadra2024.tier_eq_multi_iff (c : OutcomeClass) : c.tier = OutcomeCardinality.multi ↔ c = OutcomeClass.potentialForChange

Potential-for-change roots are the only class whose outcome sets are multi-membered.

States, boundaries, and roots

@[reducible, inline]

abbrev Bhadra2024.StateFunction (Entity : Type u_1) (State : Type u_2) (T : Type u_3) : Type (max (max u_1 u_2) u_3)

A state function gives an object's state at each time, a lifespan point (53).

Equations

• Bhadra2024.StateFunction Entity State T = (T → Entity → State)

def Bhadra2024.resState {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (e : E) (x : Entity) : State

res(e)(x) is the object's state at the right boundary of e (64).

Equations

• Bhadra2024.resState k e x = k (Event.τ e).toProd.2 x

def Bhadra2024.preState {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (e : E) (x : Entity) : State

pre(e)(x) is the object's state at the left boundary of e (65).

Equations

• Bhadra2024.preState k e x = k (Event.τ e).toProd.1 x

structure Bhadra2024.VerbOutcomes (E : Type u_5) (Entity : Type u_6) (State : Type u_7) : Type (max (max u_5 u_6) u_7)

A verb root, as the prefixes see it, is its base predicate together with the lexical outcome set of states at the right boundary and the contextual threshold set of states at the left boundary ((56), (60)).

• verb : E → Entity → Prop

  The base predicate P(e)(x).

• outcomes : Set State

  The outcome set O.

• thresholds : Set State

  The threshold set T.

noncomputable def Bhadra2024.VerbOutcomes.cardinality {Entity : Type u_1} {State : Type u_2} {E : Type u_4} (vro : VerbOutcomes E Entity State) : OutcomeCardinality

The cardinality of a root is the tier of its outcome set.

Equations

• vro.cardinality = Bhadra2024.OutcomeCardinality.ofSet vro.outcomes

The prefixes as result-state modifiers

def Bhadra2024.unSem {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (e : E) (x : Entity) : Prop

Reversative un- (66) requires a prior base event e' whose result is the state the un- event starts from and a multi-membered outcome set, and returns the object to the base event's initial state. The vacuous ∃ Q. Q(e)(x) of the assertion is dropped.

Equations

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

def Bhadra2024.reSem {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (e : E) (x : Entity) : Prop

Restitutive re- ((68), (72)) requires a prior base event e' with the same result, whose result state is an admissible start state, so that the base action does not leave the object where its result cannot be restored, and requires the base predicate to hold of the re- event. It places no demand on the cardinality of the outcome set.

Equations

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

theorem Bhadra2024.subsingleton_blocks_un {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (h : ¬vro.outcomes.Nontrivial) (e : E) (x : Entity) : ¬unSem k vro e x

A root whose outcome set is not multi-membered cannot host un- (67).

theorem Bhadra2024.singleton_blocks_un {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (s : State) (hs : vro.outcomes = {s}) (e : E) (x : Entity) : ¬unSem k vro e x

theorem Bhadra2024.empty_blocks_un {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (hs : vro.outcomes = ∅) (e : E) (x : Entity) : ¬unSem k vro e x

theorem Bhadra2024.un_requires_multi {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (e : E) (x : Entity) (h : unSem k vro e x) : vro.cardinality = OutcomeCardinality.multi

Hosting un- forces a root's outcome set into the multi-membered tier.

theorem Bhadra2024.not_reSem_of_outcome_not_threshold {Entity : Type u_1} {State : Type u_2} {T : Type u_3} {E : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] (k : StateFunction Entity State T) (vro : VerbOutcomes E Entity State) (x : Entity) (h : ∀ (e' : E), vro.verb e' x → resState k e' x ∉ vro.thresholds) (e : E) : ¬reSem k vro e x

A base action whose result is never an admissible start state blocks re- (72).

Worked roots

def Bhadra2024.ev₁ : NonemptyInterval ℤ

ev₁ is the base event of the scenario, over [0, 5].

Equations

• Bhadra2024.ev₁ = { fst := 0, snd := 5, fst_le_snd := Bhadra2024.ev₁._proof_2 }

def Bhadra2024.ev₂ : NonemptyInterval ℤ

ev₂ is the prefixed event of the scenario, over [10, 15].

Equations

• Bhadra2024.ev₂ = { fst := 10, snd := 15, fst_le_snd := Bhadra2024.ev₂._proof_2 }

def Bhadra2024.acts : NonemptyInterval ℤ → Unit → Prop

The base predicate of every worked root holds of the scenario's two events.

Equations

• Bhadra2024.acts e x✝ = (e = Bhadra2024.ev₁ ∨ e = Bhadra2024.ev₂)

def Bhadra2024.twice {State : Type u_5} (start result : State) : StateFunction Unit State ℤ

A root whose action carries the object from start to result at the base event and again at the prefixed event, both acting on the same object.

Equations

• Bhadra2024.twice start result t x✝ = if t ≤ 0 then start else result

def Bhadra2024.andBack {State : Type u_5} (start result : State) : StateFunction Unit State ℤ

A root whose action carries the object from start to result at the base event and back to start at the prefixed event.

Equations

• Bhadra2024.andBack start result t x✝ = if t ≤ 0 then start else if t ≤ 10 then result else start

inductive Bhadra2024.ParchmentState : Type

A parchment under folding is flat, slightly creased, folded or tightly folded (54).

• flat : ParchmentState
• slightlyCreased : ParchmentState
• folded : ParchmentState
• tightlyFolded : ParchmentState

@[instance_reducible]

instance Bhadra2024.instDecidableEqParchmentState : DecidableEq ParchmentState

Equations

• Bhadra2024.instDecidableEqParchmentState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprParchmentState.repr : ParchmentState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprParchmentState : Repr ParchmentState

Equations

• Bhadra2024.instReprParchmentState = { reprPrec := Bhadra2024.instReprParchmentState.repr }

def Bhadra2024.foldVRO : VerbOutcomes (NonemptyInterval ℤ) Unit ParchmentState

Fold is a potential-for-change root (60), with a multi-membered outcome set, and a folded parchment can be folded again.

Equations

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

theorem Bhadra2024.fold_outcomes_multi : foldVRO.outcomes.Nontrivial

theorem Bhadra2024.fold_un : unSem (andBack ParchmentState.flat ParchmentState.folded) foldVRO ev₂ ()

Veena unfolded the parchment is true in the scenario, the worked derivation of (66).

theorem Bhadra2024.fold_re : reSem (twice ParchmentState.flat ParchmentState.folded) foldVRO ev₂ ()

Re- attaches to fold as well, on the multi-membered tier.

inductive Bhadra2024.LimbState : Type

• intact : LimbState
• broken : LimbState

@[instance_reducible]

instance Bhadra2024.instDecidableEqLimbState : DecidableEq LimbState

Equations

• Bhadra2024.instDecidableEqLimbState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprLimbState.repr : LimbState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprLimbState : Repr LimbState

Equations

• Bhadra2024.instReprLimbState = { reprPrec := Bhadra2024.instReprLimbState.repr }

def Bhadra2024.breakLimbVRO : VerbOutcomes (NonemptyInterval ℤ) Unit LimbState

Break applied to a limb (61a) has a single result, and a broken limb admits another breaking (73a).

Equations

• Bhadra2024.breakLimbVRO = { verb := Bhadra2024.acts, outcomes := {Bhadra2024.LimbState.broken}, thresholds := {Bhadra2024.LimbState.intact, Bhadra2024.LimbState.broken} }

def Bhadra2024.breakSewerVRO : VerbOutcomes (NonemptyInterval ℤ) Unit LimbState

Break applied to a sewer has the same single result, which a sewer cannot informatively reach again (73a).

Equations

• Bhadra2024.breakSewerVRO = { verb := Bhadra2024.acts, outcomes := {Bhadra2024.LimbState.broken}, thresholds := {Bhadra2024.LimbState.intact} }

theorem Bhadra2024.breakLimb_not_un (k : StateFunction Unit LimbState ℤ) (e : NonemptyInterval ℤ) : ¬unSem k breakLimbVRO e ()

#Unbreak a limb fails, the outcome set being a singleton (67).

theorem Bhadra2024.breakLimb_re : reSem (twice LimbState.intact LimbState.broken) breakLimbVRO ev₂ ()

Rebreak a limb is true in the scenario (73a).

theorem Bhadra2024.breakSewer_not_re (e : NonemptyInterval ℤ) : ¬reSem (twice LimbState.intact LimbState.broken) breakSewerVRO e ()

#Rebreak a sewer fails, since a broken sewer is not an admissible start state (73a).

inductive Bhadra2024.SurfaceState : Type

• unaltered : SurfaceState
• surfaceAltered : SurfaceState

@[instance_reducible]

instance Bhadra2024.instDecidableEqSurfaceState : DecidableEq SurfaceState

Equations

• Bhadra2024.instDecidableEqSurfaceState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprSurfaceState.repr : SurfaceState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprSurfaceState : Repr SurfaceState

Equations

• Bhadra2024.instReprSurfaceState = { reprPrec := Bhadra2024.instReprSurfaceState.repr }

def Bhadra2024.hitVRO : VerbOutcomes (NonemptyInterval ℤ) Unit SurfaceState

Hit is an impingement-effecting root (61g), with a single, irreversible surface alteration.

Equations

• Bhadra2024.hitVRO = { verb := Bhadra2024.acts, outcomes := {Bhadra2024.SurfaceState.surfaceAltered}, thresholds := {Bhadra2024.SurfaceState.unaltered} }

theorem Bhadra2024.hit_not_un (k : StateFunction Unit SurfaceState ℤ) (e : NonemptyInterval ℤ) : ¬unSem k hitVRO e ()

*Unhit fails (25).

theorem Bhadra2024.hit_not_re (e : NonemptyInterval ℤ) : ¬reSem (twice SurfaceState.unaltered SurfaceState.surfaceAltered) hitVRO e ()

*Rehit fails, since impingement leaves the surface altered and never again unaltered (48).

inductive Bhadra2024.TruckState : Type

• empty : TruckState
• full : TruckState

@[instance_reducible]

instance Bhadra2024.instDecidableEqTruckState : DecidableEq TruckState

Equations

• Bhadra2024.instDecidableEqTruckState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bhadra2024.instReprTruckState : Repr TruckState

Equations

• Bhadra2024.instReprTruckState = { reprPrec := Bhadra2024.instReprTruckState.repr }

def Bhadra2024.instReprTruckState.repr : TruckState → ℕ → Std.Format

Equations

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

def Bhadra2024.loadVRO : VerbOutcomes (NonemptyInterval ℤ) Unit TruckState

Load is a degree achievement (70), with a single contextually salient result that does not prevent loading again.

Equations

• Bhadra2024.loadVRO = { verb := Bhadra2024.acts, outcomes := {Bhadra2024.TruckState.full}, thresholds := {Bhadra2024.TruckState.empty, Bhadra2024.TruckState.full} }

theorem Bhadra2024.load_re : reSem (twice TruckState.empty TruckState.full) loadVRO ev₂ ()

Raj reloaded the truck is true in the scenario (69a).

inductive Bhadra2024.MirrorState : Type

• intact : MirrorState
• shattered : MirrorState

@[instance_reducible]

instance Bhadra2024.instDecidableEqMirrorState : DecidableEq MirrorState

Equations

• Bhadra2024.instDecidableEqMirrorState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bhadra2024.instReprMirrorState.repr : MirrorState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bhadra2024.instReprMirrorState : Repr MirrorState

Equations

• Bhadra2024.instReprMirrorState = { reprPrec := Bhadra2024.instReprMirrorState.repr }

def Bhadra2024.shatterVRO : VerbOutcomes (NonemptyInterval ℤ) Unit MirrorState

Shatter (71) has a single result that leaves the object outside every threshold.

Equations

• Bhadra2024.shatterVRO = { verb := Bhadra2024.acts, outcomes := {Bhadra2024.MirrorState.shattered}, thresholds := {Bhadra2024.MirrorState.intact} }

theorem Bhadra2024.shatter_not_re (e : NonemptyInterval ℤ) : ¬reSem (twice MirrorState.intact MirrorState.shattered) shatterVRO e ()

#The children reshattered the mirror fails (69b).

theorem Bhadra2024.re_on_singleton : loadVRO.cardinality = OutcomeCardinality.singleton ∧ reSem (twice TruckState.empty TruckState.full) loadVRO ev₂ ()

Re- is indifferent to outcome cardinality, attaching to a root with a single outcome.

The affectedness hierarchy (§2.4, (20), (62))

inductive Bhadra2024.BeaversDegree : OutcomeClass → ArgumentStructure.AffectednessDegree → Prop

BeaversDegree c d holds when the paper places verbs of the class c at the degree d of Beavers's affectedness hierarchy ((20), §2.4.2).

• physicalProperty : BeaversDegree OutcomeClass.physicalProperty ArgumentStructure.AffectednessDegree.quantized

  Break undergoes a quantized change ((20a)).

• consumption : BeaversDegree OutcomeClass.consumption ArgumentStructure.AffectednessDegree.quantized

  Destroy and devour effect a quantized change ((20a)).

• degreeAchievement : BeaversDegree OutcomeClass.degreeAchievement ArgumentStructure.AffectednessDegree.nonquantized

  Degree achievements effect a non-quantized change ((20b)).

• potentialForChange : BeaversDegree OutcomeClass.potentialForChange ArgumentStructure.AffectednessDegree.potential

  Wrap and furl give their object potential for change ((20d)).

• impingement : BeaversDegree OutcomeClass.impingement ArgumentStructure.AffectednessDegree.potential

  Beavers places surface-contact verbs such as hit and wipe under potential for change, a placement the paper rejects in separating them as impingement-effecting (§2.4.2).

• noChange : BeaversDegree OutcomeClass.noChange ArgumentStructure.AffectednessDegree.unspecified

  See and laugh at are unspecified for change ((20c)).

theorem Bhadra2024.potentialForChange_impingement : (∃ (d : ArgumentStructure.AffectednessDegree), BeaversDegree OutcomeClass.potentialForChange d ∧ BeaversDegree OutcomeClass.impingement d) ∧ OutcomeClass.potentialForChange.tier ≠ OutcomeClass.impingement.tier

Potential-for-change and impingement-effecting verbs share a degree of affectedness but not an outcome tier, which is why the paper separates them (§2.4.2, (62)).

theorem Bhadra2024.consumption_degreeAchievement : OutcomeClass.consumption.tier = OutcomeClass.degreeAchievement.tier ∧ ∃ (d : ArgumentStructure.AffectednessDegree) (d' : ArgumentStructure.AffectednessDegree), d ≠ d' ∧ BeaversDegree OutcomeClass.consumption d ∧ BeaversDegree OutcomeClass.degreeAchievement d'

Consumption verbs and degree achievements share the singleton tier but not a degree of affectedness, the tier of lexically specified change including quantized and non-quantized change ((62)).