Documentation

Linglib.Theories.Semantics.Degree.Frameworks.Kennedy

Kennedy's Measure Function Approach #

@cite{kennedy-2007} @cite{kennedy-mcnally-2005}

@cite{kennedy-2007} "Vagueness and Grammar": gradable adjectives denote relations between individuals and degrees, mediated by a measure function μ.

Denotation #

⟦tall⟧ = λd.λx. height(x) ≥ d

The adjective takes a degree argument d (type ⟨d,⟨e,t⟩⟩) and returns a predicate true of entities whose degree meets or exceeds d.

Comparative #

⟦-er⟧ = λG.λG'. max(G') > max(G)

The comparative morpheme takes two degree predicates (from the matrix and the than-clause) and asserts the matrix maximum exceeds the standard maximum.

Scale Structure and Interpretive Economy #

Kennedy's key contribution: scale structure (open vs. closed) determines how the positive form standard is set:

Interpretive Economy: "Maximize the contribution of the conventional meanings of the elements of a sentence to the computation of its truth conditions." When a scale has an endpoint, using it as the standard is more informative than using a contextual norm.

source
def Semantics.Degree.Frameworks.Kennedy.adjDenotation {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (d : D) (x : Entity) :
Prop

Kennedy's adjective denotation: a relation between degrees and entities. ⟦tall⟧ = λd.λx. height(x) ≥ d The degree argument is abstracted over and bound by a degree morpheme (-er, as, -est, too, enough).

Equations
Instances For
    source
    def Semantics.Degree.Frameworks.Kennedy.degreeSet {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (x : Entity) :
    Set D

    The degree set of an entity: the set of degrees d such that μ(x) ≥ d. This is an initial segment (downward closed set) of the scale.

    Equations
    Instances For
      source
      def Semantics.Degree.Frameworks.Kennedy.comparativeMorpheme {D : Type u_1} [LinearOrder D] (maxA maxB : D) :
      Prop

      Kennedy's comparative morpheme: ⟦-er⟧ = λG.λG'. max(G') > max(G). Under the measure function approach, this reduces to comparing the maxima of two degree sets. Since degreeSet is [0, μ(x)] (for positive adjectives on bounded scales), max = μ(x).

      Equations
      Instances For
        source
        def Semantics.Degree.Frameworks.Kennedy.kennedyComparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) :
        Prop

        Kennedy comparative with measure function: reduces to direct comparison. "A is taller than B" iff height(A) > height(B).

        Equations
        Instances For
          source
          inductive Semantics.Degree.Frameworks.Kennedy.PositiveStandard :
          Type

          Positive form standard: how the contextual threshold is determined. @cite{kennedy-2007}: for open scales, the standard is the contextual norm; for closed scales, it's the relevant endpoint.

          Instances For
            source
            instance Semantics.Degree.Frameworks.Kennedy.instDecidableEqPositiveStandard :
            DecidableEq PositiveStandard
            Equations
            source
            def Semantics.Degree.Frameworks.Kennedy.instBEqPositiveStandard.beq :
            PositiveStandard → PositiveStandard → Bool
            Equations
            Instances For
              source
              instance Semantics.Degree.Frameworks.Kennedy.instBEqPositiveStandard :
              BEq PositiveStandard
              Equations
              source
              def Semantics.Degree.Frameworks.Kennedy.instReprPositiveStandard.repr :
              PositiveStandard → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance Semantics.Degree.Frameworks.Kennedy.instReprPositiveStandard :
                Repr PositiveStandard
                Equations
                source
                def Semantics.Degree.Frameworks.Kennedy.interpretiveEconomy (b : Core.Scale.Boundedness) :
                PositiveStandard

                Interpretive Economy determines the standard from scale structure. When a scale has an endpoint, Interpretive Economy requires using it as the standard (more informative than contextual norm).

                Equations
                Instances For
                  source
                  def Semantics.Degree.Frameworks.Kennedy.isClassA (b : Core.Scale.Boundedness) :
                  Bool

                  @cite{kennedy-2007} Class A vs. Class B adjectives.

                  • Class A (relative): open scale, contextual standard. "tall", "expensive", "heavy"
                  • Class B (absolute): closed scale, endpoint standard. "full", "empty", "straight", "bent"

                  The class is determined entirely by scale boundedness.

                  Equations
                  Instances For
                    source
                    def Semantics.Degree.Frameworks.Kennedy.isClassB (b : Core.Scale.Boundedness) :
                    Bool
                    Equations
                    Instances For
                      source
                      theorem Semantics.Degree.Frameworks.Kennedy.classA_contextual :
                      interpretiveEconomy Core.Scale.Boundedness.open_ = PositiveStandard.contextual

                      Class A adjectives have contextual standards.

                      source
                      theorem Semantics.Degree.Frameworks.Kennedy.classB_endpoint :
                      interpretiveEconomy Core.Scale.Boundedness.closed = PositiveStandard.maxEndpoint

                      Class B adjectives (closed scale) have endpoint standards.