inductive NeoGricean.Alternatives.AlternativeType : Type

Types of pragmatic alternatives.

Following @cite{horn-1984} and @cite{levinson-2000}:

• Q-alternatives: Compete on informativity (Quantity principle)
• M-alternatives: Compete on form cost (Manner principle)

These generate different types of implicatures via different mechanisms.

• quantity : AlternativeType
• manner : AlternativeType

def NeoGricean.Alternatives.instReprAlternativeType.repr : AlternativeType → ℕ → Std.Format

Equations

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

instance NeoGricean.Alternatives.instReprAlternativeType : Repr AlternativeType

Equations

• NeoGricean.Alternatives.instReprAlternativeType = { reprPrec := NeoGricean.Alternatives.instReprAlternativeType.repr }

instance NeoGricean.Alternatives.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

• NeoGricean.Alternatives.instDecidableEqAlternativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NeoGricean.Alternatives.instBEqAlternativeType : BEq AlternativeType

Equations

• NeoGricean.Alternatives.instBEqAlternativeType = { beq := NeoGricean.Alternatives.instBEqAlternativeType.beq }

def NeoGricean.Alternatives.instBEqAlternativeType.beq : AlternativeType → AlternativeType → Bool

Equations

• NeoGricean.Alternatives.instBEqAlternativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure NeoGricean.Alternatives.PragmaticAlternative : Type

A unified pragmatic alternative.

Captures both Q-alternatives and M-alternatives with their relevant properties.

• altType : AlternativeType

  Type of alternative (Q vs M)

• form : String

  The alternative form

• originalForm : String

  The original form being compared to

• isBetter : Bool

  Is this alternative "better" (stronger for Q, cheaper for M)?

• explanation : String

  Explanation of the comparison

def NeoGricean.Alternatives.instReprPragmaticAlternative.repr : PragmaticAlternative → ℕ → Std.Format

Equations

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

instance NeoGricean.Alternatives.instReprPragmaticAlternative : Repr PragmaticAlternative

Equations

• NeoGricean.Alternatives.instReprPragmaticAlternative = { reprPrec := NeoGricean.Alternatives.instReprPragmaticAlternative.repr }

structure NeoGricean.Alternatives.HornSet (α : Type) : Type

A Horn Set is an unordered collection of expressions.

Following Geurts' argument on p.58, we use sets not scales. The ordering (which term is stronger) is determined at the SENTENCE level by checking semantic entailment, not by a fixed word-level ordering.

This is crucial for handling DE contexts correctly:

• In UE context: "all" → "some" (all stronger)
• In DE context: "some" → "all" (some stronger!)

The same Horn set {some, all} works for both contexts.

• members : List α

  The members of the Horn set

def NeoGricean.Alternatives.instReprHornSet.repr {α✝ : Type} [Repr α✝] : HornSet α✝ → ℕ → Std.Format

Equations

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

instance NeoGricean.Alternatives.instReprHornSet {α✝ : Type} [Repr α✝] : Repr (HornSet α✝)

Equations

• NeoGricean.Alternatives.instReprHornSet = { reprPrec := NeoGricean.Alternatives.instReprHornSet.repr }

def NeoGricean.Alternatives.HornSet.contains {α : Type} [BEq α] (h : HornSet α) (x : α) : Bool

Check if a term is in a Horn set.

Equations

• h.contains x = h.members.contains x

def NeoGricean.Alternatives.HornSet.otherMembers {α : Type} [BEq α] (h : HornSet α) (x : α) : List α

Get all other members of a Horn set (potential alternatives).

Equations

• h.otherMembers x = List.filter (fun (x_1 : α) => x_1 != x) h.members

def NeoGricean.Alternatives.quantifierSet : HornSet Core.Scale.Quantifiers.QuantExpr

The quantifier Horn set: {some, most, all}

Uses type-safe QuantExpr from Core.Scale. Note: This is a SET, not an ordered scale. The ordering comes from sentence-level semantics, not from this data structure.

Equations

• NeoGricean.Alternatives.quantifierSet = { members := [Core.Scale.Quantifiers.QuantExpr.some_, Core.Scale.Quantifiers.QuantExpr.most, Core.Scale.Quantifiers.QuantExpr.all] }

def NeoGricean.Alternatives.connectiveSet : HornSet Core.Scale.Connectives.ConnExpr

The connective Horn set: {or, and}

Equations

• NeoGricean.Alternatives.connectiveSet = { members := [Core.Scale.Connectives.ConnExpr.or_, Core.Scale.Connectives.ConnExpr.and_] }

def NeoGricean.Alternatives.modalSet : HornSet Core.Scale.Modals.ModalExpr

The modal Horn set: {possible, necessary}

Equations

• NeoGricean.Alternatives.modalSet = { members := [Core.Scale.Modals.ModalExpr.possible, Core.Scale.Modals.ModalExpr.necessary] }

def NeoGricean.Alternatives.numeralSet : HornSet String

The numeral Horn set: {one, two, three,...} Uses strings for now (numerals are more complex).

Equations

• NeoGricean.Alternatives.numeralSet = { members := ["one", "two", "three", "four", "five"] }

structure NeoGricean.Alternatives.SentenceContext : Type

A sentence context for alternative generation.

What counts as a "stronger alternative" depends on the polarity of the context, not just the Horn set.

• polarity : Core.NaturalLogic.ContextPolarity

  The polarity of this context

• description : String

  Description of the context

instance NeoGricean.Alternatives.instReprSentenceContext : Repr SentenceContext

Equations

• NeoGricean.Alternatives.instReprSentenceContext = { reprPrec := NeoGricean.Alternatives.instReprSentenceContext.repr }

def NeoGricean.Alternatives.instReprSentenceContext.repr : SentenceContext → ℕ → Std.Format

Equations

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

def NeoGricean.Alternatives.simpleAssertion : SentenceContext

Common UE context: simple assertion

Equations

• NeoGricean.Alternatives.simpleAssertion = { polarity := Core.NaturalLogic.ContextPolarity.upward, description := "Simple assertion (e.g., 'John ate ___')" }

def NeoGricean.Alternatives.underNegation : SentenceContext

Common DE context: under negation

Equations

• NeoGricean.Alternatives.underNegation = { polarity := Core.NaturalLogic.ContextPolarity.downward, description := "Under negation (e.g., 'No one ate ___')" }

def NeoGricean.Alternatives.universalRestrictor : SentenceContext

DE context: restrictor of universal

Equations

• NeoGricean.Alternatives.universalRestrictor = { polarity := Core.NaturalLogic.ContextPolarity.downward, description := "Restrictor of 'every' (e.g., 'Every student who ate ___')" }

structure NeoGricean.Alternatives.Alternative (α : Type) : Type

An alternative utterance with its source term and context.

• term : α

  The alternative term from the Horn set

• isStrongerInContext : Bool

  Whether this is a stronger alternative in context

def NeoGricean.Alternatives.instReprAlternative.repr {α✝ : Type} [Repr α✝] : Alternative α✝ → ℕ → Std.Format

Equations

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

instance NeoGricean.Alternatives.instReprAlternative {α✝ : Type} [Repr α✝] : Repr (Alternative α✝)

Equations

• NeoGricean.Alternatives.instReprAlternative = { reprPrec := NeoGricean.Alternatives.instReprAlternative.repr }

structure NeoGricean.Alternatives.EntailmentChecker (α : Type) : Type

Abstract entailment checker for sentences.

In a real implementation, this would check semantic entailment. Here we use a simple model based on polarity.

• isStronger : Core.NaturalLogic.ContextPolarity → α → α → Bool

  Check if term1 produces a stronger sentence than term2 in context

def NeoGricean.Alternatives.generateAlternatives {α : Type} [BEq α] (hornSet : HornSet α) (checker : EntailmentChecker α) (context : SentenceContext) (term : α) : List (Alternative α)

Generate alternatives to a term using a Horn set and entailment checker.

Equations

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

def NeoGricean.Alternatives.strongerAlternatives {α : Type} [BEq α] (hornSet : HornSet α) (checker : EntailmentChecker α) (context : SentenceContext) (term : α) : List α

Get only the stronger alternatives (the ones that generate implicatures).

Equations

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

def NeoGricean.Alternatives.quantifierStrengthUE (q1 q2 : Core.Scale.Quantifiers.QuantExpr) : Bool

Standard quantifier strength ordering (for UE contexts).

Uses QuantExpr.entails from Core.Scale:

• all > most > some (in terms of logical strength)
• "all" entails "some", so "all" is stronger

Equations

• NeoGricean.Alternatives.quantifierStrengthUE q1 q2 = (Core.Scale.Quantifiers.entails q1 q2 && q1 != q2)

def NeoGricean.Alternatives.quantifierStrengthDE (q1 q2 : Core.Scale.Quantifiers.QuantExpr) : Bool

Reversed quantifier strength (for DE contexts).

In DE context, "some" is stronger than "all" at sentence level. "No one ate some" entails "No one ate all".

Equations

• NeoGricean.Alternatives.quantifierStrengthDE q1 q2 = (Core.Scale.Quantifiers.entails q2 q1 && q1 != q2)

def NeoGricean.Alternatives.quantifierChecker : EntailmentChecker Core.Scale.Quantifiers.QuantExpr

Entailment checker for quantifiers (type-safe).

Grounded in Core.Scale.Quantifiers.entails.

Equations

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

def NeoGricean.Alternatives.connectiveStrengthUE (c1 c2 : Core.Scale.Connectives.ConnExpr) : Bool

Connective strength in UE context. "and" is stronger than "or".

Equations

• NeoGricean.Alternatives.connectiveStrengthUE c1 c2 = (Core.Scale.Connectives.entails c1 c2 && c1 != c2)

def NeoGricean.Alternatives.connectiveStrengthDE (c1 c2 : Core.Scale.Connectives.ConnExpr) : Bool

Connective strength in DE context (reversed).

Equations

• NeoGricean.Alternatives.connectiveStrengthDE c1 c2 = (Core.Scale.Connectives.entails c2 c1 && c1 != c2)

def NeoGricean.Alternatives.connectiveChecker : EntailmentChecker Core.Scale.Connectives.ConnExpr

Entailment checker for connectives (type-safe).

Equations

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

theorem NeoGricean.Alternatives.some_alternatives_ue : strongerAlternatives quantifierSet quantifierChecker simpleAssertion Core.Scale.Quantifiers.QuantExpr.some_ = [Core.Scale.Quantifiers.QuantExpr.most, Core.Scale.Quantifiers.QuantExpr.all]

"some" has stronger alternatives in UE context.

In UE context, "all" and "most" are stronger than "some".

theorem NeoGricean.Alternatives.some_no_alternatives_de : strongerAlternatives quantifierSet quantifierChecker underNegation Core.Scale.Quantifiers.QuantExpr.some_ = []

"some" has no stronger alternatives in DE context.

In DE context, "some" is already the strongest term. This explains why "not all" implicature is blocked in DE contexts.

theorem NeoGricean.Alternatives.all_alternatives_de : strongerAlternatives quantifierSet quantifierChecker underNegation Core.Scale.Quantifiers.QuantExpr.all = [Core.Scale.Quantifiers.QuantExpr.some_, Core.Scale.Quantifiers.QuantExpr.most]

"all" has stronger alternatives in DE context.

In DE context, "some" is stronger than "all" at sentence level.

theorem NeoGricean.Alternatives.context_determines_alternatives : strongerAlternatives quantifierSet quantifierChecker simpleAssertion Core.Scale.Quantifiers.QuantExpr.some_ ≠ strongerAlternatives quantifierSet quantifierChecker underNegation Core.Scale.Quantifiers.QuantExpr.some_

Context determines alternatives.

The same Horn set produces different alternatives depending on context.

def NeoGricean.Alternatives.fromHornScale {α : Type} (scale : Core.Scale.HornScale α) : HornSet α

Convert a HornScale (from Core.Scale) to a HornSet.

This allows us to reuse the scale definitions while treating them as unordered sets. The ordering comes from the SentenceContext.

Equations

• NeoGricean.Alternatives.fromHornScale scale = { members := scale.members }

def NeoGricean.Alternatives.quantifierCheckerString : EntailmentChecker String

String-based quantifier checker for interface with syntax.

Converts strings to QuantExpr, then uses the type-safe checker.

Equations

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

def NeoGricean.Alternatives.connectiveCheckerString : EntailmentChecker String

String-based connective checker for interface with syntax.

Equations

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

def NeoGricean.Alternatives.quantifierSetString : HornSet String

String-based quantifier set for interface with syntax.

Equations

• NeoGricean.Alternatives.quantifierSetString = { members := ["some", "most", "all"] }

def NeoGricean.Alternatives.connectiveSetString : HornSet String

String-based connective set for interface with syntax.

Equations

• NeoGricean.Alternatives.connectiveSetString = { members := ["or", "and"] }

inductive NeoGricean.Alternatives.PolarVariance : Type

Polar variance: do antonyms have the same truth conditions in this construction?

This determines whether M-alternatives exist:

• Polar-VARIANT: "taller than" ≠ "shorter than" → no M-alternatives
• Polar-INVARIANT: "as tall as" = "as short as" → M-alternatives exist

From @cite{rett-2015} Chapter 5.

• variant : PolarVariance
• invariant : PolarVariance

instance NeoGricean.Alternatives.instReprPolarVariance : Repr PolarVariance

Equations

• NeoGricean.Alternatives.instReprPolarVariance = { reprPrec := NeoGricean.Alternatives.instReprPolarVariance.repr }

def NeoGricean.Alternatives.instReprPolarVariance.repr : PolarVariance → ℕ → Std.Format

Equations

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

instance NeoGricean.Alternatives.instDecidableEqPolarVariance : DecidableEq PolarVariance

Equations

• NeoGricean.Alternatives.instDecidableEqPolarVariance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.Alternatives.instBEqPolarVariance.beq : PolarVariance → PolarVariance → Bool

Equations

• NeoGricean.Alternatives.instBEqPolarVariance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Alternatives.instBEqPolarVariance : BEq PolarVariance

Equations

• NeoGricean.Alternatives.instBEqPolarVariance = { beq := NeoGricean.Alternatives.instBEqPolarVariance.beq }

def NeoGricean.Alternatives.polarVariance : Semantics.Degree.AdjectivalConstruction → PolarVariance

Polar variance by adjectival construction type.

Equations

• NeoGricean.Alternatives.polarVariance Semantics.Degree.AdjectivalConstruction.positive = NeoGricean.Alternatives.PolarVariance.variant
• NeoGricean.Alternatives.polarVariance Semantics.Degree.AdjectivalConstruction.comparative = NeoGricean.Alternatives.PolarVariance.variant
• NeoGricean.Alternatives.polarVariance Semantics.Degree.AdjectivalConstruction.equative = NeoGricean.Alternatives.PolarVariance.invariant
• NeoGricean.Alternatives.polarVariance Semantics.Degree.AdjectivalConstruction.degreeQuestion = NeoGricean.Alternatives.PolarVariance.invariant
• NeoGricean.Alternatives.polarVariance Semantics.Degree.AdjectivalConstruction.measurePhrase = NeoGricean.Alternatives.PolarVariance.variant

structure NeoGricean.Alternatives.MAlternativeSet : Type

An M-alternative set: forms differing in cost but not truth conditions.

Unlike Q-alternatives (which differ in informativity), M-alternatives are EQUIVALENT in meaning but differ in production cost.

• marked : String

  The marked (costlier) form

• unmarked : String

  The unmarked (cheaper) form

• dimension : Core.Dimension

  The dimension they share (e.g., .height)

• costDifference : ℚ

  The cost difference between forms

• construction : Semantics.Degree.AdjectivalConstruction

  Construction where they're equivalent

def NeoGricean.Alternatives.instReprMAlternativeSet.repr : MAlternativeSet → ℕ → Std.Format

Equations

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

instance NeoGricean.Alternatives.instReprMAlternativeSet : Repr MAlternativeSet

Equations

• NeoGricean.Alternatives.instReprMAlternativeSet = { reprPrec := NeoGricean.Alternatives.instReprMAlternativeSet.repr }

instance NeoGricean.Alternatives.instBEqMAlternativeSet : BEq MAlternativeSet

Equations

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

def NeoGricean.Alternatives.generateMAlternatives (adj1 adj2 : Markedness.GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) : Option MAlternativeSet

Generate M-alternatives from an antonym pair.

M-alternatives are generated when:

1. The construction is polar-invariant (antonyms semantically equivalent)
2. Markedness can be determined for the pair

Returns none if no M-alternatives exist.

Equations

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

def NeoGricean.Alternatives.isMarkedInMAlternatives (form : String) (adj1 adj2 : Markedness.GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) : Bool

Check if a form is the marked member of an M-alternative pair.

Equations

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

def NeoGricean.Alternatives.getMAlternative (form : String) (adj1 adj2 : Markedness.GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) : Option String

Get the M-alternative for a form (if any).

Equations

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

def NeoGricean.Alternatives.generateAllAlternatives (form : String) (adj1 adj2 : Markedness.GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) (context : SentenceContext) : List PragmaticAlternative

Generate all pragmatic alternatives (both Q and M) for a form.

This is the unified entry point for alternative generation.

Equations

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

def NeoGricean.Alternatives.alternativeComparison : String

Key distinction between Q-alternatives and M-alternatives.

Equations

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