Levin and Rappaport Hovav (1995): Unaccusativity

This file formalizes the linking rules of [LRH95] and the classification of [Lev93]'s intransitive verb classes they yield. The Immediate Cause Linking Rule (1), the Directed Change Linking Rule (24), the Existence Linking Rule (47) and the Default Linking Rule (49) of chapter 4 assign an argument to the external or the direct internal argument position from what the verb's meaning says of it (Characterization), the Directed Change and Existence rules taking precedence over the Immediate Cause rule and that over the Default rule (§4.2, link); a monadic verb is unaccusative when its sole argument is a direct internal argument. Appendix A assigns Levin's classes to the book's semantic classes (characterizations), whence chapter 4's verdicts: verbs of emission are unergative, verbs of change of state, of inherently directed motion and of existence and appearance unaccusative whatever their agentivity, the run verbs unergative and the roll verbs unaccusative when nonagentive. The book's diagnostics in Data/Examples/LevinRappaportHovav1995.json sort the verbs the same way (diagnostics_agree).

Implementation notes

• A class the book discusses under several construals, such as the verbs of spatial configuration in their simple, maintain and assume position senses, lists one characterization per construal, and a data row records whether its verb is used agentively.
• The relative order of the Directed Change and Existence rules, which the book leaves open (§4.2.4), does not affect the position either assigns.

References

• [LRH95]
• [Lev93]

structure LevinRappaportHovav1995.Characterization : Type

What a verb's meaning says of an argument, as the linking rules read it: whether it is the immediate cause of the eventuality, so that the verb is internally caused (§3.2.1), whether it undergoes a directed change (§4.1.2), and whether its existence is asserted or denied (§4.1.3).

• immediateCause : Bool
• directedChange : Bool
• existence : Bool

@[instance_reducible]

instance LevinRappaportHovav1995.instDecidableEqCharacterization : DecidableEq Characterization

Equations

• LevinRappaportHovav1995.instDecidableEqCharacterization = LevinRappaportHovav1995.instDecidableEqCharacterization.decEq

def LevinRappaportHovav1995.instDecidableEqCharacterization.decEq (x✝ x✝¹ : Characterization) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LevinRappaportHovav1995.instReprCharacterization : Repr Characterization

Equations

• LevinRappaportHovav1995.instReprCharacterization = { reprPrec := LevinRappaportHovav1995.instReprCharacterization.repr }

def LevinRappaportHovav1995.instReprCharacterization.repr : Characterization → ℕ → Std.Format

Equations

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

inductive LevinRappaportHovav1995.Position : Type

The argument-structure positions the rules assign.

• external : Position
• directInternal : Position

@[instance_reducible]

instance LevinRappaportHovav1995.instDecidableEqPosition : DecidableEq Position

Equations

• LevinRappaportHovav1995.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LevinRappaportHovav1995.instReprPosition : Repr Position

Equations

• LevinRappaportHovav1995.instReprPosition = { reprPrec := LevinRappaportHovav1995.instReprPosition.repr }

def LevinRappaportHovav1995.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

inductive LevinRappaportHovav1995.LinkingRule : Type

The four linking rules of chapter 4.

• immediateCause : LinkingRule

  (1): the argument denoting the immediate cause is the external argument.

• directedChange : LinkingRule

  (24): the argument undergoing the directed change is the direct internal argument.

• existence : LinkingRule

  (47): the argument whose existence is asserted or denied is the direct internal argument.

• default : LinkingRule

  (49): an argument under the scope of no other rule is the direct internal argument.

@[instance_reducible]

instance LevinRappaportHovav1995.instDecidableEqLinkingRule : DecidableEq LinkingRule

Equations

• LevinRappaportHovav1995.instDecidableEqLinkingRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LevinRappaportHovav1995.instReprLinkingRule : Repr LinkingRule

Equations

• LevinRappaportHovav1995.instReprLinkingRule = { reprPrec := LevinRappaportHovav1995.instReprLinkingRule.repr }

def LevinRappaportHovav1995.instReprLinkingRule.repr : LinkingRule → ℕ → Std.Format

Equations

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

def LevinRappaportHovav1995.LinkingRule.Applies : LinkingRule → Characterization → Prop

The rule's scope.

Equations

• LevinRappaportHovav1995.LinkingRule.immediateCause.Applies x✝ = (x✝.immediateCause = true)
• LevinRappaportHovav1995.LinkingRule.directedChange.Applies x✝ = (x✝.directedChange = true)
• LevinRappaportHovav1995.LinkingRule.existence.Applies x✝ = (x✝.existence = true)
• LevinRappaportHovav1995.LinkingRule.default.Applies x✝ = (x✝.immediateCause = false ∧ x✝.directedChange = false ∧ x✝.existence = false)

@[instance_reducible]

instance LevinRappaportHovav1995.LinkingRule.instDecidableApplies (r : LinkingRule) (c : Characterization) : Decidable (r.Applies c)

Equations

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

def LevinRappaportHovav1995.LinkingRule.position : LinkingRule → Position

The position the rule assigns.

Equations

• LevinRappaportHovav1995.LinkingRule.immediateCause.position = LevinRappaportHovav1995.Position.external
• x✝.position = LevinRappaportHovav1995.Position.directInternal

def LevinRappaportHovav1995.LinkingRule.rank : LinkingRule → ℕ

Precedence (§4.2.4), lower first: the Directed Change and Existence rules over the Immediate Cause rule over the Default rule.

Equations

• LevinRappaportHovav1995.LinkingRule.directedChange.rank = 0
• LevinRappaportHovav1995.LinkingRule.existence.rank = 0
• LevinRappaportHovav1995.LinkingRule.immediateCause.rank = 1
• LevinRappaportHovav1995.LinkingRule.default.rank = 2

def LevinRappaportHovav1995.link (c : Characterization) : LinkingRule

The rule that links the argument: the applicable rule of highest precedence.

Equations

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

theorem LevinRappaportHovav1995.link_applies (c : Characterization) : (link c).Applies c

theorem LevinRappaportHovav1995.link_rank_le (c : Characterization) (r : LinkingRule) (h : r.Applies c) : (link c).rank ≤ r.rank

def LevinRappaportHovav1995.Unaccusative (c : Characterization) : Prop

The verb is unaccusative: its sole argument is a direct internal argument.

Equations

• LevinRappaportHovav1995.Unaccusative c = ((LevinRappaportHovav1995.link c).position = LevinRappaportHovav1995.Position.directInternal)

def LevinRappaportHovav1995.Unergative (c : Characterization) : Prop

The verb is unergative: its sole argument is the external argument.

Equations

• LevinRappaportHovav1995.Unergative c = ((LevinRappaportHovav1995.link c).position = LevinRappaportHovav1995.Position.external)

@[instance_reducible]

instance LevinRappaportHovav1995.instDecidableUnaccusative (c : Characterization) : Decidable (Unaccusative c)

Equations

• LevinRappaportHovav1995.instDecidableUnaccusative c = LevinRappaportHovav1995.instDecidableUnaccusative._aux_1 c

@[instance_reducible]

instance LevinRappaportHovav1995.instDecidableUnergative (c : Characterization) : Decidable (Unergative c)

Equations

• LevinRappaportHovav1995.instDecidableUnergative c = LevinRappaportHovav1995.instDecidableUnergative._aux_1 c

theorem LevinRappaportHovav1995.unaccusative_iff (c : Characterization) : Unaccusative c ↔ c.directedChange = true ∨ c.existence = true ∨ c.immediateCause = false

Unaccusativity in one line: the argument undergoes a directed change, has its existence at issue, or is not the immediate cause.

The verdicts of chapter 4

theorem LevinRappaportHovav1995.internallyCaused_unergative : Unergative { immediateCause := true, directedChange := false, existence := false }

An internally caused verb whose argument neither undergoes a directed change nor has its existence at issue is unergative (§4.1.1): the agentive monadic verbs, verbs such as cough and tremble, the verbs of emission (§4.1.1.1) and the verbs of spatial configuration in their maintain position sense (§4.1.1.2).

theorem LevinRappaportHovav1995.directedChange_unaccusative (ic ex : Bool) : Unaccusative { immediateCause := ic, directedChange := true, existence := ex }

A verb of directed change is unaccusative whatever its causation: the externally caused verbs of change of state (§4.1.2), the internally caused ones (§4.2.1), the verbs of inherently directed motion (§4.2.2) and the assume position sense (§4.2.3).

theorem LevinRappaportHovav1995.existence_unaccusative (ic dc : Bool) : Unaccusative { immediateCause := ic, directedChange := dc, existence := true }

A verb whose argument's existence is at issue is unaccusative whatever its causation (§4.1.3, §4.2.4): verbs of existence, appearance and disappearance.

theorem LevinRappaportHovav1995.default_unaccusative : Unaccusative { immediateCause := false, directedChange := false, existence := false }

The roll verbs used nonagentively fall under the Default rule alone and are unaccusative (§4.1.4).

Appendix A: the classes of Levin 1993

def LevinRappaportHovav1995.characterizations : ArgumentStructure.LevinClass → List Characterization

Appendix A's assignment of [Lev93]'s intransitive classes to the book's semantic classes, one characterization per construal the book discusses: the verbs of emission are internally caused (§4.1.1.1); the verbs of inherently directed motion undergo a directed change, agentively or not (§4.2.2); the roll verbs are externally caused with no directed change, and internally caused when agentive (§4.1.4, §4.2.2); the run verbs are internally caused (§4.1.4); the verbs of existence, appearance, occurrence and disappearance have their argument's existence at issue, agentively or not (§4.1.3, §4.2.4); the verbs of spatial configuration assert existence in their simple position sense, are internally caused in their maintain position sense and add a directed change in their assume position sense (§4.1.1.2, §4.2.3); the verbs of change of state undergo a directed change, externally caused for the break, bend, cooking and other alternating verbs and internally caused for the entity-specific ones (§4.1.2, §4.2.1).

Equations

• One or more equations did not get rendered due to their size.
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.lightEmission = [{ immediateCause := true, directedChange := false, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.soundEmission = [{ immediateCause := true, directedChange := false, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.smellEmission = [{ immediateCause := true, directedChange := false, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.substanceEmission = [{ immediateCause := true, directedChange := false, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.run = [{ immediateCause := true, directedChange := false, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.break_ = [{ immediateCause := false, directedChange := true, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.bend = [{ immediateCause := false, directedChange := true, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.cooking = [{ immediateCause := false, directedChange := true, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.otherChangeOfState = [{ immediateCause := false, directedChange := true, existence := false }]
• LevinRappaportHovav1995.characterizations ArgumentStructure.LevinClass.entitySpecificChangeOfState = [{ immediateCause := true, directedChange := true, existence := false }]
• LevinRappaportHovav1995.characterizations x✝ = []

theorem LevinRappaportHovav1995.emission_unergative (c : ArgumentStructure.LevinClass) : c ∈ [ArgumentStructure.LevinClass.lightEmission, ArgumentStructure.LevinClass.soundEmission, ArgumentStructure.LevinClass.smellEmission, ArgumentStructure.LevinClass.substanceEmission] → ∀ ch ∈ characterizations c, Unergative ch

Verbs of emission are unergative (§4.1.1.1).

theorem LevinRappaportHovav1995.changeOfState_unaccusative (c : ArgumentStructure.LevinClass) : c ∈ [ArgumentStructure.LevinClass.break_, ArgumentStructure.LevinClass.bend, ArgumentStructure.LevinClass.cooking, ArgumentStructure.LevinClass.otherChangeOfState, ArgumentStructure.LevinClass.entitySpecificChangeOfState] → ∀ ch ∈ characterizations c, Unaccusative ch

Verbs of change of state are unaccusative, externally or internally caused (§4.1.2, §4.2.1).

theorem LevinRappaportHovav1995.directedMotion_unaccusative (ch : Characterization) : ch ∈ characterizations ArgumentStructure.LevinClass.inherentlyDirectedMotion → Unaccusative ch

Verbs of inherently directed motion are unaccusative whether used agentively or not (§4.2.2).

theorem LevinRappaportHovav1995.existence_classes_unaccusative (c : ArgumentStructure.LevinClass) : c ∈ [ArgumentStructure.LevinClass.exist, ArgumentStructure.LevinClass.appear, ArgumentStructure.LevinClass.occurrence, ArgumentStructure.LevinClass.disappearance] → ∀ ch ∈ characterizations c, Unaccusative ch

Verbs of existence, appearance, occurrence and disappearance are unaccusative whether used agentively or not (§4.1.3, §4.2.4).

theorem LevinRappaportHovav1995.run_unergative (ch : Characterization) : ch ∈ characterizations ArgumentStructure.LevinClass.run → Unergative ch

The run verbs are unergative (§4.1.4).

theorem LevinRappaportHovav1995.roll_variable : (∃ ch ∈ characterizations ArgumentStructure.LevinClass.roll, ch.immediateCause = false ∧ Unaccusative ch) ∧ ∃ ch ∈ characterizations ArgumentStructure.LevinClass.roll, ch.immediateCause = true ∧ Unergative ch

The roll verbs are unaccusative when nonagentive and unergative when agentive (§4.1.4, §4.2.2).

theorem LevinRappaportHovav1995.spatialConfiguration_variable : (∃ ch ∈ characterizations ArgumentStructure.LevinClass.spatialConfiguration, ch.existence = true ∧ Unaccusative ch) ∧ (∃ ch ∈ characterizations ArgumentStructure.LevinClass.spatialConfiguration, ch.directedChange = true ∧ Unaccusative ch) ∧ ∃ ch ∈ characterizations ArgumentStructure.LevinClass.spatialConfiguration, ch.immediateCause = true ∧ ch.directedChange = false ∧ Unergative ch

Verbs of spatial configuration are unaccusative in their simple and assume position senses and unergative in their maintain position sense (§4.1.1.2, §4.2.3).

The diagnostics

def LevinRappaportHovav1995.diagnosticOf (ex : Datum) : Option Bool

The unaccusative diagnostics the data rows apply, by what acceptability indicates: the unergative resultative pattern, the X's way construction and a cognate object indicate an unergative verb, the unaccusative resultative pattern an unaccusative one (§4.1.1, §4.1.2, §4.1.4). Locative inversion and there-insertion rows are data, not diagnostics: chapter 6 finds unergative verbs in locative inversion too.

Equations

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

def LevinRappaportHovav1995.classOf (ex : Datum) : Option ArgumentStructure.LevinClass

The class of a row's verb, by the book's section number.

Equations

• LevinRappaportHovav1995.classOf ex = (ex.feature? "class").bind ArgumentStructure.LevinClass.ofNumberString?

def LevinRappaportHovav1995.construalOf (ex : Datum) : List Characterization

The construal of a row's verb: its characterization in the class with the row's agentivity.

Equations

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

theorem LevinRappaportHovav1995.diagnostics_agree (ex : Datum) : ex ∈ Examples.all → ∀ unerg ∈ diagnosticOf ex, ∀ ch ∈ construalOf ex, ex.judgment = Judgment.acceptable ↔ if unerg = true then Unergative ch else Unaccusative ch

Every diagnostic row is acceptable exactly when the verb's construal has the status the diagnostic indicates.