Linglib.Core.Scales.HornScale

Under lower-bound semantics, numerals do form a scale (⟨1, 2, 3,...⟩), but it is infinite — a finite HornScale list can't represent it correctly ("five" would have no stronger alternatives).
Under bilateral semantics, numerals are non-monotonic and do NOT form a Horn scale at all. The relevant alternatives are {bare n, Class A n, Class B n}, not other numerals.

Both cases are handled properly in Theories/Semantics.Montague/Determiner/Numeral/Semantics.lean:

NumeralTheory.isStrongerThan computes strength for any theory
NumeralAlternative represents Kennedy's alternative sets
lowerBound_monotonic / bilateral_not_monotonic prove the key contrast

Singular/Plural as a Horn Scale #

@cite{sauerland-2003} @cite{spector-2007} @cite{tieu-etal-2020}

The singular and plural morphemes form a Horn scale ⟨singular, plural⟩ where singular ("a giraffe") is the stronger alternative to plural ("giraffes").

Under the implicature approach to multiplicity inferences, the plural literally means "one or more" and the "more than one" inference arises as a scalar implicature: the listener reasons that the speaker chose the weaker "giraffes" over the stronger "a giraffe," implying that the singular alternative is false — hence more than one.

This scale is structurally unusual: the alternatives differ in morphology (number marking), not in lexical choice (unlike some/all, or/and).

source

inductive Core.Scale.Number.NumberExpr :

Type

singular : NumberExpr
plural : NumberExpr

Instances For

source

instance Core.Scale.Number.instDecidableEqNumberExpr :

DecidableEq NumberExpr

Equations

Core.Scale.Number.instDecidableEqNumberExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Core.Scale.Number.instBEqNumberExpr :

BEq NumberExpr

Equations

Core.Scale.Number.instBEqNumberExpr = { beq := Core.Scale.Number.instBEqNumberExpr.beq }

source

def Core.Scale.Number.instBEqNumberExpr.beq :

NumberExpr → NumberExpr → Bool

Equations

Core.Scale.Number.instBEqNumberExpr.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.Scale.Number.instReprNumberExpr :

Repr NumberExpr

Equations

Core.Scale.Number.instReprNumberExpr = { reprPrec := Core.Scale.Number.instReprNumberExpr.repr }

source

def Core.Scale.Number.instReprNumberExpr.repr :

NumberExpr → ℕ → Std.Format

Equations

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

Instances For

source

instance Core.Scale.Number.instInhabitedNumberExpr :

Inhabited NumberExpr

Equations

Core.Scale.Number.instInhabitedNumberExpr = { default := Core.Scale.Number.instInhabitedNumberExpr.default }

source

def Core.Scale.Number.instInhabitedNumberExpr.default :

NumberExpr

Equations

Core.Scale.Number.instInhabitedNumberExpr.default = Core.Scale.Number.NumberExpr.singular

Instances For

source

def Core.Scale.Number.NumberExpr.toString :

NumberExpr → String

Equations

Core.Scale.Number.NumberExpr.singular.toString = "singular"
Core.Scale.Number.NumberExpr.plural.toString = "plural"

Instances For

source

instance Core.Scale.Number.instToStringNumberExpr :

ToString NumberExpr

Equations

Core.Scale.Number.instToStringNumberExpr = { toString := Core.Scale.Number.NumberExpr.toString }

source

def Core.Scale.Number.numberScale :

HornScale NumberExpr

Singular is stronger: "a giraffe" entails "giraffes" (one or more).

Equations

Core.Scale.Number.numberScale = { members := [Core.Scale.Number.NumberExpr.plural , Core.Scale.Number.NumberExpr.singular ] }

Instances For

source

theorem Core.Scale.Number.singular_stronger_than_plural :

isStronger numberScale NumberExpr.singular NumberExpr.plural = true

source

theorem Core.Scale.Number.plural_alternative :

strongerAlternatives numberScale NumberExpr.plural = [NumberExpr.singular ]

source

def Core.Scale.scalarImplicatures {α : Type} [BEq α] (s : HornScale α) (x : α) :

List α

Equations

Core.Scale.scalarImplicatures s x = Core.Scale.strongerAlternatives s x

Instances For

source

inductive Core.Scale.Monotonicity :

Type

upward : Monotonicity
downward : Monotonicity

Instances For

source

instance Core.Scale.instDecidableEqMonotonicity :

DecidableEq Monotonicity

Equations

Core.Scale.instDecidableEqMonotonicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.Scale.instBEqMonotonicity.beq :

Monotonicity → Monotonicity → Bool

Equations

Core.Scale.instBEqMonotonicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.Scale.instBEqMonotonicity :

BEq Monotonicity

Equations

Core.Scale.instBEqMonotonicity = { beq := Core.Scale.instBEqMonotonicity.beq }

source

def Core.Scale.instReprMonotonicity.repr :

Monotonicity → ℕ → Std.Format

Equations

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

Instances For

source

instance Core.Scale.instReprMonotonicity :

Repr Monotonicity

Equations

Core.Scale.instReprMonotonicity = { reprPrec := Core.Scale.instReprMonotonicity.repr }

source

def Core.Scale.scalarAlternativesInContext {α : Type} [BEq α] (s : HornScale α) (x : α) (m : Monotonicity) :

List α

Equations

Instances For

source

theorem Core.Scale.de_blocks_some_not_all :

scalarAlternativesInContext Quantifiers.quantScale Quantifiers.QuantExpr.all Monotonicity.downward = [Quantifiers.QuantExpr.none_, Quantifiers.QuantExpr.some_, Quantifiers.QuantExpr.most ]

source

def Core.Scale.Polarity.toMonotonicity :

Polarity → Monotonicity

Sentence polarity determines monotonicity context: positive sentences are upward-entailing, negative are downward-entailing. This is the Ladusaw (1979) / Fauconnier (1975) connection.

Equations

Instances For