Documentation

Linglib.Theories.Semantics.Degree.ThanClause

Than-Clause Semantics #

@cite{bhatt-pancheva-2004} @cite{heim-2006} @cite{von-stechow-1984}

Compositional semantics for the than-clause in comparative constructions. The than-clause introduces the standard of comparison and determines the degree set against which the matrix predicate is evaluated.

Key Issues #

  1. Max operator: the than-clause denotes a degree set, and the comparative requires its maximum (max(than-clause)) to compare against the matrix degree.

  2. Phrasal vs. clausal: phrasal "than Bill" vs. clausal "than Bill is tall" — the clausal than-clause makes the degree abstraction explicit.

  3. Scope: the than-clause interacts with scope-taking elements (quantifiers, modals, negation).

source
def Semantics.Degree.ThanClause.thanClauseDenotation {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (standard : Entity) :
Set D

A than-clause denotes a degree predicate: the set of degrees that the standard entity has.

"than Bill is tall" → λd. height(Bill) ≥ d = {d | d ≤ height(Bill)}

This is a downward-closed set (initial segment) when the predicate is a positive adjective.

Equations
Instances For
    source
    def Semantics.Degree.ThanClause.thanClauseMax {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (standard : Entity) :
    D

    The maximum of a than-clause denotation is the degree of the standard entity: max({d | d ≤ μ(b)}) = μ(b).

    Equations
    Instances For
      source
      theorem Semantics.Degree.ThanClause.max_in_denotation {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (b : Entity) :
      thanClauseMax μ b ∈ thanClauseDenotation μ b

      The than-clause maximum is in the than-clause denotation.

      source
      theorem Semantics.Degree.ThanClause.max_is_upper_bound {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (b : Entity) (d : D) :
      d ∈ thanClauseDenotation μ b → d ≤ thanClauseMax μ b

      The than-clause maximum is an upper bound of the denotation.

      source
      inductive Semantics.Degree.ThanClause.ThanClauseType :
      Type

      The two syntactic forms of than-clauses.

      Instances For
        source
        instance Semantics.Degree.ThanClause.instDecidableEqThanClauseType :
        DecidableEq ThanClauseType
        Equations
        source
        def Semantics.Degree.ThanClause.instBEqThanClauseType.beq :
        ThanClauseType → ThanClauseType → Bool
        Equations
        Instances For
          source
          instance Semantics.Degree.ThanClause.instBEqThanClauseType :
          BEq ThanClauseType
          Equations
          source
          def Semantics.Degree.ThanClause.instReprThanClauseType.repr :
          ThanClauseType → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance Semantics.Degree.ThanClause.instReprThanClauseType :
            Repr ThanClauseType
            Equations
            source
            theorem Semantics.Degree.ThanClause.phrasal_clausal_equivalence {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (b : Entity) :
            thanClauseMax μ b = μ b

            Phrasal and clausal than-clauses yield the same degree when the elided material is the same predicate. "taller than Bill" and "taller than Bill is tall" have the same truth conditions.

            source
            theorem Semantics.Degree.ThanClause.thanClause_eq_posExt {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (b : Entity) :
            thanClauseDenotation μ b = Core.Scale.posExt μ b

            The than-clause denotation is the positive extent of the standard entity — the same algebraic object that Kennedy calls "degree set" and Schwarzschild calls "positive interval".