Reciprocal verb entries

A reciprocal verb expresses mutual action without a reciprocal anaphor, as intransitive kiss, Hebrew hitnašek and French s'embrasser do. An entry records the verb, the locus where reciprocalization formed it, which is Reinhart and Siloni's lexicon-syntax parameter, and its transitive alternate when the vocabulary has one; frozen entries such as Hebrew hitgošeš 'wrestle' lack one. The subject profile bundled from the base's grid is the union of the base's two entailment profiles, Reinhart and Siloni's role bundling.

References

• [RS05]
• [Sil08]
• [Sil12]

structure Verb.Reciprocal : Type

A reciprocal verb entry, with the intransitive verb, its formation locus, and its transitive alternate when one exists in the vocabulary.

• verb : Verb
• formation : Reciprocal.Formation

  Where reciprocalization applied (the lex-syn parameter).

• base : Option Verb

  The transitive alternate; none for frozen entries.

@[instance_reducible]

instance Verb.instBEqReciprocal : BEq Reciprocal

Equations

• Verb.instBEqReciprocal = { beq := Verb.instBEqReciprocal.beq }

def Verb.instBEqReciprocal.beq : Reciprocal → Reciprocal → Bool

Equations

• Verb.instBEqReciprocal.beq { verb := a, formation := a_1, base := a_2 } { verb := b, formation := b_1, base := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Verb.instBEqReciprocal.beq x✝¹ x✝ = false

def Verb.Reciprocal.IsFrozen (v : Reciprocal) : Prop

A frozen entry has no transitive alternate in the vocabulary.

Equations

• v.IsFrozen = (v.base = none)

@[instance_reducible]

instance Verb.Reciprocal.instDecidablePredIsFrozen : DecidablePred IsFrozen

Equations

• v.instDecidablePredIsFrozen = decidable_of_iff (v.base.isNone = true) ⋯

def Verb.Reciprocal.bundledSubjectProfile (v : Reciprocal) : Option ArgumentStructure.EntailmentProfile

The subject profile bundled from the base's grid, the union of the base's subject and object entailments, none when the entry is frozen or the base's grid is unannotated.

Equations

• v.bundledSubjectProfile = do let b ← v.base let __do_lift ← b.subjectEntailments let __do_lift_1 ← b.objectEntailments pure (__do_lift ∪ __do_lift_1)

theorem Verb.Reciprocal.bundledSubjectProfile_eq {v : Reciprocal} {b : Verb} {ps po : ArgumentStructure.EntailmentProfile} (hb : v.base = some b) (hs : b.subjectEntailments = some ps) (ho : b.objectEntailments = some po) : v.bundledSubjectProfile = some (ps ∪ po)

theorem Verb.Reciprocal.bundledSubjectProfile_isComplexRole {v : Reciprocal} {b : Verb} {ps po : ArgumentStructure.EntailmentProfile} (hb : v.base = some b) (hs : b.subjectEntailments = some ps) (ho : b.objectEntailments = some po) (ha : ps.protoAgent.Nonempty) (hp : po.protoPatient.Nonempty) : ∃ (prof : ArgumentStructure.EntailmentProfile), v.bundledSubjectProfile = some prof ∧ prof.IsComplexRole

The bundled subject role of an entry whose base has an agentive subject and an affected object is a complex role.