Documentation

Linglib.Theories.Semantics.Degree.Differential

Differential Comparative Semantics #

@cite{schwarzschild-2005} @cite{solt-2015} @cite{winter-2005}

Compositional semantics for measure phrase differentials in comparatives: "3 inches taller", "twice as tall as".

Measure Phrase Composition #

@cite{schwarzschild-2005}: measure phrases modify the degree argument of the comparative, specifying the gap between matrix and standard degrees.

"A is 3 inches taller than B" iff height(A) - height(B) = 3 inches

This requires a ratio scale (with a meaningful zero point and unit), not just an ordinal or interval scale. Hence "3 inches taller" ✓ but "*3 units more beautiful" ✗.

source
def Semantics.Degree.Differential.differentialComparative {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (diff : ℚ) :
Prop

Differential comparative: "A is d-much Adj-er than B" iff the difference μ(A) - μ(B) = d.

Requires a type with subtraction (ring-like structure), not just ordering. This is what makes measure phrase differentials more restrictive than bare comparatives.

Equations
Instances For
    source
    theorem Semantics.Degree.Differential.differential_positive_iff {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (diff : ℚ) (hdiff : diff > 0) :
    differentialComparative μ a b diff → μ a > μ b

    The differential is positive iff the comparative holds.

    source
    inductive Semantics.Degree.Differential.MeasurementLevel :
    Type

    Measurement level: what kind of scale an adjective's degrees live on. Measure phrase differentials require at least interval scale; factor phrases require ratio scale.

    Instances For
      source
      instance Semantics.Degree.Differential.instDecidableEqMeasurementLevel :
      DecidableEq MeasurementLevel
      Equations
      source
      def Semantics.Degree.Differential.instBEqMeasurementLevel.beq :
      MeasurementLevel → MeasurementLevel → Bool
      Equations
      Instances For
        source
        instance Semantics.Degree.Differential.instBEqMeasurementLevel :
        BEq MeasurementLevel
        Equations
        source
        instance Semantics.Degree.Differential.instReprMeasurementLevel :
        Repr MeasurementLevel
        Equations
        source
        def Semantics.Degree.Differential.instReprMeasurementLevel.repr :
        MeasurementLevel → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Degree.Differential.admitsMeasurePhrase :
          MeasurementLevel → Bool

          Does this measurement level admit measure phrase differentials?

          Equations
          Instances For
            source
            def Semantics.Degree.Differential.admitsFactorPhrase :
            MeasurementLevel → Bool

            Does this measurement level admit factor phrases ("twice as tall")?

            Equations
            Instances For
              source
              def Semantics.Degree.Differential.factorEquative {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (factor : ℚ) :
              Prop

              Factor phrase equative: "A is n times as tall as B" iff μ(A) = n × μ(B). Requires ratio scale: a meaningful zero point.

              Equations
              Instances For