Quantity Domains for Scalar Implicatures

Building blocks for tutorial-style scalar quantity domains used in scalar-implicature studies (RSA models, EXH models, neo-Gricean derivations). The canonical 6-element ⟨none, few, some, half, most, all⟩ paradigm now lives in Phenomena.Quantification.Inventory; this file covers the smaller 3- and 4-element domains used as toy tutorial scales.

Components

• Utterance: 3-element scalar utterances (none, some, all)
• ExtUtterance: 4-element extension with "most"
• meaning: Literal semantics for scalar utterances
• extMeaning: Extended semantics with "most"

inductive Phenomena.ScalarImplicatures.QuantityDomain.Utterance : Type

Scalar utterances for quantity domains

• none_ : Utterance
• some_ : Utterance
• all : Utterance

def Phenomena.ScalarImplicatures.QuantityDomain.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instReprUtterance : Repr Utterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instReprUtterance = { reprPrec := Phenomena.ScalarImplicatures.QuantityDomain.instReprUtterance.repr }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instDecidableEqUtterance : DecidableEq Utterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedUtterance.default : Utterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedUtterance.default = Phenomena.ScalarImplicatures.QuantityDomain.Utterance.none_

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedUtterance : Inhabited Utterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedUtterance = { default := Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedUtterance.default }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instFintypeUtterance : Fintype Utterance

Equations

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

def Phenomena.ScalarImplicatures.QuantityDomain.meaning (n : ℕ) : Utterance → Fin (n + 1) → Bool

Literal semantics (weak "some")

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.meaning n Phenomena.ScalarImplicatures.QuantityDomain.Utterance.none_ x✝ = (↑x✝ == 0)
• Phenomena.ScalarImplicatures.QuantityDomain.meaning n Phenomena.ScalarImplicatures.QuantityDomain.Utterance.some_ x✝ = decide (↑x✝ ≥ 1)
• Phenomena.ScalarImplicatures.QuantityDomain.meaning n Phenomena.ScalarImplicatures.QuantityDomain.Utterance.all x✝ = (↑x✝ == n)

def Phenomena.ScalarImplicatures.QuantityDomain.allUtterances : List Utterance

All utterances

Equations

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

def Phenomena.ScalarImplicatures.QuantityDomain.allWorlds (n : ℕ) : List (Fin (n + 1))

All worlds for a domain of size n

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.allWorlds n = List.finRange (n + 1)

def Phenomena.ScalarImplicatures.QuantityDomain.w0 {n : ℕ} : Fin (n + 1)

World where 0 have the property

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.w0 = ⟨0, ⋯⟩

def Phenomena.ScalarImplicatures.QuantityDomain.w1 {n : ℕ} (h : 1 < n + 1 := by omega) : Fin (n + 1)

World where 1 has the property

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.w1 h = ⟨1, h⟩

def Phenomena.ScalarImplicatures.QuantityDomain.w2 {n : ℕ} (h : 2 < n + 1 := by omega) : Fin (n + 1)

World where 2 have the property

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.w2 h = ⟨2, h⟩

def Phenomena.ScalarImplicatures.QuantityDomain.wAll {n : ℕ} : Fin (n + 1)

World where all n have the property

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.wAll = ⟨n, ⋯⟩

inductive Phenomena.ScalarImplicatures.QuantityDomain.ExtUtterance : Type

Extended scalar utterances including "most"

• none_ : ExtUtterance
• some_ : ExtUtterance
• most : ExtUtterance
• all : ExtUtterance

def Phenomena.ScalarImplicatures.QuantityDomain.instReprExtUtterance.repr : ExtUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instReprExtUtterance : Repr ExtUtterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instReprExtUtterance = { reprPrec := Phenomena.ScalarImplicatures.QuantityDomain.instReprExtUtterance.repr }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instDecidableEqExtUtterance : DecidableEq ExtUtterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instDecidableEqExtUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedExtUtterance.default : ExtUtterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedExtUtterance.default = Phenomena.ScalarImplicatures.QuantityDomain.ExtUtterance.none_

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedExtUtterance : Inhabited ExtUtterance

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedExtUtterance = { default := Phenomena.ScalarImplicatures.QuantityDomain.instInhabitedExtUtterance.default }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.QuantityDomain.instFintypeExtUtterance : Fintype ExtUtterance

Equations

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

def Phenomena.ScalarImplicatures.QuantityDomain.extMeaning (n : ℕ) : ExtUtterance → Fin (n + 1) → Bool

Extended semantics with "most"

Equations

• Phenomena.ScalarImplicatures.QuantityDomain.extMeaning n Phenomena.ScalarImplicatures.QuantityDomain.ExtUtterance.none_ x✝ = (↑x✝ == 0)
• Phenomena.ScalarImplicatures.QuantityDomain.extMeaning n Phenomena.ScalarImplicatures.QuantityDomain.ExtUtterance.some_ x✝ = decide (↑x✝ ≥ 1)
• Phenomena.ScalarImplicatures.QuantityDomain.extMeaning n Phenomena.ScalarImplicatures.QuantityDomain.ExtUtterance.most x✝ = decide (↑x✝ * 2 > n)
• Phenomena.ScalarImplicatures.QuantityDomain.extMeaning n Phenomena.ScalarImplicatures.QuantityDomain.ExtUtterance.all x✝ = (↑x✝ == n)

def Phenomena.ScalarImplicatures.QuantityDomain.allExtUtterances : List ExtUtterance

All extended utterances

Equations

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