Documentation

Linglib.Theories.Semantics.ArgumentStructure.Defs

Thematic Roles — type definitions #

Neo-Davidsonian thematic roles as two-place predicates relating entities to events. This file is the Defs partner to LF.lean: pure type/structure declarations and the Fragment ↔ Theory bridge.

Main definitions #

References #

source
@[reducible, inline]
abbrev Semantics.ArgumentStructure.ThematicRel (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] :
Type (max u_1 u_2)

A thematic relation: a two-place predicate relating an entity to an event. The core neo-Davidsonian type. Agent(j, e) means "j is the agent of event e".

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Semantics.ArgumentStructure.EventRel (Time : Type u_1) (α : Type u_2) [LinearOrder Time] :
    Type (max u_2 u_1)

    A relation between an event and an argument of arbitrary sort. Generalizes ThematicRel past the entity-first restriction: arguments may be propositions, questions, performances, content individuals, or any other ontological category. The argument order is event-first (vs. ThematicRel's entity-first), reflecting the neo-Davidsonian convention for thematic roles vs. the more general event-relation pattern used by content/reenactment relations (@cite{rudin-2025b}, §4.4–4.7).

    Equations
    Instances For
      source
      structure Semantics.ArgumentStructure.ThematicFrame (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] :
      Type (max u_1 u_2)

      A thematic frame bundles thematic relations for a given model.

      Note: holder is a Theory-level role distinct from agent — it selects for states, not actions. The Fragment-layer ThetaRole enum does not include holder since VendlerClass already encodes dynamicity.

      • agent : ThematicRel Entity Time

        Agent: volitional causer

      • patient : ThematicRel Entity Time

        Patient: affected entity

      • theme : ThematicRel Entity Time

        Theme: entity in a state/location

      • experiencer : ThematicRel Entity Time

        Experiencer: perceiver/cognizer

      • goal : ThematicRel Entity Time

        Goal: recipient/target

      • source : ThematicRel Entity Time

        Source: origin

      • instrument : ThematicRel Entity Time

        Instrument: means

      • stimulus : ThematicRel Entity Time

        Stimulus: cause of experience

      • holder : ThematicRel Entity Time

        Holder: entity in a state. Distinct from Agent: selects for states, not actions.

      Instances For
        source
        def Semantics.ArgumentStructure.ThetaRole.toRel {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (θ : ThetaRole) (frame : ThematicFrame Entity Time) :
        ThematicRel Entity Time

        Map the Fragment-layer ThetaRole enum to the corresponding ThematicFrame field. Bridges lexical annotations to semantic content.

        Equations
        Instances For