Proto-role attribution data schema

Typed schema for the per-argument proto-role entailment attributions that [Dow91] states explicitly in the text. Generated rows live in Data/ProtoRoles/<Paper>.lean, emitted from the canonical <Paper>.json by scripts/gen_protoroles.py.

This is substrate: it imports nothing from Linglib/. Consumers (the paper's study file, Studies/Dowty1991.lean) import the generated module and supply their own adapters to theory types such as ArgumentStructure.EntailmentProfile.

Each entailment field is Option Bool: some true/some false only where the paper explicitly attributes or denies the entailment for that argument; none where it is silent. Rows never interpolate — hedged attributions (e.g. [Dow91] p. 577's "(mostly)") stay none.

Main definitions

• ArgPosition — grammatical slot of the argument the attribution concerns.
• ProtoRoleDatum — one verb argument's attributed entailments plus a locator into the source text.

inductive Dowty1991.ArgPosition : Type

Grammatical slot of the attributed argument. nonsubject is for alternating argument pairs attributed jointly without a fixed frame ([Dow91] (64 I) on spray/load: "both nonsubject arguments").

• subject : ArgPosition
• object : ArgPosition
• oblique : ArgPosition
• nonsubject : ArgPosition

@[implicit_reducible]

instance Dowty1991.instDecidableEqArgPosition : DecidableEq ArgPosition

Equations

• Dowty1991.instDecidableEqArgPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dowty1991.instReprArgPosition.repr : ArgPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Dowty1991.instReprArgPosition : Repr ArgPosition

Equations

• Dowty1991.instReprArgPosition = { reprPrec := Dowty1991.instReprArgPosition.repr }

@[implicit_reducible]

instance Dowty1991.instInhabitedArgPosition : Inhabited ArgPosition

Equations

• Dowty1991.instInhabitedArgPosition = { default := Dowty1991.instInhabitedArgPosition.default }

structure Dowty1991.ProtoRoleDatum : Type

One explicit per-argument entailment attribution ([Dow91]). The ten fields follow the (27)/(28) proto-role lists: five Proto-Agent, five Proto-Patient. locator cites the example number and page.

• verb : String

  The attributing predicate, as named in the text.

• arg : ArgPosition

  Grammatical slot of the argument.

• argDesc : String

  Short gloss of the argument (e.g. "the fence (location)").

• volition : Option Bool

  (27a) volitional involvement.

• sentience : Option Bool

  (27b) sentience/perception.

• causation : Option Bool

  (27c) causing an event or change of state.

• movement : Option Bool

  (27d) movement relative to another participant.

• independentExistence : Option Bool

  (27e) exists independently of the event.

• changeOfState : Option Bool

  (28a) undergoes change of state.

• incrementalTheme : Option Bool

  (28b) incremental theme.

• causallyAffected : Option Bool

  (28c) causally affected by another participant.

• stationary : Option Bool

  (28d) stationary relative to another participant.

• dependentExistence : Option Bool

  (28e) does not exist independently of the event.

• locator : String

  Example number and page in the source text.

def Dowty1991.instDecidableEqProtoRoleDatum.decEq (x✝ x✝¹ : ProtoRoleDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Dowty1991.instDecidableEqProtoRoleDatum : DecidableEq ProtoRoleDatum

Equations

• Dowty1991.instDecidableEqProtoRoleDatum = Dowty1991.instDecidableEqProtoRoleDatum.decEq

def Dowty1991.instReprProtoRoleDatum.repr : ProtoRoleDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Dowty1991.instReprProtoRoleDatum : Repr ProtoRoleDatum

Equations

• Dowty1991.instReprProtoRoleDatum = { reprPrec := Dowty1991.instReprProtoRoleDatum.repr }