Gradable Nouns as Measure Functions

@cite{morzycki-2009} @cite{kennedy-mcnally-2005}

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)]

@[reducible, inline]

abbrev Semantics.Lexical.Noun.GradableNouns.Degree : Type

Degree on a 0–10 scale, backed by the canonical Degree 10 type.

Equations

• Semantics.Lexical.Noun.GradableNouns.Degree = Core.Scale.Degree 10

def Semantics.Lexical.Noun.GradableNouns.allDegrees : List Degree

All degrees on the 0–10 scale.

Equations

• Semantics.Lexical.Noun.GradableNouns.allDegrees = Core.Scale.allDegrees 10

theorem Semantics.Lexical.Noun.GradableNouns.d0_is_minimum (d : Degree) : Core.Scale.deg 0 ⋯ ≤ d

d0 is the minimum degree (from BoundedOrder).

structure Semantics.Lexical.Noun.GradableNouns.GradableNoun (Entity : Type) : Type

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

• name : String
• measure : Entity → Degree

  The measure function: entity -> degree.

• standard : Degree

  The contextual standard for this predicate.

def Semantics.Lexical.Noun.GradableNouns.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.Core: an entity satisfies POS(N) iff its degree exceeds the standard (@cite{kennedy-2007}).

Equations

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

inductive Semantics.Lexical.Noun.GradableNouns.SizePolarity : Type

Size adjectives characterized by polarity (big vs small).

• big : SizePolarity
• small : SizePolarity

def Semantics.Lexical.Noun.GradableNouns.instReprSizePolarity.repr : SizePolarity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Semantics.Lexical.Noun.GradableNouns.instReprSizePolarity : Repr SizePolarity

Equations

• Semantics.Lexical.Noun.GradableNouns.instReprSizePolarity = { reprPrec := Semantics.Lexical.Noun.GradableNouns.instReprSizePolarity.repr }

instance Semantics.Lexical.Noun.GradableNouns.instDecidableEqSizePolarity : DecidableEq SizePolarity

Equations

• Semantics.Lexical.Noun.GradableNouns.instDecidableEqSizePolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Noun.GradableNouns.instBEqSizePolarity : BEq SizePolarity

Equations

• Semantics.Lexical.Noun.GradableNouns.instBEqSizePolarity = { beq := Semantics.Lexical.Noun.GradableNouns.instBEqSizePolarity.beq }

def Semantics.Lexical.Noun.GradableNouns.instBEqSizePolarity.beq : SizePolarity → SizePolarity → Bool

Equations

• Semantics.Lexical.Noun.GradableNouns.instBEqSizePolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Noun.GradableNouns.bigness (d : Degree) : Degree

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

Equations

• Semantics.Lexical.Noun.GradableNouns.bigness d = d

def Semantics.Lexical.Noun.GradableNouns.smallness (d : Degree) : Degree

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

Equations

• Semantics.Lexical.Noun.GradableNouns.smallness d = Core.Scale.Degree.ofNat 10 (10 - Core.Scale.Degree.toNat d)

def Semantics.Lexical.Noun.GradableNouns.bigStandard : Degree

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

Equations

• Semantics.Lexical.Noun.GradableNouns.bigStandard = Core.Scale.deg 5 Semantics.Lexical.Noun.GradableNouns.bigStandard._proof_2

def Semantics.Lexical.Noun.GradableNouns.smallStandard : Degree

Standard for "small" (contextual).

Equations

• Semantics.Lexical.Noun.GradableNouns.smallStandard = Core.Scale.deg 5 Semantics.Lexical.Noun.GradableNouns.bigStandard._proof_2

def Semantics.Lexical.Noun.GradableNouns.posBig (d : Degree) : Bool

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

Equations

• Semantics.Lexical.Noun.GradableNouns.posBig d = decide (Semantics.Lexical.Noun.GradableNouns.bigStandard ≤ Semantics.Lexical.Noun.GradableNouns.bigness d)

def Semantics.Lexical.Noun.GradableNouns.posSmall (d : Degree) : Bool

Equations

• Semantics.Lexical.Noun.GradableNouns.posSmall d = decide (Semantics.Lexical.Noun.GradableNouns.smallStandard ≤ Semantics.Lexical.Noun.GradableNouns.smallness d)

def Semantics.Lexical.Noun.GradableNouns.minDegree (p : Degree → Bool) : Option Degree

Find minimum degree satisfying a predicate.

Equations

• Semantics.Lexical.Noun.GradableNouns.minDegree p = List.find? p Semantics.Lexical.Noun.GradableNouns.allDegrees

def Semantics.Lexical.Noun.GradableNouns.measN {E : Type} (noun : GradableNoun E) (sizeAdj : Degree → 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

• One or more equations did not get rendered due to their size.

def Semantics.Lexical.Noun.GradableNouns.idiotNoun {E : Type} (measure : E → Degree) : GradableNoun E

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

Equations

• Semantics.Lexical.Noun.GradableNouns.idiotNoun measure = { name := "idiot", measure := measure, standard := Core.Scale.deg 3 Semantics.Lexical.Noun.GradableNouns.idiotNoun._proof_2 }

def Semantics.Lexical.Noun.GradableNouns.bigIdiot {E : Type} (noun : GradableNoun E) : E → Bool

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

Equations

• Semantics.Lexical.Noun.GradableNouns.bigIdiot noun = Semantics.Lexical.Noun.GradableNouns.measN noun Semantics.Lexical.Noun.GradableNouns.posBig

def Semantics.Lexical.Noun.GradableNouns.smallIdiot {E : Type} (noun : GradableNoun E) : E → Bool

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

Equations

• Semantics.Lexical.Noun.GradableNouns.smallIdiot noun = Semantics.Lexical.Noun.GradableNouns.measN noun Semantics.Lexical.Noun.GradableNouns.posSmall

theorem Semantics.Lexical.Noun.GradableNouns.min_big_is_d5 : minDegree posBig = some (Core.Scale.deg 5 ⋯)

Minimum degree satisfying "big" is d5.

theorem Semantics.Lexical.Noun.GradableNouns.min_small_is_d0 : minDegree posSmall = some (Core.Scale.deg 0 ⋯)

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

theorem Semantics.Lexical.Noun.GradableNouns.d0_satisfies_small : posSmall (Core.Scale.deg 0 ⋯) = true

d0 always satisfies smallness because it is maximally small.

theorem Semantics.Lexical.Noun.GradableNouns.d0_is_min_for_small (d : Degree) : posSmall d = true → Core.Scale.deg 0 ⋯ ≤ d

d0 is the unique minimum for smallness.

theorem Semantics.Lexical.Noun.GradableNouns.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 Semantics.Lexical.Noun.GradableNouns.big_idiot_restrictive {E : Type} (noun : GradableNoun E) (_h : noun.standard < Core.Scale.deg 5 ⋯) (x : E) : bigIdiot noun x = true → noun.pos x = true

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

inductive Semantics.Lexical.Noun.GradableNouns.Person : Type

A simple entity type for examples.

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

instance Semantics.Lexical.Noun.GradableNouns.instReprPerson : Repr Person

Equations

• Semantics.Lexical.Noun.GradableNouns.instReprPerson = { reprPrec := Semantics.Lexical.Noun.GradableNouns.instReprPerson.repr }

def Semantics.Lexical.Noun.GradableNouns.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Semantics.Lexical.Noun.GradableNouns.instDecidableEqPerson : DecidableEq Person

Equations

• Semantics.Lexical.Noun.GradableNouns.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Noun.GradableNouns.instBEqPerson.beq : Person → Person → Bool

Equations

• Semantics.Lexical.Noun.GradableNouns.instBEqPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Noun.GradableNouns.instBEqPerson : BEq Person

Equations

• Semantics.Lexical.Noun.GradableNouns.instBEqPerson = { beq := Semantics.Lexical.Noun.GradableNouns.instBEqPerson.beq }

def Semantics.Lexical.Noun.GradableNouns.idiocyMeasure : Person → Degree

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

Equations

• Semantics.Lexical.Noun.GradableNouns.idiocyMeasure Semantics.Lexical.Noun.GradableNouns.Person.george = Core.Scale.deg 8 Semantics.Lexical.Noun.GradableNouns.idiocyMeasure._proof_4
• Semantics.Lexical.Noun.GradableNouns.idiocyMeasure Semantics.Lexical.Noun.GradableNouns.Person.sarah = Core.Scale.deg 4 Semantics.Lexical.Noun.GradableNouns.idiocyMeasure._proof_5
• Semantics.Lexical.Noun.GradableNouns.idiocyMeasure Semantics.Lexical.Noun.GradableNouns.Person.floyd = Core.Scale.deg 1 Semantics.Lexical.Noun.GradableNouns.idiocyMeasure._proof_6

def Semantics.Lexical.Noun.GradableNouns.exampleIdiot : GradableNoun Person

Equations

• Semantics.Lexical.Noun.GradableNouns.exampleIdiot = Semantics.Lexical.Noun.GradableNouns.idiotNoun Semantics.Lexical.Noun.GradableNouns.idiocyMeasure

theorem Semantics.Lexical.Noun.GradableNouns.george_is_idiot : exampleIdiot.pos Person.george = true

George is an idiot.

theorem Semantics.Lexical.Noun.GradableNouns.george_is_big_idiot : bigIdiot exampleIdiot Person.george = true

George is a big idiot.

theorem Semantics.Lexical.Noun.GradableNouns.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 Semantics.Lexical.Noun.GradableNouns.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).