Yu, Ausensi & Smith (2023): States and Changes-of-State in the Semantics of Result Roots

This file formalizes the account of result roots by Yu, Ausensi and Smith. The roots of result verbs are of two types. A property concept root, such as that of open, relates an individual to a state. A change-of-state root, such as that of break, relates an individual to an event of change into the state the root names, so it is the change-of-state head applied to a state predicate (changeOfState). Events and states are sorts of one domain of eventualities.

Three predictions follow from the types. Again attached to a change-of-state root presupposes an earlier change, so such verbs have no restitutive reading, a prediction shared with Beavers and Koontz-Garboden's stative roots that entail change. A durative for-phrase measures a state only where a constituent holds of states, which a change-of-state root never does (not_isState_of_changeOfState). And a root modifies a resultative verb phrase, by conjunction with it, only if it holds of events, so a property concept root cannot (not_modifies_of_isStative) while a change-of-state root can, with the holder of its state existentially closed.

Implementation notes

• The causative head relates an event to the state it causes, as in the paper, with no change-of-state head beneath it and the agent introduced separately.
• The derivations with Voice and existential closure at the verb phrase are not represented.

References

• [YAS23]
• [BKG20]

Roots of two types

structure YuAusensiSmith2023.Sorted {Entity : Type u_1} {Ev : Type u_2} (M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev) (IsState : Ev → Prop) : Prop

The interpretation is sorted when a change is an event giving rise to a state, and a cause is an event bringing about a state.

• isState_of_become {s e : Ev} : M.become s e → IsState s
• not_isState_of_become {s e : Ev} : M.become s e → ¬IsState e
• isState_of_cause {e s : Ev} : M.cause e s → IsState s
• not_isState_of_cause {e s : Ev} : M.cause e s → ¬IsState e

def YuAusensiSmith2023.IsStative {Entity : Type u_1} {Ev : Type u_2} (IsState : Ev → Prop) (B : Entity → Ev → Prop) : Prop

A property concept root holds of states only.

Equations

• YuAusensiSmith2023.IsStative IsState B = ∀ (x : Entity) (s : Ev), B x s → IsState s

def YuAusensiSmith2023.changeOfState {Entity : Type u_1} {Ev : Type u_2} (M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev) (B : Entity → Ev → Prop) : Entity → Ev → Prop

A change-of-state root relates an individual to an event of change into a state of B.

Equations

• YuAusensiSmith2023.changeOfState M B = M.vBecome B

def YuAusensiSmith2023.vCause {Entity : Type u_1} {Ev : Type u_2} (M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev) (L : Ev → Prop) (e : Ev) : Prop

The causative head relates an event to a state of L that it causes.

Equations

• YuAusensiSmith2023.vCause M L e = ∃ (s : Ev), M.cause e s ∧ L s

def YuAusensiSmith2023.modify {Entity : Type u_1} {Ev : Type u_2} (R : Entity → Ev → Prop) (V : Ev → Prop) (x : Entity) (e : Ev) : Prop

A root modifies a verb phrase by conjunction with it.

Equations

• YuAusensiSmith2023.modify R V x e = (R x e ∧ V e)

theorem YuAusensiSmith2023.not_isState_of_changeOfState {Entity : Type u_1} {Ev : Type u_2} {M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev} {IsState : Ev → Prop} {B : Entity → Ev → Prop} {x : Entity} {e : Ev} (h : Sorted M IsState) (he : changeOfState M B x e) : ¬IsState e

A change-of-state root holds of no state, so no constituent built on it alone is stative.

theorem YuAusensiSmith2023.not_isState_of_vCause {Entity : Type u_1} {Ev : Type u_2} {M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev} {IsState L : Ev → Prop} {e : Ev} (h : Sorted M IsState) (he : vCause M L e) : ¬IsState e

A causative verb phrase holds of no state.

theorem YuAusensiSmith2023.not_modifies_of_isStative {Entity : Type u_1} {Ev : Type u_2} {M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev} {IsState : Ev → Prop} {B : Entity → Ev → Prop} {L : Ev → Prop} {x : Entity} {e : Ev} (h : Sorted M IsState) (hB : IsStative IsState B) : ¬modify B (vCause M L) x e

A property concept root cannot modify a causative verb phrase, since nothing is both a state and an event.

theorem YuAusensiSmith2023.exists_of_modify_changeOfState {Entity : Type u_1} {Ev : Type u_2} {M : ArgumentStructure.EventStructure.Interpretation Entity Ev Ev} {B : Entity → Ev → Prop} {L : Ev → Prop} {e : Ev} (h : ∃ (x : Entity), modify (changeOfState M B) (vCause M L) x e) : (∃ (x : Entity) (s : Ev), M.become s e ∧ B x s) ∧ ∃ (s : Ev), M.cause e s ∧ L s

A resultative built on a change-of-state root entails that something came to be in a state of the root and that the event caused a state of the result phrase.

Again

theorem YuAusensiSmith2023.change_of_again_changeOfState {Entity : Type u_1} {State Event : Type u} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {R : SetRel Event Event} {B : Entity → State → Prop} {x : Entity} {e : Event} (h : Presupposition.again R (M.vBecome B x) e ≠ 0) : ∃ (e' : Event), (e, e') ∈ R ∧ ∃ (s : State), M.become s e'

Again attached to a change-of-state root presupposes an earlier change, so no attachment gives a restitutive reading.

Breaking the corpse loose

inductive YuAusensiSmith2023.Ev : Type

The eventualities of a couple of monks broke the corpse loose from the deck.

• breaking : Ev
• broken : Ev
• loose : Ev

@[instance_reducible]

instance YuAusensiSmith2023.instDecidableEqEv : DecidableEq Ev

Equations

• YuAusensiSmith2023.instDecidableEqEv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YuAusensiSmith2023.monks : ArgumentStructure.EventStructure.Interpretation Unit Ev Ev

The breaking gives rise to the broken state and causes the loose one.

Equations

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

def YuAusensiSmith2023.IsState (v : Ev) : Prop

The states of the scene.

Equations

• YuAusensiSmith2023.IsState v = (v ≠ YuAusensiSmith2023.Ev.breaking)

@[instance_reducible]

instance YuAusensiSmith2023.instDecidablePredEvIsState : DecidablePred IsState

Equations

• YuAusensiSmith2023.instDecidablePredEvIsState x✝ = { decide := !decide (x✝ = YuAusensiSmith2023.Ev.breaking), reflects_decide := ⋯ }

theorem YuAusensiSmith2023.sorted_monks : Sorted monks IsState

theorem YuAusensiSmith2023.modify_monks : modify (changeOfState monks fun (x : Unit) (s : Ev) => s = Ev.broken) (vCause monks fun (x : Ev) => x = Ev.loose) () Ev.breaking

The change-of-state root modifies the resultative verb phrase, with the broken state and the loose state distinct.

theorem YuAusensiSmith2023.not_stative_modify_monks : ¬∃ (s : Ev), modify (fun (x : Unit) (s : Ev) => s = Ev.broken) (fun (x : Ev) => x = Ev.loose) () s

On the stative analysis of the root the result phrase must describe the root's own state, and no state of the scene is both the broken one and the loose one.

The judgments

theorem YuAusensiSmith2023.restitutive_iff_propertyConcept (e : Datum) : e ∈ Examples.all → e.feature? "diagnostic" = some "again" → (List.lookup "restitutive" e.readings = some Judgment.acceptable ↔ e.feature? "root class" = some "property concept")

Again has a restitutive reading in the examples exactly with a property concept root.

theorem YuAusensiSmith2023.internal_iff_propertyConcept (e : Datum) : e ∈ Examples.all → e.feature? "diagnostic" = some "for-phrase" → (List.lookup "internal" e.readings = some Judgment.acceptable ↔ e.feature? "root class" = some "property concept")

A for-phrase has an internal reading in the examples exactly with a property concept root.

theorem YuAusensiSmith2023.modifier_iff_changeOfState (e : Datum) : e ∈ Examples.all → e.feature? "diagnostic" = some "resultative modifier" → (e.judgment = Judgment.acceptable ↔ e.feature? "root class" = some "change of state")

A root modifies a resultative in the examples exactly when it is a change-of-state root.