Documentation

Linglib.Theories.Semantics.Events.ThematicRolesGrounding

Thematic Role Grounding #

Bridge theorems connecting Fragment-layer verb entries (kick, give,) to Theory-layer thematic role infrastructure. These verify that the theta role annotations in the lexicon correctly map to ThematicFrame fields via ThetaRole.toRel.

Separated from ThematicRoles.lean to keep the Theory layer free of Fragment imports (Theories → Fragments dependency discipline).

source
theorem Semantics.Events.ThematicRoles.Grounding.kick_subject_agent :
Fragments.English.Predicates.Verbal.kick.subjectTheta = some ThetaRole.agent

"kick" has agent as subject theta role.

source
theorem Semantics.Events.ThematicRoles.Grounding.kick_object_patient :
Fragments.English.Predicates.Verbal.kick.objectTheta = some ThetaRole.patient

"kick" has patient as object theta role.

source
theorem Semantics.Events.ThematicRoles.Grounding.give_roles :
Fragments.English.Predicates.Verbal.give.subjectTheta = some ThetaRole.agent ∧ Fragments.English.Predicates.Verbal.give.objectTheta = some ThetaRole.theme ∧ Fragments.English.Predicates.Verbal.give.object2Theta = some ThetaRole.goal

"give" has agent subject, theme direct object, goal indirect object.

source
theorem Semantics.Events.ThematicRoles.Grounding.see_roles :
Fragments.English.Predicates.Verbal.see.subjectTheta = some ThetaRole.experiencer ∧ Fragments.English.Predicates.Verbal.see.objectTheta = some ThetaRole.stimulus

"see" has experiencer subject and stimulus object.

source
theorem Semantics.Events.ThematicRoles.Grounding.subjectTheta_toRel_kick {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.kick.subjectTheta = some frame.agent

"kick"'s subject theta role maps to the agent relation in any frame.

source
theorem Semantics.Events.ThematicRoles.Grounding.objectTheta_toRel_kick {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.kick.objectTheta = some frame.patient

"kick"'s object theta role maps to the patient relation in any frame.

source
theorem Semantics.Events.ThematicRoles.Grounding.subjectTheta_toRel_give {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.give.subjectTheta = some frame.agent

"give"'s subject theta role maps to the agent relation.

source
theorem Semantics.Events.ThematicRoles.Grounding.objectTheta_toRel_give {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.give.objectTheta = some frame.theme

"give"'s object theta role maps to the theme relation.

source
theorem Semantics.Events.ThematicRoles.Grounding.object2Theta_toRel_give {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.give.object2Theta = some frame.goal

"give"'s indirect object theta role maps to the goal relation.

source
theorem Semantics.Events.ThematicRoles.Grounding.subjectTheta_toRel_see {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.see.subjectTheta = some frame.experiencer

"see"'s subject theta role maps to the experiencer relation.

source
theorem Semantics.Events.ThematicRoles.Grounding.objectTheta_toRel_see {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) :
Option.map (fun (x : ThetaRole) => ThetaRole.toRel x frame) Fragments.English.Predicates.Verbal.see.objectTheta = some frame.stimulus

"see"'s object theta role maps to the stimulus relation.

source
inductive Semantics.Events.ThematicRoles.Grounding.Person :
Type

A toy entity type for examples.

Instances For
    source
    instance Semantics.Events.ThematicRoles.Grounding.instDecidableEqPerson :
    DecidableEq Person
    Equations
    source
    def Semantics.Events.ThematicRoles.Grounding.instReprPerson.repr :
    Person → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Semantics.Events.ThematicRoles.Grounding.instReprPerson :
      Repr Person
      Equations
      source
      def Semantics.Events.ThematicRoles.Grounding.instBEqPerson.beq :
      Person → Person → Bool
      Equations
      Instances For
        source
        instance Semantics.Events.ThematicRoles.Grounding.instBEqPerson :
        BEq Person
        Equations
        source
        def Semantics.Events.ThematicRoles.Grounding.exampleFrame :
        ThematicFrame Person ℤ

        A toy thematic frame for the kicking example.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Events.ThematicRoles.Grounding.kickPred :
          EvPred ℤ

          A toy "kick" event predicate.

          Equations
          Instances For
            source
            theorem Semantics.Events.ThematicRoles.Grounding.john_kicked_mary :
            transitiveLogicalForm kickPred exampleFrame Person.john Person.mary

            "John kicked Mary" is true in the example model: ∃e. kick(e) ∧ Agent(john, e) ∧ Patient(mary, e).