Documentation

Linglib.Semantics.ArgumentStructure.EventStructure.Basic

Event structure templates #

An event structure template is a term over a small set of primitive predicates: a state, an action ACT, a change BECOME and causation CAUSE, where BECOME and CAUSE take templates as arguments and so build larger templates out of smaller ones ([RHL98]; [BKG20]). A verb's meaning pairs a template, which fixes its class, with a root, which tells it apart from the other members of the class. The basic inventory of [RHL98] is the state [x ⟨STATE⟩], the activity [x ACT⟨MANNER⟩], the achievement [BECOME [x ⟨STATE⟩]] and the two accomplishments [[x ACT⟨MANNER⟩] CAUSE [BECOME [y ⟨STATE⟩]]] and [x CAUSE [BECOME [y ⟨STATE⟩]]], the second with an individual causer, which is the vcause of [BKG20].

Templates are sorted like the domain of an Interpretation: BECOME turns a state template into an event template and CAUSE relates two event templates. Template.denote interprets a template with a root in its slots, the root's state predicate at the state and its manner at ACT, through the heads vBecome and vCause. The primitives are the four kinds of entailment of the root typology of [BKG20], so Template.kinds reads a template's primitives as a root signature, and membership in it is exactly what every denotation of the template entails: a change for HasResultState, a causal relation for HasCause. A template's denotation entails that each of its subterms is realized, which orders the readings of a modifier such as again attached at different subterms.

Main definitions #

Main results #

Implementation notes #

A template relates two participants, the actor y, which is the effector of an action and of a causing subevent, and the undergoer x, of which the state holds. The caused subevent of CAUSE is predicated of the undergoer, which is its actor when the caused subevent is itself an action or a causation. An individual causer is the leaf effector, an eventuality with the actor as its effector and no further content, so that CAUSE always relates two subevents. A root has one manner, which every ACT of the template carries. The carriers of the two sorts share a universe, so that the type of a denotation can depend on the sort.

References #

source
inductive ArgumentStructure.EventStructure.Eventuality :
Type

The two sorts of eventuality a template describes.

Instances For
    source
    @[instance_reducible]
    instance ArgumentStructure.EventStructure.instDecidableEqEventuality :
    DecidableEq Eventuality
    Equations
    source
    def ArgumentStructure.EventStructure.instReprEventuality.repr :
    Eventuality → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance ArgumentStructure.EventStructure.instReprEventuality :
      Repr Eventuality
      Equations
      source
      @[reducible, inline]
      abbrev ArgumentStructure.EventStructure.Eventuality.Carrier (State Event : Type u) :
      Eventuality → Type u

      The carrier of a sort, the states or the events of an interpretation.

      Equations
      Instances For
        source
        instance ArgumentStructure.EventStructure.instNonemptyCarrier {State Event : Type u} [Nonempty State] [Nonempty Event] (σ : Eventuality) :
        Nonempty (Eventuality.Carrier State Event σ)
        source
        inductive ArgumentStructure.EventStructure.Template :
        Eventuality → Type

        An event structure template, a sorted term over the primitive predicates.

        Instances For
          source
          def ArgumentStructure.EventStructure.Template.achievement :
          Template Eventuality.event

          The achievement [BECOME [x ⟨STATE⟩]].

          Equations
          Instances For
            source
            def ArgumentStructure.EventStructure.Template.accomplishment :
            Template Eventuality.event

            The accomplishment [[x ACT⟨MANNER⟩] CAUSE [BECOME [y ⟨STATE⟩]]].

            Equations
            Instances For
              source
              def ArgumentStructure.EventStructure.Template.kinds {σ : Eventuality} :
              Template σ → Semantics.Root.Kinds

              The kinds of entailment a template's primitives contribute: a state, the manner of an action, the change of BECOME and the causation of CAUSE.

              Equations
              Instances For
                source
                def ArgumentStructure.EventStructure.Template.HasCause {σ : Eventuality} (t : Template σ) :
                Prop

                The template has CAUSE.

                Equations
                Instances For
                  source
                  def ArgumentStructure.EventStructure.Template.HasResultState {σ : Eventuality} (t : Template σ) :
                  Prop

                  The template has BECOME, and so a result state.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance ArgumentStructure.EventStructure.Template.instDecidableHasCause {σ : Eventuality} (t : Template σ) :
                    Decidable t.HasCause
                    Equations
                    source
                    @[instance_reducible]
                    instance ArgumentStructure.EventStructure.Template.instDecidableHasResultState {σ : Eventuality} (t : Template σ) :
                    Decidable t.HasResultState
                    Equations
                    source
                    def ArgumentStructure.EventStructure.Template.causing :
                    Template Eventuality.event → Option (Template Eventuality.event)

                    The causing subevent of a causative template.

                    Equations
                    Instances For
                      source
                      def ArgumentStructure.EventStructure.Template.caused :
                      Template Eventuality.event → Option (Template Eventuality.event)

                      The caused subevent of a causative template.

                      Equations
                      Instances For
                        source
                        inductive ArgumentStructure.EventStructure.Template.IsSubterm {α β : Eventuality} :
                        Template α → Template β → Prop

                        u occurs in t.

                        Instances For
                          source
                          theorem ArgumentStructure.EventStructure.Template.IsSubterm.kinds_subset {σ τ : Eventuality} {u : Template τ} {t : Template σ} (h : u.IsSubterm t) :
                          u.kinds ⊆ t.kinds

                          A subterm's primitives are among the template's.

                          Denotation #

                          source
                          def ArgumentStructure.EventStructure.Template.denote {Entity : Type u_1} {State Event : Type u} (M : Interpretation Entity State Event) (P : Entity → State → Prop) (Q : Event → Prop) {σ : Eventuality} :
                          Template σ → Entity → Entity → Eventuality.Carrier State Event σ → Prop

                          The denotation of a template in M, with a root's state predicate P at the state and its manner Q at ACT: a relation between the actor, the undergoer and an eventuality of the template's sort.

                          Equations
                          Instances For
                            source
                            theorem ArgumentStructure.EventStructure.Template.denote_cause_effector {Entity : Type u_1} {State Event : Type u} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {y x : Entity} {t : Template Eventuality.event} {v : Event} :
                            denote M P Q (effector.cause t) y x v ↔ M.vCause (denote M P Q t x x) y v

                            CAUSE with an individual causer is the head vCause over its caused subevent: an event whose effector is the causer.

                            source
                            theorem ArgumentStructure.EventStructure.Template.exists_denote_of_isSubterm {σ τ : Eventuality} {Entity : Type u_1} {State Event : Type u} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {y x : Entity} {u : Template τ} {t : Template σ} (hu : u.IsSubterm t) {v : Eventuality.Carrier State Event σ} (h : denote M P Q t y x v) :
                            ∃ (y' : Entity) (w : Eventuality.Carrier State Event τ), denote M P Q u y' x w

                            A template's denotation entails that each of its subterms is realized, with the same undergoer.

                            source
                            theorem ArgumentStructure.EventStructure.Template.exists_become_of_denote {σ : Eventuality} {Entity : Type u_1} {State Event : Type u} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {y x : Entity} {t : Template σ} (ht : t.HasResultState) {v : Eventuality.Carrier State Event σ} (h : denote M P Q t y x v) :
                            ∃ (s : State) (e : Event), M.become s e

                            A template with BECOME describes only eventualities that involve a change.

                            source
                            theorem ArgumentStructure.EventStructure.Template.exists_cause_of_denote {σ : Eventuality} {Entity : Type u_1} {State Event : Type u} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {y x : Entity} {t : Template σ} (ht : t.HasCause) {v : Eventuality.Carrier State Event σ} (h : denote M P Q t y x v) :
                            ∃ (v : Event) (e : Event), M.cause v e

                            A template with CAUSE describes only eventualities that involve a causal relation.

                            Completeness of the diagnostics #

                            source
                            theorem ArgumentStructure.EventStructure.Template.hasResultState_iff {σ : Eventuality} {Entity : Type u_1} {State Event : Type u} [Nonempty Entity] [Nonempty State] [Nonempty Event] {t : Template σ} :
                            t.HasResultState ↔ ∀ (M : Interpretation Entity State Event) (P : Entity → State → Prop) (Q : Event → Prop) (y x : Entity) (v : Eventuality.Carrier State Event σ), denote M P Q t y x v → ∃ (s : State) (e : Event), M.become s e

                            A template has BECOME iff every denotation of it, in every interpretation, involves a change.

                            source
                            theorem ArgumentStructure.EventStructure.Template.hasCause_iff {σ : Eventuality} {Entity : Type u_1} {State Event : Type u} [Nonempty Entity] [Nonempty State] [Nonempty Event] {t : Template σ} :
                            t.HasCause ↔ ∀ (M : Interpretation Entity State Event) (P : Entity → State → Prop) (Q : Event → Prop) (y x : Entity) (v : Eventuality.Carrier State Event σ), denote M P Q t y x v → ∃ (v : Event) (e : Event), M.cause v e

                            A template has CAUSE iff every denotation of it, in every interpretation, involves a causal relation.