Generic Scalar Implicature Helpers

@cite{geurts-2010}

Generic scalar-implicature computation built on HornScale (from Theories/Semantics/Alternatives/Lexical.lean) and contextual polarity (from Theories/Semantics/Entailment/Polarity.lean).

Key operations

• scaleAlternatives: filter Horn-scale members by polarity, returning the context-appropriate alternatives (UE: stronger; DE: weaker; NM: none).
• quantImplicatureArises: does a particular alternative arise as a scalar implicature for a given quantifier in context?
• deriveScalarImplicatures / deriveFromWords / hasImplicature: produce the negation-of-stronger-alternative implicatures from a scalar term and scan a word list for them.

Scope

Generic infrastructure only — no paper-specific worked examples. Worked examples live in the Phenomena/ScalarImplicatures/Studies/*.lean files that exercise this API.

Scale semantics (SemanticScale, HurfordSemantic, SinghSemantic) and exhaustification predictions live in Alternatives/Lexical.lean and Exhaustification/ScalePredictions.lean.

def Implicature.Scales.scaleAlternatives (sm : Alternatives.ScaleMembership) (ctx : Core.NaturalLogic.ContextPolarity) : List String

Get scalar alternatives for a scale member in context. Delegates to HornScale members filtered by semantic entailment, polarity-aware.

Equations

• Implicature.Scales.scaleAlternatives (Alternatives.ScaleMembership.quantifier pos) ctx = Implicature.Scales.filterAlts✝ Alternatives.Quantifiers.quantScale pos Alternatives.Quantifiers.entails ctx
• Implicature.Scales.scaleAlternatives (Alternatives.ScaleMembership.connective pos) ctx = Implicature.Scales.filterAlts✝ Alternatives.Connectives.connScale pos Alternatives.Connectives.entails ctx
• Implicature.Scales.scaleAlternatives (Alternatives.ScaleMembership.modal pos) ctx = Implicature.Scales.filterAlts✝ Alternatives.Modals.modalScale pos Alternatives.Modals.entails ctx

def Implicature.Scales.QuantImplicatureArises (term alt : Alternatives.Quantifiers.QuantExpr) (ctx : Core.NaturalLogic.ContextPolarity) : Prop

Does an alternative arise as a scalar implicature of a quantifier term? True iff alt is among the polarity-appropriate Horn-scale alternatives of term.

Equations

• Implicature.Scales.QuantImplicatureArises term alt ctx = (toString alt ∈ Implicature.Scales.scaleAlternatives (Alternatives.ScaleMembership.quantifier term) ctx)

@[implicit_reducible]

instance Implicature.Scales.instDecidableQuantImplicatureArises (term alt : Alternatives.Quantifiers.QuantExpr) (ctx : Core.NaturalLogic.ContextPolarity) : Decidable (QuantImplicatureArises term alt ctx)

Equations

• Implicature.Scales.instDecidableQuantImplicatureArises term alt ctx = Implicature.Scales.instDecidableQuantImplicatureArises._aux_1 term alt ctx

structure Implicature.Scales.ScalarImplicatureResult : Type

Complete scalar implicature derivation result.

• term : String

  The original utterance's scalar term

• strongerAlts : List String

  Stronger alternatives found

• implicatures : List String

  Implicatures derived (negations of stronger alternatives)

@[implicit_reducible]

instance Implicature.Scales.instReprScalarImplicatureResult : Repr ScalarImplicatureResult

Equations

• Implicature.Scales.instReprScalarImplicatureResult = { reprPrec := Implicature.Scales.instReprScalarImplicatureResult.repr }

def Implicature.Scales.instReprScalarImplicatureResult.repr : ScalarImplicatureResult → ℕ → Std.Format

Equations

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

def Implicature.Scales.deriveScalarImplicatures (term : String) (sm : Alternatives.ScaleMembership) (ctx : Core.NaturalLogic.ContextPolarity) : ScalarImplicatureResult

Derive all scalar implicatures for a term via HornScale.

Equations

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

def Implicature.Scales.deriveFromWords (words : List String) (ctx : Core.NaturalLogic.ContextPolarity) : List ScalarImplicatureResult

Derive scalar implicatures from a list of words. Each word is looked up in the scale registry; scalar words produce implicatures based on polarity context.

Equations

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

def Implicature.Scales.HasImplicature (results : List ScalarImplicatureResult) (alt : String) : Prop

Does any implicature in the results negate a given alternative?

Equations

• Implicature.Scales.HasImplicature results alt = ∃ r ∈ results, toString "not(" ++ toString alt ++ toString ")" ∈ r.implicatures

@[implicit_reducible]

instance Implicature.Scales.instDecidableHasImplicature (results : List ScalarImplicatureResult) (alt : String) : Decidable (HasImplicature results alt)

Equations

• Implicature.Scales.instDecidableHasImplicature results alt = Implicature.Scales.instDecidableHasImplicature._aux_1 results alt