Gradable Nouns as Measure Functions

[Mor09] [KMcN05]

Gradable nouns denote measure functions from individuals to degrees (eq. 48b): ⟦idiot⟧ = λx . ιd[x is d-idiotic] = idiot.

Size adjectives in degree readings are introduced by MEAS_N (eq. 76), the nominal counterpart of the adjectival MEAS morpheme. The Bigness Generalization (§2.2) follows from scale structure: min{d : small(d)} = d₀, making "small" vacuous.

Simplification: Our measN omits the d ∈ scale(g) restriction from Morzycki's full MEAS_N (eq. 76), since all examples here use a single shared degree scale. The full denotation is: ⟦MEAS_N⟧ = λg.λm.λx . [min{d : d ∈ scale(g) ∧ m(d)} ≤ g(x)] ∧ [standard(g) ≤ g(x)]

theorem Degree.d0_is_minimum (d : Bounded 10) : deg 0 ⋯ ≤ d

d0 is the minimum degree (from BoundedOrder).

structure Degree.GradableNoun (Entity : Type) : Type

A gradable noun maps individuals to degrees: ⟦idiot⟧ = λx.ιd[x is d-idiotic].

• name : String
• measure : Entity → Bounded 10

  The measure function: entity -> degree.

• standard : Bounded 10

  The contextual standard for this predicate.

def Degree.GradableNoun.pos {E : Type} (n : GradableNoun E) : E → Bool

Apply POS to a gradable noun: λx. standard(g) < g(x).

Uses strict inequality, matching positiveMeaning in Degree.Basic: an entity satisfies POS(N) iff its degree exceeds the standard ([Ken07]).

Equations

• n.pos x = decide (n.standard < n.measure x)

inductive Degree.SizePolarity : Type

Size adjectives characterized by polarity (big vs small).

• big : SizePolarity
• small : SizePolarity

def Degree.instReprSizePolarity.repr : SizePolarity → ℕ → Std.Format

Equations

• Degree.instReprSizePolarity.repr Degree.SizePolarity.big prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.SizePolarity.big")).group prec✝
• Degree.instReprSizePolarity.repr Degree.SizePolarity.small prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.SizePolarity.small")).group prec✝

@[implicit_reducible]

instance Degree.instReprSizePolarity : Repr SizePolarity

Equations

• Degree.instReprSizePolarity = { reprPrec := Degree.instReprSizePolarity.repr }

@[implicit_reducible]

instance Degree.instDecidableEqSizePolarity : DecidableEq SizePolarity

Equations

• Degree.instDecidableEqSizePolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.bigness (d : Bounded 10) : Bounded 10

Big: maps degrees to their "bigness" (identity on the degree scale).

Equations

• Degree.bigness d = d

def Degree.smallness (d : Bounded 10) : Bounded 10

Small: inverted ordering (0 maximally small, 10 minimally small).

Equations

• Degree.smallness d = Degree.Bounded.ofNat 10 (10 - d.toNat)

def Degree.bigStandard : Bounded 10

Standard for "big" (contextual, typically middling).

Equations

• Degree.bigStandard = Degree.deg 5 Degree.bigStandard._proof_2

def Degree.smallStandard : Bounded 10

Standard for "small" (contextual).

Equations

• Degree.smallStandard = Degree.deg 5 Degree.bigStandard._proof_2

def Degree.posBig (d : Bounded 10) : Bool

POS applied to size adjective: λd. standard(size) ≤ size(d).

Equations

• Degree.posBig d = decide (Degree.bigStandard ≤ Degree.bigness d)

def Degree.posSmall (d : Bounded 10) : Bool

Equations

• Degree.posSmall d = decide (Degree.smallStandard ≤ Degree.smallness d)

def Degree.minDegree (p : Bounded 10 → Bool) : Option (Bounded 10)

Find minimum degree satisfying a predicate.

Equations

• Degree.minDegree p = List.find? p (Degree.allDegrees 10)

def Degree.measN {E : Type} (noun : GradableNoun E) (sizeAdj : Bounded 10 → Bool) : E → Bool

Simplified MEAS_N: ⟦MEAS_N⟧(g)(m)(x) = [min{d : m(d)} ≤ g(x)] ∧ [standard(g) ≤ g(x)]. Full version (Morzycki eq. 76) has min over {d : d ∈ scale(g) ∧ m(d)}.

Equations

• Degree.measN noun sizeAdj x = match Degree.minDegree sizeAdj with | none => false | some minD => decide (minD ≤ noun.measure x ∧ noun.standard < noun.measure x)

def Degree.idiotNoun {E : Type} (measure : E → Bounded 10) : GradableNoun E

Example: an "idiot" gradable noun with standard at d3.

Equations

• Degree.idiotNoun measure = { name := "idiot", measure := measure, standard := Degree.deg 3 Degree.idiotNoun._proof_2 }

def Degree.bigIdiot {E : Type} (noun : GradableNoun E) : E → Bool

"big idiot" = MEASN(idiot)(POS big).

Equations

• Degree.bigIdiot noun = Degree.measN noun Degree.posBig

def Degree.smallIdiot {E : Type} (noun : GradableNoun E) : E → Bool

"small idiot" = MEASN(idiot)(POS small).

Equations

• Degree.smallIdiot noun = Degree.measN noun Degree.posSmall

theorem Degree.min_big_is_d5 : minDegree posBig = some (deg 5 ⋯)

Minimum degree satisfying "big" is d5.

theorem Degree.min_small_is_d0 : minDegree posSmall = some (deg 0 ⋯)

Minimum degree satisfying "small" is d0 (the scale minimum).

theorem Degree.d0_satisfies_small : posSmall (deg 0 ⋯) = true

d0 always satisfies smallness because it is maximally small.

theorem Degree.d0_is_min_for_small (d : Bounded 10) : posSmall d = true → deg 0 ⋯ ≤ d

d0 is the unique minimum for smallness.

theorem Degree.small_idiot_vacuous {E : Type} (noun : GradableNoun E) (x : E) : smallIdiot noun x = noun.pos x

"small idiot" is equivalent to just "idiot" (size adj is vacuous).

theorem Degree.big_idiot_restrictive {E : Type} (noun : GradableNoun E) (_h : noun.standard < deg 5 ⋯) (x : E) : bigIdiot noun x = true → noun.pos x = true

"big idiot" is more restrictive than just "idiot".

inductive Degree.Person : Type

A simple entity type for examples.

• george : Person
• sarah : Person
• floyd : Person

def Degree.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• Degree.instReprPerson.repr Degree.Person.george prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Person.george")).group prec✝
• Degree.instReprPerson.repr Degree.Person.sarah prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Person.sarah")).group prec✝
• Degree.instReprPerson.repr Degree.Person.floyd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Person.floyd")).group prec✝

@[implicit_reducible]

instance Degree.instReprPerson : Repr Person

Equations

• Degree.instReprPerson = { reprPrec := Degree.instReprPerson.repr }

@[implicit_reducible]

instance Degree.instDecidableEqPerson : DecidableEq Person

Equations

• Degree.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.idiocyMeasure : Person → Bounded 10

George: d8, Sarah: d4, Floyd: d1.

Equations

• Degree.idiocyMeasure Degree.Person.george = Degree.deg 8 Degree.idiocyMeasure._proof_4
• Degree.idiocyMeasure Degree.Person.sarah = Degree.deg 4 Degree.idiocyMeasure._proof_5
• Degree.idiocyMeasure Degree.Person.floyd = Degree.deg 1 Degree.idiocyMeasure._proof_6

def Degree.exampleIdiot : GradableNoun Person

Equations

• Degree.exampleIdiot = Degree.idiotNoun Degree.idiocyMeasure

theorem Degree.george_is_idiot : exampleIdiot.pos Person.george = true

George is an idiot.

theorem Degree.george_is_big_idiot : bigIdiot exampleIdiot Person.george = true

George is a big idiot.

theorem Degree.sarah_is_idiot_not_big : exampleIdiot.pos Person.sarah = true ∧ bigIdiot exampleIdiot Person.sarah = false

Sarah is an idiot but not a big idiot.

theorem Degree.small_idiot_same_as_idiot : smallIdiot exampleIdiot Person.george = exampleIdiot.pos Person.george ∧ smallIdiot exampleIdiot Person.sarah = exampleIdiot.pos Person.sarah ∧ smallIdiot exampleIdiot Person.floyd = exampleIdiot.pos Person.floyd

"Small idiot" gives same result as "idiot" (vacuous).