Documentation

Linglib.Semantics.Degree.Scale

Scalar dimensions #

This file defines Degree.ScalarDimension, the dimensions along which gradable adjectives and degree achievements measure, such as height, temperature and fullness. A dimension has a perceptual domain, the shape of its scale in its increasing direction, and, when it is a dimension of physical measurement, the physical dimension its degrees are measured in. Evaluative and psychological scales have none, which is why they reject measure phrases (six feet tall but not six feet happy), and speed is a primitive lexical scale although physically a quotient, in line with Bale and Schwarz's hypothesis that semantic composition has no quantity division. The degrees of a dimension are the canonical linear order of its scale's shape, and the default Vendler class of a degree achievement is read off that shape.

Main definitions #

Main results #

References #

source
inductive Degree.ScalarDimension :
Type

A scalar dimension is what a gradable adjective or a degree achievement measures along.

Instances For
    source
    @[instance_reducible]
    instance Degree.instDecidableEqScalarDimension :
    DecidableEq ScalarDimension
    Equations
    source
    def Degree.instReprScalarDimension.repr :
    ScalarDimension → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Degree.instReprScalarDimension :
      Repr ScalarDimension
      Equations
      source
      @[instance_reducible]
      instance Degree.instFintypeScalarDimension :
      Fintype ScalarDimension
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance Degree.instInhabitedScalarDimension :
      Inhabited ScalarDimension
      Equations
      source
      @[instance_reducible]
      instance Degree.instBEqScalarDimension :
      BEq ScalarDimension
      Equations
      source
      def Degree.instBEqScalarDimension.beq :
      ScalarDimension → ScalarDimension → Bool
      Equations
      Instances For
        source
        def Degree.ScalarDimension.domain :
        ScalarDimension → PropertyDomain

        The perceptual or cognitive domain of a dimension.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Degree.ScalarDimension.boundedness :
          ScalarDimension → Boundedness

          The shape of a dimension's scale in its increasing direction ([KMcN05] (24)–(27), [Ken07b] (33), (49)–(50), (60)). Wetness is lower closed, wet taking a minimum standard and dry a maximum one, straightness upper closed, by fully straight against ??fully bent, and fullness closed, by 100% full and 100% empty. Possibility is lower closed, since nothing is less possible than the impossible ([Las17a] §5.2.3), so possible takes a minimum standard and impossible a maximum one, as wet and dry do; whether it also has a maximum turns on the disputed identity of its scale with that of likely. The negative member of an antonym pair measures on the dual scale. The definition is reducible, so that order instances on the degrees of a dimension see through it.

          Equations
          Instances For

            Bridges to the physical quantity algebra #

            source
            def Degree.ScalarDimension.dimension? :
            ScalarDimension → Option QuantityDimension

            The physical dimension a scalar dimension is measured in, if any. Spatial scales are measured in distance, weight in mass, age in time, temperature in temperature and quantity in cardinality, and fast lexicalizes the quotient of distance by time as a primitive scale. Evaluative, psychological and state scales, which reject ratio measure phrases, have none.

            Equations
            Instances For

              Degrees #

              source
              @[reducible, inline]
              abbrev Degree.ScalarDimension.Scale (d : ScalarDimension) :
              Type

              The degrees of a dimension are the canonical linear order of its scale's shape.

              Equations
              Instances For
                source
                @[instance_reducible]
                instance Degree.instLinearOrderScale (d : ScalarDimension) :
                LinearOrder d.Scale
                Equations
                source
                theorem Degree.ScalarDimension.hasGreatest_scale_iff (d : ScalarDimension) :
                (∃ (m : d.Scale), IsTop m) ↔ d.boundedness.HasMax

                The degrees of a dimension have a greatest element exactly when its scale has a maximum.

                Degree achievements #

                source
                def Degree.Boundedness.defaultVendlerClass (b : Boundedness) :
                Aspect.VendlerClass

                A degree achievement on a scale of shape b is by default an accomplishment when Interpretive Economy prefers the maximum standard on b with a least degree adjoined, the scale of its measure of change, and an activity otherwise ([KL08]).

                Equations
                Instances For
                  source
                  theorem Degree.Boundedness.defaultVendlerClass_eq_accomplishment_iff {b : Boundedness} :
                  b.defaultVendlerClass = Aspect.VendlerClass.accomplishment ↔ b.HasMax
                  source
                  theorem Degree.Boundedness.telicity_defaultVendlerClass_eq_telic_iff {b : Boundedness} :
                  b.defaultVendlerClass.telicity = Aspect.Telicity.telic ↔ b.HasMax

                  A degree achievement on a scale is telic by default exactly when the scale has a maximum.

                  source
                  def Degree.ScalarDimension.defaultVendlerClass (d : ScalarDimension) :
                  Aspect.VendlerClass

                  The default Vendler class of a degree achievement towards the positive pole of a dimension is that of the dimension's scale.

                  Equations
                  Instances For
                    source
                    def Degree.ScalarDimension.defaultTelicity (d : ScalarDimension) :
                    Aspect.Telicity

                    The default telicity of a degree achievement on a dimension is that of its default Vendler class.

                    Equations
                    Instances For
                      source
                      theorem Degree.ScalarDimension.defaultTelicity_telic_iff_hasGreatest (d : ScalarDimension) :
                      d.defaultTelicity = Aspect.Telicity.telic ↔ ∃ (m : d.Scale), IsTop m

                      A degree achievement is telic by default exactly when the degrees of its scale have a greatest element ([KL08]).

                      source
                      @[simp]
                      theorem Degree.ScalarDimension.telicity_defaultVendlerClass (d : ScalarDimension) :
                      d.defaultVendlerClass.telicity = d.defaultTelicity

                      The default Vendler class has the default telicity.

                      source
                      @[simp]
                      theorem Degree.ScalarDimension.duration_defaultVendlerClass (d : ScalarDimension) :
                      d.defaultVendlerClass.duration = Aspect.Duration.durative

                      A degree achievement is durative.

                      source
                      @[simp]
                      theorem Degree.ScalarDimension.dynamicity_defaultVendlerClass (d : ScalarDimension) :
                      d.defaultVendlerClass.dynamicity = Aspect.Dynamicity.dynamic

                      A degree achievement is dynamic.