Documentation

Linglib.Core.Nominal.Description

Nominal Descriptions: Unified Sum Type #

@cite{coppock-beaver-2015} @cite{patel-grosz-grosz-2017} @cite{hanink-2021} @cite{bondarenko-2023} @cite{moroney-2021} @cite{schwarz-2009} @cite{schwarz-2013} @cite{sharvy-1980} @cite{kriz-2015}

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

The whole type is parameterized by a Core.Logic.Intensional.Frame, so all restrictors, situation pronouns, and possessor expressions are typed via the unified F.Denot machinery rather than ad-hoc E → Bool predicates.

Design notes #

source
inductive Core.Nominal.NominalKind (F : Logic.Intensional.Frame) :
Type

Principal flavors of nominal description. The frame parameter F supplies the entity domain and index set so all subexpressions live in the same F.Denot universe.

Instances For
    source
    def Core.Nominal.NominalKind.isDefinite {F : Logic.Intensional.Frame} :
    NominalKind F → Prop

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

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Core.Nominal.NominalKind.instDecidablePredIsDefinite {F : Logic.Intensional.Frame} :
      DecidablePred isDefinite
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Core.Nominal.NominalKind.isAnaphoric {F : Logic.Intensional.Frame} :
      NominalKind F → 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 Core.Nominal.NominalKind.instDecidablePredIsAnaphoric {F : Logic.Intensional.Frame} :
        DecidablePred isAnaphoric
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Core.Nominal.NominalKind.usesSituationPronoun {F : Logic.Intensional.Frame} :
        NominalKind F → 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 Core.Nominal.NominalKind.expectedPresupType {F : Logic.Intensional.Frame} :
          NominalKind F → Option Features.Definiteness.DefPresupType

          Map each NominalKind flavor to the @cite{schwarz-2009}–@cite{schwarz-2013} presupposition type it expresses, where applicable. Bare and indefinite return none because they are not (in themselves) definites.

          Equations
          Instances For
            source
            theorem Core.Nominal.NominalKind.isDefinite_iff_expectedPresup_some {F : Logic.Intensional.Frame} (n : NominalKind F) :
            n.isDefinite ↔ n.expectedPresupType.isSome = true

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

            source
            theorem Core.Nominal.NominalKind.isAnaphoric_implies_familiarity {F : Logic.Intensional.Frame} (n : NominalKind F) (h : n.isAnaphoric) :
            n.expectedPresupType = some Features.Definiteness.DefPresupType.familiarity

            Anaphoric flavors all carry the familiarity presupposition type.