Documentation

Linglib.Semantics.Degree.Boundedness

Scale boundedness #

The four-way endpoint classification of scales — open, lower closed, upper closed, closed — of [kennedy-mcnally-2005] (22) and [kennedy-2007] (59), found independently by [rotstein-winter-2004]. Boundedness is the lexical tag a fragment entry stores (a record field cannot hold an OrderTop instance); degreeShape is an order carrier of that shape, with a greatest element exactly when the scale HasMax. dual is the antonym's scale, the same degrees with the ends exchanged, and ScalePolarity says which member of an antonym pair an adjective is.

Main declarations #

Scale boundedness #

source
inductive Degree.Boundedness :
Type

Which endpoints a scale has ([kennedy-mcnally-2005] (22), [kennedy-2007] (59)). Open scales may further approach a value without reaching it or be unbounded ([kennedy-2007] fn. 28); the tag does not record that.

Instances For
    source
    @[instance_reducible]
    instance Degree.instDecidableEqBoundedness :
    DecidableEq Boundedness
    Equations
    source
    @[instance_reducible]
    instance Degree.instReprBoundedness :
    Repr Boundedness
    Equations
    source
    def Degree.instReprBoundedness.repr :
    Boundedness → ℕ → Std.Format
    Equations
    Instances For
      source
      def Degree.Boundedness.HasMax :
      Boundedness → Prop

      The scale has a maximum.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance Degree.Boundedness.instDecidablePredHasMax :
        DecidablePred HasMax
        Equations
        source
        def Degree.Boundedness.HasMin :
        Boundedness → Prop

        The scale has a minimum.

        Equations
        Instances For
          source
          @[instance_reducible]
          instance Degree.Boundedness.instDecidablePredHasMin :
          DecidablePred HasMin
          Equations
          source
          def Degree.Boundedness.dual :
          Boundedness → Boundedness

          The antonym's scale: the same degrees with the ends exchanged ([kennedy-2007] (61)).

          Equations
          Instances For
            source
            @[simp]
            theorem Degree.Boundedness.dual_dual (b : Boundedness) :
            b.dual.dual = b
            source
            @[simp]
            theorem Degree.Boundedness.hasMax_dual {b : Boundedness} :
            b.dual.HasMax ↔ b.HasMin
            source
            @[simp]
            theorem Degree.Boundedness.hasMin_dual {b : Boundedness} :
            b.dual.HasMin ↔ b.HasMax

            Degree carrier per scale shape #

            A computable order carrier for each shape — only the OrderTop/NoMaxOrder mixin matters, not the carrier. The grounding is proved once here; per-dimension views transport it (Features.ScalarDimension.degree).

            source
            @[reducible, inline]
            abbrev Degree.Boundedness.degreeShape :
            Boundedness → Type

            Degree carrier per boundedness shape: a greatest element exists exactly when the scale HasMax.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance Degree.Boundedness.instLinearOrderDegreeShape (b : Boundedness) :
              LinearOrder b.degreeShape
              Equations
              • One or more equations did not get rendered due to their size.
              source
              theorem Degree.Boundedness.hasGreatest_degreeShape_iff (b : Boundedness) :
              (∃ (m : b.degreeShape), IsTop m) ↔ b.HasMax

              A greatest degree exists exactly when the classification says HasMax.

              Scale polarity #

              source
              inductive Degree.ScalePolarity :
              Type

              Intrinsic polarity of a scale dimension: positive is the unmarked direction (tall, hot), negative the inverted one (short, cold).

              Instances For
                source
                @[instance_reducible]
                instance Degree.instDecidableEqScalePolarity :
                DecidableEq ScalePolarity
                Equations
                source
                @[instance_reducible]
                instance Degree.instReprScalePolarity :
                Repr ScalePolarity
                Equations
                source
                def Degree.instReprScalePolarity.repr :
                ScalePolarity → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Degree.Boundedness.ofPolarity (b : Boundedness) :
                  ScalePolarity → Boundedness

                  The scale an adjective measures on: its dimension's scale for the positive member of an antonym pair, the same scale with the ends exchanged for the negative member.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Degree.Boundedness.ofPolarity_positive (b : Boundedness) :
                    b.ofPolarity ScalePolarity.positive = b
                    source
                    @[simp]
                    theorem Degree.Boundedness.ofPolarity_negative (b : Boundedness) :
                    b.ofPolarity ScalePolarity.negative = b.dual