Reciprocal verb entries

A reciprocal verb expresses mutual action without a reciprocal anaphor — intransitive kiss, Hebrew hitnašek, French s'embrasser. An entry records the verb, the locus where reciprocalization formed it ([RS05]'s lex-syn parameter; [Sil08], [Sil12]), and its transitive alternate when the vocabulary has one — frozen entries (Hebrew hitgošeš 'wrestle') lack one. The subject profile bundled from the base's grid is the join of the base's two entailment profiles, [RS05]'s [θᵢ · θⱼ] role bundling.

structure Verb.Reciprocal : Type

A reciprocal verb entry: 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.

def Verb.instReprReciprocal.repr : Reciprocal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprReciprocal : Repr Reciprocal

Equations

• Verb.instReprReciprocal = { reprPrec := Verb.instReprReciprocal.repr }

@[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 join 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 : 0 < ps.pAgentScore) (hp : 0 < po.pPatientScore) : ∃ (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.