Beavers (2010): The Structure of Lexical Meaning

This file formalizes Beavers's account of object/oblique alternations. The direct realization of an alternating argument carries monotonically stronger lexical entailments than its oblique realization, rather than a different event structure. In the conative and locative alternations the entailments are the degrees of affectedness, each an existential weakening of the next, so that of the eight sets of the three affectedness entailments only four are contentful, and they form a chain. The Morphosyntactic Alignment Principle requires the oblique to bear the minimally weaker role, which on the chain is weak covering. Every attested contrast satisfies it, the three conatives together realize each covering pair, and reversed and level-skipping alternations violate it. Total traversal of a path is the same entailment as quantized change, read of the scale rather than the theme, and adding it to the entailments of patienthood gives five contentful roles, among which climb the stairs and climb up the stairs are a minimal contrast. The same principle runs on the chain of arrival and possession behind the dative alternation.

Implementation notes

• A role is a set of entailments. The contentful sets of affectedness entailments are the lower sets, which correspond to the degrees by Birkhoff's representation, so a contrast records the degrees of the alternating participant in its two realizations.
• The entailments are stated over a result relation relative to a world. Potential for change is modal ((38)), and it is an existential generalization of nonquantized change only when the actual world is among the worlds the modality ranges over, which the paper assumes and the file takes as a hypothesis. Beavers leaves the modal base open.
• The paper defines the degrees of traversal (85) by the formulas of the degrees of affectedness, abstracting over the scale instead of the theme, so the file states each formula once. Only total traversal enters the roles of (86), and naming a role of (87) by its strongest entailment rules out affected paths, as the paper assumes.
• The paper states its conditions of a sentence with the theme, scale and event given; the file states them of a relation, over all themes, scales and events. A predicate-supplied goal is fixed across the predicate's events, so the end of the path in (84a) is read as the endpoint of the goal type.
• Beavers's rough correspondence between Dowty's proto-patient entailments and his own (Table 5) is not formalized, since it marks two of its cells as uncertain.

TODO

• Derive the contrasts from the example rows of Data.Examples.Beavers2010 rather than typing the verbs and degrees in.

References

• J. Beavers, The structure of lexical meaning: Why semantics really matters (2010)
• J. Beavers, On Affectedness (2011)
• B. Levin, English Verb Classes and Alternations: A Preliminary Investigation (1993)

L-thematic roles as sets of entailments ((65)–(67))

An L-thematic role is a set of lexical entailments. The three affectedness entailments of (65) entail one another, so a set of them is contentful exactly when it is closed under entailment, and the contentful sets are the degrees of affectedness (AffectednessDegree.entailments).

The entailments ((31), (38))

The result relation R w x s g e says that in the world w the theme x ends the event e at the goal g on the scale s, and w₀ is the actual world.

def Beavers2010.Quantized {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} (w₀ : W) (R : W → α → S → G → β → Prop) (φ : α → S → β → Prop) (g : G) : Prop

A predicate entails a quantized change to the goal g when its theme ends every event of it at g on its scale ((31a)). Of the scale, the same condition says it is totally traversed ((85a)).

Equations

• Beavers2010.Quantized w₀ R φ g = ∀ (x : α) (s : S) (e : β), φ x s e → R w₀ x s g e

def Beavers2010.Nonquantized {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} (w₀ : W) (R : W → α → S → G → β → Prop) (φ : α → S → β → Prop) : Prop

A predicate entails a nonquantized change when its theme ends every event of it at some goal on its scale ((31b)). Of the scale, the same condition says it is traversed ((85b)).

Equations

• Beavers2010.Nonquantized w₀ R φ = ∀ (x : α) (s : S) (e : β), φ x s e → ∃ (g : G), R w₀ x s g e

def Beavers2010.Potential {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} (acc : W → W → Prop) (w₀ : W) (R : W → α → S → G → β → Prop) (φ : α → S → β → Prop) : Prop

A predicate gives its theme potential for change when in every event of it the theme ends at some goal on its scale in some world accessible from the actual one ((38a)). Of the scale, the same condition says it is potentially traversed ((85c)).

Equations

• Beavers2010.Potential acc w₀ R φ = ∀ (x : α) (s : S) (e : β), φ x s e → ∃ (w : W), acc w₀ w ∧ ∃ (g : G), R w x s g e

theorem Beavers2010.Quantized.nonquantized {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} {w₀ : W} {R : W → α → S → G → β → Prop} {φ : α → S → β → Prop} {g : G} (h : Quantized w₀ R φ g) : Nonquantized w₀ R φ

theorem Beavers2010.Nonquantized.potential {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} {acc : W → W → Prop} {w₀ : W} {R : W → α → S → G → β → Prop} {φ : α → S → β → Prop} (hacc : acc w₀ w₀) (h : Nonquantized w₀ R φ) : Potential acc w₀ R φ

A nonquantized change entails potential for change when the actual world is among the worlds the modality ranges over, (38a) being the existential generalization of (31b) over worlds.

def Beavers2010.Holds {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} (acc : W → W → Prop) (w₀ : W) (R : W → α → S → G → β → Prop) (φ : α → S → β → Prop) : ArgumentStructure.AffectednessDegree → Prop

The condition each degree of affectedness names for a predicate ((31), (38)).

Equations

• Beavers2010.Holds acc w₀ R φ ArgumentStructure.AffectednessDegree.unspecified = True
• Beavers2010.Holds acc w₀ R φ ArgumentStructure.AffectednessDegree.potential = Beavers2010.Potential acc w₀ R φ
• Beavers2010.Holds acc w₀ R φ ArgumentStructure.AffectednessDegree.nonquantized = Beavers2010.Nonquantized w₀ R φ
• Beavers2010.Holds acc w₀ R φ ArgumentStructure.AffectednessDegree.quantized = ∃ (g : G), Beavers2010.Quantized w₀ R φ g

theorem Beavers2010.holds_antitone {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} {acc : W → W → Prop} {w₀ : W} {R : W → α → S → G → β → Prop} {φ : α → S → β → Prop} (hacc : acc w₀ w₀) : Antitone (Holds acc w₀ R φ)

Each degree entails every weaker one, given that the actual world is among the worlds the modality ranges over.

def Beavers2010.role {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} (acc : W → W → Prop) (w₀ : W) (R : W → α → S → G → β → Prop) (φ : α → S → β → Prop) : Set ArgumentStructure.AffectednessEntailment

The role a predicate assigns its theme is the set of affectedness entailments it has ((65)).

Equations

• Beavers2010.role acc w₀ R φ = {e : ArgumentStructure.AffectednessEntailment | Beavers2010.Holds acc w₀ R φ ↑e}

theorem Beavers2010.isLowerSet_role {W : Type u_1} {α : Type u_2} {S : Type u_3} {G : Type u_4} {β : Type u_5} {acc : W → W → Prop} {w₀ : W} {R : W → α → S → G → β → Prop} {φ : α → S → β → Prop} (hacc : acc w₀ w₀) : IsLowerSet (role acc w₀ R φ)

Every predicate's role is contentful, closed under entailment ((67)), given that the actual world is among the worlds the modality ranges over.

The MAP ((68)–(69)) as weak covering

@[instance_reducible]

instance Beavers2010.instDecidableRelAffectednessDegreeWCovBy_studies : DecidableRel fun (x1 x2 : ArgumentStructure.AffectednessDegree) => x1 ⩿ x2

Equations

• Beavers2010.instDecidableRelAffectednessDegreeWCovBy_studies a b = decidable_of_iff (a ≤ b ∧ ∀ (c : ArgumentStructure.AffectednessDegree), a < c → ¬c < b) ⋯

@[instance_reducible]

instance Beavers2010.instDecidableRelAffectednessDegreeCovBy_studies : DecidableRel fun (x1 x2 : ArgumentStructure.AffectednessDegree) => x1 ⋖ x2

Equations

• Beavers2010.instDecidableRelAffectednessDegreeCovBy_studies a b = decidable_of_iff (a < b ∧ ∀ (c : ArgumentStructure.AffectednessDegree), a < c → ¬c < b) ⋯

def Beavers2010.MAP {ρ : Type u_1} [Preorder ρ] (direct oblique : ρ) : Prop

The Morphosyntactic Alignment Principle (69) holds of the roles of an alternating participant's direct and oblique realizations on a hierarchy of roles when the oblique role is minimally weaker, weakly covered by the direct one ((68)).

Equations

• Beavers2010.MAP direct oblique = (oblique ⩿ direct)

@[instance_reducible]

instance Beavers2010.instDecidableMAPOfDecidableRelWCovBy {ρ : Type u_1} [Preorder ρ] [DecidableRel fun (x1 x2 : ρ) => x1 ⩿ x2] (d o : ρ) : Decidable (MAP d o)

Equations

• Beavers2010.instDecidableMAPOfDecidableRelWCovBy d o = id inferInstance

theorem Beavers2010.entailments_wcovBy_entailments_iff (d d' : ArgumentStructure.AffectednessDegree) : ArgumentStructure.AffectednessDegree.entailments d ⩿ ArgumentStructure.AffectednessDegree.entailments d' ↔ d ⩿ d'

Minimal contrast of the roles of (66) is weak covering of their degrees.

theorem Beavers2010.MAP.oblique_le {ρ : Type u_1} [Preorder ρ] {d o : ρ} (h : MAP d o) : o ≤ d

Under the MAP the oblique degree is at most the direct one, so the oblique's entailments are among the direct realization's (27).

The attested contrasts (Tables 3–4, (75))

structure Beavers2010.AlternationContrast : Type

An alternation contrast records a verb and the affectedness degrees of its alternating participant as direct object and as oblique.

• verb : String

  The verb.

• alternationType : ArgumentStructure.DiathesisAlternation

  The alternation it instantiates.

• directDegree : ArgumentStructure.AffectednessDegree

  Degree in direct realization.

• obliqueDegree : ArgumentStructure.AffectednessDegree

  Degree in oblique realization.

def Beavers2010.instReprAlternationContrast.repr : AlternationContrast → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Beavers2010.instReprAlternationContrast : Repr AlternationContrast

Equations

• Beavers2010.instReprAlternationContrast = { reprPrec := Beavers2010.instReprAlternationContrast.repr }

@[instance_reducible]

instance Beavers2010.instDecidableEqAlternationContrast : DecidableEq AlternationContrast

Equations

• Beavers2010.instDecidableEqAlternationContrast = Beavers2010.instDecidableEqAlternationContrast.decEq

def Beavers2010.instDecidableEqAlternationContrast.decEq (x✝ x✝¹ : AlternationContrast) : Decidable (x✝ = x✝¹)

Equations

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

def Beavers2010.eatConative : AlternationContrast

Ate her cake against ate at her cake (21) contrasts quantized with non-quantized change.

Equations

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

def Beavers2010.cutConative : AlternationContrast

Cut the rope against cut at the rope (20) contrasts non-quantized change with potential for change.

Equations

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

def Beavers2010.hitConative : AlternationContrast

Hit Defarge against hit at Defarge (22) contrasts potential for change with no entailment about change.

Equations

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

def Beavers2010.loadLocation : AlternationContrast

In loaded the wagon (with hay) (49) the location is completely filled as object and partly as oblique.

Equations

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

def Beavers2010.loadTheme : AlternationContrast

In loaded the hay (onto the wagon) (49) the theme is all moved as object and partly as oblique.

Equations

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

def Beavers2010.cutLocation : AlternationContrast

In cut the window (with the diamond) (54) the location is damaged as object and potentially damaged as oblique.

Equations

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

def Beavers2010.cutTheme : AlternationContrast

Cut the diamond (on the window) (54) shows the same contrast for the theme.

Equations

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

def Beavers2010.hitLocative : AlternationContrast

In hit the fence with the stick against hit the stick against the fence ((24), (75)) both realizations have potential for change, the equal-role alternation the MAP permits with no truth-conditional contrast.

Equations

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

def Beavers2010.allContrasts : List AlternationContrast

The attested contrasts.

Equations

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

def Beavers2010.MapHolds (c : AlternationContrast) : Prop

The MAP holds of a contrast.

Equations

• Beavers2010.MapHolds c = Beavers2010.MAP c.directDegree c.obliqueDegree

@[instance_reducible]

instance Beavers2010.instDecidableMapHolds (c : AlternationContrast) : Decidable (MapHolds c)

Equations

• Beavers2010.instDecidableMapHolds c = id inferInstance

theorem Beavers2010.MAP_holds_all_alternations (c : AlternationContrast) : c ∈ allContrasts → MapHolds c

The MAP holds of every attested contrast, each oblique realization being a minimal weakening of its direct counterpart or, as in (75), the same role.

theorem Beavers2010.MapHolds.oblique_le {c : AlternationContrast} (h : MapHolds c) : c.obliqueDegree ≤ c.directDegree

Under the MAP the direct degree dominates the oblique one.

theorem Beavers2010.conatives_witness_all_covers (q r : ArgumentStructure.AffectednessDegree) : q ⋖ r ↔ ∃ c ∈ [eatConative, cutConative, hitConative], c.directDegree = r ∧ c.obliqueDegree = q

The three conatives realize exactly the covering pairs of the affectedness hierarchy, together tiling the chain (Table 3).

Impossible alternations ((76)–(77))

def Beavers2010.reversedConative : AlternationContrast

In a reversed contrast (76) the oblique strictly outranks the direct realization.

Equations

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

def Beavers2010.skippingLocative : AlternationContrast

A level-skipping contrast (77) has a quantized direct and a potential oblique realization.

Equations

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

theorem Beavers2010.reversed_violates_MAP : ¬MapHolds reversedConative

theorem Beavers2010.skipping_violates_MAP : ¬MapHolds skippingLocative ∧ skippingLocative.obliqueDegree ≤ skippingLocative.directDegree

Skipping a level violates the MAP even though the degree order is respected, since ⊆_M demands the next-weakest role, not any weaker one.

Total traversal ((84)–(87))

@[reducible, inline]

abbrev Beavers2010.Role : Type

A role of (87) is named by its strongest entailment ((66)), an affectedness entailment or total traversal of a path ((86d)), which is incomparable with the affectedness entailments, and ⊥ is the empty role. A role with both kinds would be an affected path, which (87) rules out.

Equations

• Beavers2010.Role = WithBot (ArgumentStructure.AffectednessEntailment ⊕ Unit)

def Beavers2010.Role.totallyTraversed : Role

{totally traversed}.

Equations

• Beavers2010.Role.totallyTraversed = ↑(Sum.inr ())

theorem Beavers2010.climb_map : MAP Role.totallyTraversed ⊥

Climbed the stairs against climbed up the stairs ((81)–(84)) contrasts a totally traversed path with one of which nothing is entailed on (86). The empty role is covered by total traversal on (87), a minimal contrast, as the MAP (69) requires.

The dative chain (90)

inductive Beavers2010.DativeRole : Type

The roles of the dative chain (90) are being arrived at and being arrived into the possession of.

• goal : DativeRole

  A goal is arrived at.

• recipientGoal : DativeRole

  A recipient-goal is arrived into the possession of.

@[instance_reducible]

instance Beavers2010.instDecidableEqDativeRole : DecidableEq DativeRole

Equations

• Beavers2010.instDecidableEqDativeRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Beavers2010.instFintypeDativeRole : Fintype DativeRole

Equations

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

@[instance_reducible]

instance Beavers2010.instReprDativeRole : Repr DativeRole

Equations

• Beavers2010.instReprDativeRole = { reprPrec := Beavers2010.instReprDativeRole.repr }

def Beavers2010.instReprDativeRole.repr : DativeRole → ℕ → Std.Format

Equations

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

def Beavers2010.DativeRole.strength : DativeRole → ℕ

Strength on the dative chain.

Equations

• Beavers2010.DativeRole.goal.strength = 0
• Beavers2010.DativeRole.recipientGoal.strength = 1

@[instance_reducible]

instance Beavers2010.instLinearOrderDativeRole : LinearOrder DativeRole

Equations

• Beavers2010.instLinearOrderDativeRole = LinearOrder.lift' Beavers2010.DativeRole.strength ⋯

@[instance_reducible]

instance Beavers2010.instDecidableRelDativeRoleWCovBy : DecidableRel fun (x1 x2 : DativeRole) => x1 ⩿ x2

Equations

• Beavers2010.instDecidableRelDativeRoleWCovBy a b = decidable_of_iff (a ≤ b ∧ ∀ (c : Beavers2010.DativeRole), a < c → ¬c < b) ⋯

theorem Beavers2010.dative_map : MAP DativeRole.recipientGoal DativeRole.goal

In mailed Mary the letter against mailed the letter to Mary ((88)–(89)) the indirect object adds prospective possession to arrival, the MAP on the possession chain.

Bridge to [Lev93]'s judgment rows

theorem Beavers2010.conative_data_attested : Levin1993.Examples.con_cut.judgment = Judgment.acceptable ∧ Levin1993.Examples.con_hit.judgment = Judgment.acceptable

The conative alternation is attested for cut and hit (Table 3).

theorem Beavers2010.break_no_conative : Levin1993.Examples.con_break.judgment = Judgment.ungrammatical

Break does not take the conative, since its object's quantized change is inherent to the verb's meaning and the weakening is blocked.

theorem Beavers2010.locative_data_attested : Levin1993.Examples.loc_spray.judgment = Judgment.acceptable ∧ Levin1993.Examples.loc_load.judgment = Judgment.acceptable

The locative alternation is attested for spray/load verbs (Table 4).