Documentation

Linglib.Theories.Syntax.Minimalist.Polarity

Syntactic Polarity: PolP and [±Pol] #

@cite{holmberg-2016} @cite{laka-1990}

Syntactic polarity as a formal feature on the PolP functional head, connecting @cite{laka-1990}'s ΣP and @cite{holmberg-2016}'s analysis of yes/no answers.

Key Claims #

  1. Every finite clause has a polarity head (Pol⁰) projecting PolP in the IP domain
  2. In declaratives, [±Pol] is valued: [+Pol] for affirmative, [-Pol] for negative
  3. In polar questions, [±Pol] is unvalued — the answer values it
  4. "Yes"/"No" are focus-movement remnants of PolP ellipsis under identity

Connection to Features.Polarity #

Features.Polarity provides the semantic type (.positive / .negative). This file provides the syntactic feature [±Pol] that participates in Agree and maps to Features.Polarity at LF.

Connection to Cat.Pol #

Minimalist.Cat.Pol is the categorial label for the polarity head. This file adds the feature infrastructure for what that head carries.

source
inductive Minimalist.Polarity.PolFeature :
Type

The polarity feature on Pol⁰, which may be valued or unvalued.

In declaratives: valued [+Pol] or [-Pol] In polar questions: unvalued [uPol] — waiting for an answer to value it

  • valued : Features.Polarity → PolFeature

    Valued polarity: [+Pol] (affirmative) or [-Pol] (negative)

  • unvalued : PolFeature

    Unvalued polarity: the feature in polar questions that the answer resolves

Instances For
    source
    @[implicit_reducible]
    instance Minimalist.Polarity.instDecidableEqPolFeature :
    DecidableEq PolFeature
    Equations
    source
    def Minimalist.Polarity.instDecidableEqPolFeature.decEq (x✝ x✝¹ : PolFeature) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Minimalist.Polarity.instReprPolFeature :
      Repr PolFeature
      Equations
      source
      def Minimalist.Polarity.instReprPolFeature.repr :
      PolFeature → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Minimalist.Polarity.PolFeature.toFeatureVal :
        PolFeature → GramFeature

        Convert a PolFeature to a FeatureVal for use in the Agree system. [+Pol] maps to .pol true, [-Pol] maps to .pol false.

        Equations
        Instances For
          source
          def Minimalist.Polarity.PolFeature.toPolarity :
          PolFeature → Option Features.Polarity

          Recover Features.Polarity from a valued syntactic [±Pol] feature.

          Equations
          Instances For
            source
            structure Minimalist.Polarity.PolHead :
            Type

            A Pol⁰ head: the functional head projecting PolP.

            In @cite{holmberg-2016}'s analysis, every finite clause has a Pol⁰ bearing a [±Pol] feature. The head's category is Cat.Pol.

            • feature : PolFeature

              The polarity feature on this head

            • inQuestion : Bool

              Is this in a question context (unvalued [±Pol])?

            Instances For
              source
              @[implicit_reducible]
              instance Minimalist.Polarity.instReprPolHead :
              Repr PolHead
              Equations
              source
              def Minimalist.Polarity.instReprPolHead.repr :
              PolHead → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Minimalist.Polarity.PolHead.affirmative :
                PolHead

                An affirmative declarative Pol⁰: [+Pol]

                Equations
                Instances For
                  source
                  def Minimalist.Polarity.PolHead.negative :
                  PolHead

                  A negative declarative Pol⁰: [-Pol]

                  Equations
                  Instances For
                    source
                    def Minimalist.Polarity.PolHead.question :
                    PolHead

                    A polar question Pol⁰: [uPol]

                    Equations
                    Instances For
                      source
                      def Minimalist.Polarity.PolFeature.value (f : PolFeature) (p : Features.Polarity) :
                      Option PolFeature

                      Value an unvalued [±Pol] feature — the core operation in answering a polar question. The answer provides a Features.Polarity that values the feature.

                      Returns none if the feature is already valued (nothing to do).

                      Equations
                      Instances For
                        source
                        theorem Minimalist.Polarity.value_unvalued (p : Features.Polarity) :
                        PolFeature.unvalued.value p = some (PolFeature.valued p)

                        Valuing an unvalued feature always succeeds.

                        source
                        theorem Minimalist.Polarity.value_valued (p q : Features.Polarity) :
                        (PolFeature.valued p).value q = none

                        Valuing a valued feature always fails.

                        source
                        theorem Minimalist.Polarity.value_then_toPolarity (p : Features.Polarity) :
                        (PolFeature.unvalued.value p).bind PolFeature.toPolarity = some p

                        Round-trip: valuing then extracting polarity recovers the answer.

                        source
                        theorem Minimalist.Polarity.pol_feature_matches :
                        (FeatureVal.pol true).sameType (FeatureVal.pol false) = true

                        The [±Pol] feature matches itself in the Agree system.

                        source
                        theorem Minimalist.Polarity.pol_ne_neg :
                        (FeatureVal.pol true).sameType (FeatureVal.neg true) = false

                        [±Pol] is distinct from [±neg]: polarity and negation are separate features on separate heads (PolP vs NegP).