Documentation

Linglib.Theories.Semantics.Dynamic.Boxes.Syntax

DRS Syntax: Discourse Representation Structures #

@cite{kamp-reyle-1993} @cite{muskens-1996}

Pure syntactic representation of DRS expressions with structural operations — no semantic imports, no interpretation.

Definitions #

Design #

This module is the pure-syntax layer of the four-layer dynamic semantics architecture:

DynProp.lean       ← semantic algebra (DRS S, dseq, test, ...)
DynamicTy2.lean    ← compositional layer (Dref, AssignmentStructure)
DRSExpr.lean       ← DRS syntax (this file)
Accessibility.lean ← interpretation bridge (DRSExpr → DRS)

DRSExpr has no dependency on the semantic algebra (DRS S) or compositional types (Dref, Assign). Interpretation is defined in Accessibility.lean via interp : DRSExpr → DRS (Assign E).

source
inductive Semantics.Dynamic.Core.DRSExpr.DRSExpr :
Type

Syntactic representation of DRS expressions.

Dref indices are natural numbers. Relation symbols are identified by natural number indices; their arity is implicit in the dref list.

  • atom (rel : Nat) (drefs : List Nat) : DRSExpr

    Atomic condition: relation R applied to drefs

  • is (u v : Nat) : DRSExpr

    Identity condition: u₁ is u₂

  • neg (K : DRSExpr) : DRSExpr

    Negation: not K

  • disj (K₁ K₂ : DRSExpr) : DRSExpr

    Disjunction: K₁ or K₂

  • impl (K₁ K₂ : DRSExpr) : DRSExpr

    Implication: K₁ ⇒ K₂

  • box (newDrefs : List Nat) (conds : List DRSExpr) : DRSExpr

    Box: [u₁,...,uₙ | γ₁,...,γₘ]

  • seq (K₁ K₂ : DRSExpr) : DRSExpr

    Sequencing: K₁ ; K₂

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Dynamic.Core.DRSExpr.instReprDRSExpr :
    Repr DRSExpr
    Equations
    source
    partial def Semantics.Dynamic.Core.DRSExpr.instReprDRSExpr.repr :
    DRSExpr → Nat → Std.Format
    source
    def Semantics.Dynamic.Core.DRSExpr.adr :
    DRSExpr → List Nat

    Active discourse referents: the drefs introduced by K.

    adr([u₁,...,uₙ | γ₁,...,γₘ]) = {u₁,...,uₙ} adr(K₁ ; K₂) = adr(K₁) ∪ adr(K₂)

    Conditions (atoms, negation, disjunction, implication) introduce no drefs.

    Equations
    Instances For
      source
      def Semantics.Dynamic.Core.DRSExpr.occurs (u : Nat) :
      DRSExpr → Bool

      Whether dref u occurs anywhere in expression K.

      Equations
      Instances For
        source
        def Semantics.Dynamic.Core.DRSExpr.occurs.occursAny (u : Nat) :
        List DRSExpr → Bool
        Equations
        Instances For
          source
          def Semantics.Dynamic.Core.DRSExpr.acc (u : Nat) :
          DRSExpr → List Nat

          Accessible drefs from an occurrence of u in K.

          Defined by structural recursion following @cite{muskens-1996} pp. 170–171:

          • Atomic: no drefs are accessible
          • Negation: accessibility passes through
          • Disjunction/implication: accessibility from the branch containing u, with antecedent drefs accessible in the consequent
          • Box: new drefs are accessible, plus accessibility from the condition containing u
          • Sequencing: drefs from K₁ are accessible in K₂
          Equations
          Instances For
            source
            def Semantics.Dynamic.Core.DRSExpr.acc.accFind (u : Nat) :
            List DRSExpr → Option (List Nat)

            Find the first condition containing u and return its accessible drefs.

            Equations
            Instances For
              source
              def Semantics.Dynamic.Core.DRSExpr.allOccurring :
              DRSExpr → List Nat

              Collect all dref indices mentioned anywhere in K.

              Equations
              Instances For
                source
                def Semantics.Dynamic.Core.DRSExpr.allOccurring.allOccurringList :
                List DRSExpr → List Nat
                Equations
                Instances For
                  source
                  def Semantics.Dynamic.Core.DRSExpr.isFree (u : Nat) (K : DRSExpr) :
                  Bool

                  A dref u is free in K if it occurs in K but is not among the drefs accessible from its position.

                  Equations
                  Instances For
                    source
                    def Semantics.Dynamic.Core.DRSExpr.isProper (K : DRSExpr) :
                    Bool

                    A DRS is proper if it contains no free referents (@cite{muskens-1996}, p. 171).

                    Equations
                    Instances For
                      source
                      def Semantics.Dynamic.Core.DRSExpr.exManAdoresWoman :
                      DRSExpr

                      "A man adores a woman" as a syntactic DRS.

                      [u₁ u₂ | man u₁, woman u₂, u₁ adores u₂]

                      Using relation indices: 0 = man, 1 = woman, 2 = adores.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Semantics.Dynamic.Core.DRSExpr.exDonkey :
                        DRSExpr

                        "If a farmer owns a donkey, he beats it" as a syntactic DRS.

                        [u₁ u₂ | farmer u₁, donkey u₂, u₁ owns u₂] ⇒ [| u₁ beats u₂]

                        Using relation indices: 0 = farmer, 1 = donkey, 2 = owns, 3 = beats.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Semantics.Dynamic.Core.DRSExpr.exFree :
                          DRSExpr

                          "He₁ stinks" (with no antecedent) is NOT proper: dref 1 is free.

                          Equations
                          Instances For