Gricean Maxims of Conversation

@cite{grice-1975}

Logic and Conversation. In P. Cole & J.L. Morgan (eds.), Syntax and Semantics 3: Speech Acts, 41–58. Academic Press.

Design

The Cooperative Principle and four maxims are formalized as types, not as behavioral predictions. Behavioral predictions (e.g., "speakers maximize informativity") belong in the implementing frameworks — RSA formalizes Quantity via s1Score, NeoGricean via the Standard Recipe, Dale & Reiter via incremental attribute selection. Study files that test the maxims directly (e.g., @cite{engelhardt-etal-2006}) import this module.

Linking theorems connecting maxims to specific frameworks belong in Comparisons/.

The Quantity Maxim

Grice's Quantity maxim has two sub-maxims:

1. Q1: "Make your contribution as informative as is required (for the current purposes of the exchange)."
2. Q2: "Do not make your contribution more informative than is required."

@cite{engelhardt-etal-2006} showed these behave asymmetrically: Q1 violations (under-description) are penalized in both production and explicit judgment; Q2 violations (over-description) are produced frequently, tolerated explicitly, but detected implicitly via processing costs.

inductive Theories.Pragmatics.GriceanMaxims.Maxim : Type

The four Gricean maxims of conversation.

• quantity : Maxim

  Make your contribution as informative as is required; do not make it more informative than is required.

• quality : Maxim

  Do not say what you believe to be false; do not say that for which you lack adequate evidence.

• relation : Maxim

  Be relevant.

• manner : Maxim

  Avoid obscurity of expression; avoid ambiguity; be brief; be orderly.

instance Theories.Pragmatics.GriceanMaxims.instDecidableEqMaxim : DecidableEq Maxim

Equations

• Theories.Pragmatics.GriceanMaxims.instDecidableEqMaxim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Pragmatics.GriceanMaxims.instBEqMaxim.beq : Maxim → Maxim → Bool

Equations

• Theories.Pragmatics.GriceanMaxims.instBEqMaxim.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Pragmatics.GriceanMaxims.instBEqMaxim : BEq Maxim

Equations

• Theories.Pragmatics.GriceanMaxims.instBEqMaxim = { beq := Theories.Pragmatics.GriceanMaxims.instBEqMaxim.beq }

def Theories.Pragmatics.GriceanMaxims.instReprMaxim.repr : Maxim → Nat → Std.Format

Equations

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

instance Theories.Pragmatics.GriceanMaxims.instReprMaxim : Repr Maxim

Equations

• Theories.Pragmatics.GriceanMaxims.instReprMaxim = { reprPrec := Theories.Pragmatics.GriceanMaxims.instReprMaxim.repr }

inductive Theories.Pragmatics.GriceanMaxims.QuantitySubmaxim : Type

The Quantity maxim decomposes into two independent sub-maxims. Grice (1975) states both; @cite{engelhardt-etal-2006} showed empirically that they are independently violable.

• Q1 : QuantitySubmaxim

  "Make your contribution as informative as is required (for the current purposes of the exchange)."

• Q2 : QuantitySubmaxim

  "Do not make your contribution more informative than is required."

instance Theories.Pragmatics.GriceanMaxims.instDecidableEqQuantitySubmaxim : DecidableEq QuantitySubmaxim

Equations

• Theories.Pragmatics.GriceanMaxims.instDecidableEqQuantitySubmaxim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Pragmatics.GriceanMaxims.instBEqQuantitySubmaxim.beq : QuantitySubmaxim → QuantitySubmaxim → Bool

Equations

• Theories.Pragmatics.GriceanMaxims.instBEqQuantitySubmaxim.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Pragmatics.GriceanMaxims.instBEqQuantitySubmaxim : BEq QuantitySubmaxim

Equations

• Theories.Pragmatics.GriceanMaxims.instBEqQuantitySubmaxim = { beq := Theories.Pragmatics.GriceanMaxims.instBEqQuantitySubmaxim.beq }

instance Theories.Pragmatics.GriceanMaxims.instReprQuantitySubmaxim : Repr QuantitySubmaxim

Equations

• Theories.Pragmatics.GriceanMaxims.instReprQuantitySubmaxim = { reprPrec := Theories.Pragmatics.GriceanMaxims.instReprQuantitySubmaxim.repr }

def Theories.Pragmatics.GriceanMaxims.instReprQuantitySubmaxim.repr : QuantitySubmaxim → Nat → Std.Format

Equations

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

inductive Theories.Pragmatics.GriceanMaxims.QuantityViolation : Type

Direction of a Quantity violation.

• underInformative : QuantityViolation

  Too little information (violates Q1). E.g., "the apple" when two apples are present.

• overInformative : QuantityViolation

  Too much information (violates Q2). E.g., "the red apple" when only one apple is present.

instance Theories.Pragmatics.GriceanMaxims.instDecidableEqQuantityViolation : DecidableEq QuantityViolation

Equations

• Theories.Pragmatics.GriceanMaxims.instDecidableEqQuantityViolation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Pragmatics.GriceanMaxims.instBEqQuantityViolation.beq : QuantityViolation → QuantityViolation → Bool

Equations

• Theories.Pragmatics.GriceanMaxims.instBEqQuantityViolation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Pragmatics.GriceanMaxims.instBEqQuantityViolation : BEq QuantityViolation

Equations

• Theories.Pragmatics.GriceanMaxims.instBEqQuantityViolation = { beq := Theories.Pragmatics.GriceanMaxims.instBEqQuantityViolation.beq }

instance Theories.Pragmatics.GriceanMaxims.instReprQuantityViolation : Repr QuantityViolation

Equations

• Theories.Pragmatics.GriceanMaxims.instReprQuantityViolation = { reprPrec := Theories.Pragmatics.GriceanMaxims.instReprQuantityViolation.repr }

def Theories.Pragmatics.GriceanMaxims.instReprQuantityViolation.repr : QuantityViolation → Nat → Std.Format

Equations

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

def Theories.Pragmatics.GriceanMaxims.QuantityViolation.submaxim : QuantityViolation → QuantitySubmaxim

Which sub-maxim a violation direction targets.

Equations

• Theories.Pragmatics.GriceanMaxims.QuantityViolation.underInformative.submaxim = Theories.Pragmatics.GriceanMaxims.QuantitySubmaxim.Q1
• Theories.Pragmatics.GriceanMaxims.QuantityViolation.overInformative.submaxim = Theories.Pragmatics.GriceanMaxims.QuantitySubmaxim.Q2

theorem Theories.Pragmatics.GriceanMaxims.violations_independent : QuantityViolation.underInformative.submaxim ≠ QuantityViolation.overInformative.submaxim

The two violation directions target different sub-maxims.