Documentation

Linglib.Semantics.Definiteness.Description

Nominal Descriptions: Unified Sum Type #

[CB15] [PGG17] [Han21] [Mor21] [Sch09b] [Sch13] [Sha80] [Kri15b]

A single sum type Description E W covering the principal flavors of nominal description that the syntax–semantics interface needs to distinguish:

The whole type is parameterized by entity and index types E/W, so all restrictors, situation pronouns, and possessor expressions are typed via the unified Denot E W machinery rather than ad-hoc E → Bool predicates.

Design notes #

source
inductive Semantics.Definiteness.Description (E W : Type) :
Type

Principal flavors of nominal description — the definiteness/reference axis (bare/indefinite vs the definite subtypes), orthogonal to Features.BindingClass (binding distribution) and to a pronoun's lexical kind. The type parameters E/W supply the entity domain and index set so all subexpressions live in the same Denot E W universe.

Instances For
    source
    def Semantics.Definiteness.Description.isDefinite {E W : Type} :
    Description E W → Prop

    Is this a definite description (in the broad sense — uniqueness, familiarity, demonstrative, or possessive)?

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Definiteness.Description.instDecidablePredIsDefinite {E W : Type} :
      DecidablePred isDefinite
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Semantics.Definiteness.Description.isAnaphoric {E W : Type} :
      Description E W → Prop

      Does this description require a discourse antecedent? Anaphoric and demonstrative do; unique/possessive/bare/indefinite do not.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Definiteness.Description.instDecidablePredIsAnaphoric {E W : Type} :
        DecidablePred isAnaphoric
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Semantics.Definiteness.Description.usesSituationPronoun {E W : Type} :
        Description E W → Bool

        Does this description bind a structural situation pronoun? Coppock–Beaver uniqueness and demonstratives do (resource situation for maximality and deictic check); the other constructors do not.

        Equations
        Instances For
          source
          def Semantics.Definiteness.Description.expectedPresupType {E W : Type} :
          Description E W → Option Features.Definiteness.DefPresupType

          Map each Description flavor to the [Sch09b]–[Sch13] presupposition type it expresses, where applicable. Bare and indefinite return none because they are not (in themselves) definites.

          Equations
          Instances For
            source
            theorem Semantics.Definiteness.Description.isDefinite_iff_expectedPresup_some {E W : Type} (n : Description E W) :
            n.isDefinite ↔ n.expectedPresupType.isSome = true

            Definites are exactly those flavors with a non-none expected presupposition type. By construction.

            source
            theorem Semantics.Definiteness.Description.isAnaphoric_implies_familiarity {E W : Type} (n : Description E W) (h : n.isAnaphoric) :
            n.expectedPresupType = some Features.Definiteness.DefPresupType.familiarity

            Anaphoric flavors all carry the familiarity presupposition type.

            source
            def Semantics.Definiteness.Description.ofPresupType {E W : Type} (p : Features.Definiteness.DefPresupType) (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) :
            Description E W

            The definite description for a [Sch09b] presupposition type: the weak article (uniqueness) is unique, the strong article (familiarity) is anaphoric. A section of expectedPresupType over the two article strengths, so any item carrying a DefPresupType — a determiner, a definite, or (per [PGG17]) a personal/demonstrative pronoun — denotes by ofPresupType and recovers its strength via expectedPresupType.

            idx is the strong article's anaphoric/discourse index; for the weak article it fills the situation-pronoun slot, which interpret discards (interpret_unique_index_irrelevant).

            Equations
            Instances For
              source
              theorem Semantics.Definiteness.Description.expectedPresupType_ofPresupType {E W : Type} (p : Features.Definiteness.DefPresupType) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) :
              (ofPresupType p R idx).expectedPresupType = some p

              ofPresupType is a section of expectedPresupType: the strength round-trips.