Implicature Theory

Abstract interface for scalar implicature predictions.

inductive Interfaces.ImplicatureStatus : Type

The possible implicature outcomes for a scalar position.

• triggered : ImplicatureStatus

  Implicature is derived (Bel_S(¬ψ) or P > threshold)

• possible : ImplicatureStatus

  Implicature is available but not required

• blocked : ImplicatureStatus

  Implicature is blocked (DE context, no competence)

• absent : ImplicatureStatus

  No scalar item / irrelevant position

instance Interfaces.instReprImplicatureStatus : Repr ImplicatureStatus

Equations

• Interfaces.instReprImplicatureStatus = { reprPrec := Interfaces.instReprImplicatureStatus.repr }

def Interfaces.instReprImplicatureStatus.repr : ImplicatureStatus → Nat → Std.Format

Equations

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

instance Interfaces.instDecidableEqImplicatureStatus : DecidableEq ImplicatureStatus

Equations

• Interfaces.instDecidableEqImplicatureStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

class Interfaces.ImplicatureTheory (T : Type) : Type 1

A theory that makes predictions about scalar implicatures.

• Structure : Type

  The theory's internal representation of an utterance in context

• parse : List Word → Option (Structure T)

  Parse words into the theory's representation. Returns none if the theory can't parse this input.

• implicatureStatus : Structure T → Nat → ImplicatureStatus

  Predict the implicature status for a scalar position.

  Position indexes into the word list:

  • "some students sleep" → position 0 = some (scalar item)

  Returns the theory's prediction about whether an implicature arises.

• implicatureStrength : Structure T → Nat → Option Nat

  Optional: strength/probability (0-100 scale).

  NeoGricean: baseline rate (e.g., 35% for contextualism) RSA: L1 probability converted to percentage

  Returns none if the theory doesn't provide quantitative predictions.

• predictsDEBlocking : Bool

  Does the theory predict implicature blocked in downward-entailing contexts?

• predictsTaskEffect : Bool

  Does the theory predict a task effect (asking about SI raises rate)?

• predictedBaselineRate : Nat

  Predicted baseline implicature rate (%) in neutral contexts

def Interfaces.derivesImplicature {T : Type} [ImplicatureTheory T] (s : ImplicatureTheory.Structure T) (pos : Nat) : Bool

Check if implicature is derived at position pos

Equations

• Interfaces.derivesImplicature s pos = match Interfaces.ImplicatureTheory.implicatureStatus s pos with | Interfaces.ImplicatureStatus.triggered => true | x => false

def Interfaces.blocksImplicature {T : Type} [ImplicatureTheory T] (s : ImplicatureTheory.Structure T) (pos : Nat) : Bool

Check if implicature is blocked at position pos

Equations

• Interfaces.blocksImplicature s pos = match Interfaces.ImplicatureTheory.implicatureStatus s pos with | Interfaces.ImplicatureStatus.blocked => true | x => false

def Interfaces.possibleImplicature {T : Type} [ImplicatureTheory T] (s : ImplicatureTheory.Structure T) (pos : Nat) : Bool

Check if implicature is possible (but not required) at position pos

Equations

• Interfaces.possibleImplicature s pos = match Interfaces.ImplicatureTheory.implicatureStatus s pos with | Interfaces.ImplicatureStatus.possible => true | x => false

def Interfaces.anyImplicature {T : Type} [ImplicatureTheory T] (s : ImplicatureTheory.Structure T) (pos : Nat) : Bool

Check if any implicature arises (triggered or possible) at position pos

Equations

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

def Interfaces.theoriesAgreeOnStatus {T1 T2 : Type} [ImplicatureTheory T1] [ImplicatureTheory T2] (ws : List Word) (pos : Nat) : Bool

Two theories agree on a sentence at a position if they make the same status prediction

Equations

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

def Interfaces.theoriesAgreeOnDerivation {T1 T2 : Type} [ImplicatureTheory T1] [ImplicatureTheory T2] (ws : List Word) (pos : Nat) : Bool

Two theories agree on whether an implicature is derived

Equations

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

def Interfaces.theoriesAgreeOnDEPrediction {T1 T2 : Type} [ImplicatureTheory T1] [ImplicatureTheory T2] : Bool

Two theories agree on DE blocking prediction

Equations

• Interfaces.theoriesAgreeOnDEPrediction = (Interfaces.ImplicatureTheory.predictsDEBlocking T1 == Interfaces.ImplicatureTheory.predictsDEBlocking T2)

def Interfaces.theoriesAgreeOnTaskEffect {T1 T2 : Type} [ImplicatureTheory T1] [ImplicatureTheory T2] : Bool

Two theories agree on task effect prediction

Equations

• Interfaces.theoriesAgreeOnTaskEffect = (Interfaces.ImplicatureTheory.predictsTaskEffect T1 == Interfaces.ImplicatureTheory.predictsTaskEffect T2)

def Interfaces.rateMatchesData (predictedRate observedRate : Nat) (tolerance : Nat := 5) : Bool

Compare a theory's predicted rate to empirical data.

Equations

• Interfaces.rateMatchesData predictedRate observedRate tolerance = decide ((if predictedRate > observedRate then predictedRate - observedRate else observedRate - predictedRate) ≤ tolerance)

def Interfaces.closerToData {T1 T2 : Type} [ImplicatureTheory T1] [ImplicatureTheory T2] (observed : Nat) : Bool

Which theory's baseline is closer to observed data?

Equations

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

inductive Interfaces.CoverageStatus : Type

Coverage status for a phenomenon.

• complete : CoverageStatus
• incomplete : CoverageStatus
• outOfScope : CoverageStatus
• wrong : CoverageStatus

instance Interfaces.instReprCoverageStatus : Repr CoverageStatus

Equations

• Interfaces.instReprCoverageStatus = { reprPrec := Interfaces.instReprCoverageStatus.repr }

def Interfaces.instReprCoverageStatus.repr : CoverageStatus → Nat → Std.Format

Equations

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

instance Interfaces.instDecidableEqCoverageStatus : DecidableEq CoverageStatus

Equations

• Interfaces.instDecidableEqCoverageStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Interfaces.instBEqCoverageStatus : BEq CoverageStatus

Equations

• Interfaces.instBEqCoverageStatus = { beq := Interfaces.instBEqCoverageStatus.beq }

def Interfaces.instBEqCoverageStatus.beq : CoverageStatus → CoverageStatus → Bool

Equations

• Interfaces.instBEqCoverageStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Interfaces.PragmaticPhenomenon : Type

Pragmatic phenomena that theories might cover

• scalarImplicature : PragmaticPhenomenon
• deBlocking : PragmaticPhenomenon
• taskEffect : PragmaticPhenomenon
• referenceGames : PragmaticPhenomenon
• knowledgeCancellation : PragmaticPhenomenon
• exhaustivity : PragmaticPhenomenon
• freeChoice : PragmaticPhenomenon

def Interfaces.instReprPragmaticPhenomenon.repr : PragmaticPhenomenon → Nat → Std.Format

Equations

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

instance Interfaces.instReprPragmaticPhenomenon : Repr PragmaticPhenomenon

Equations

• Interfaces.instReprPragmaticPhenomenon = { reprPrec := Interfaces.instReprPragmaticPhenomenon.repr }

instance Interfaces.instDecidableEqPragmaticPhenomenon : DecidableEq PragmaticPhenomenon

Equations

• Interfaces.instDecidableEqPragmaticPhenomenon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Interfaces.instBEqPragmaticPhenomenon.beq : PragmaticPhenomenon → PragmaticPhenomenon → Bool

Equations

• Interfaces.instBEqPragmaticPhenomenon.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instBEqPragmaticPhenomenon : BEq PragmaticPhenomenon

Equations

• Interfaces.instBEqPragmaticPhenomenon = { beq := Interfaces.instBEqPragmaticPhenomenon.beq }

structure Interfaces.PhenomenonCoverage : Type

Coverage report for a single phenomenon

• phenomenon : PragmaticPhenomenon
• status : CoverageStatus
• notes : String

def Interfaces.instReprPhenomenonCoverage.repr : PhenomenonCoverage → Nat → Std.Format

Equations

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

instance Interfaces.instReprPhenomenonCoverage : Repr PhenomenonCoverage

Equations

• Interfaces.instReprPhenomenonCoverage = { reprPrec := Interfaces.instReprPhenomenonCoverage.repr }

structure Interfaces.TheoryCoverage : Type

Full coverage report for a theory

• theoryName : String
• phenomena : List PhenomenonCoverage

instance Interfaces.instReprTheoryCoverage : Repr TheoryCoverage

Equations

• Interfaces.instReprTheoryCoverage = { reprPrec := Interfaces.instReprTheoryCoverage.repr }

def Interfaces.instReprTheoryCoverage.repr : TheoryCoverage → Nat → Std.Format

Equations

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

def Interfaces.TheoryCoverage.statusFor (tc : TheoryCoverage) (p : PragmaticPhenomenon) : Option CoverageStatus

Get status for a phenomenon (helper)

Equations

• tc.statusFor p = Option.map (fun (x : Interfaces.PhenomenonCoverage) => x.status) (List.find? (fun (x : Interfaces.PhenomenonCoverage) => x.phenomenon == p) tc.phenomena)

def Interfaces.TheoryCoverage.countByStatus (tc : TheoryCoverage) (s : CoverageStatus) : Nat

Count phenomena by status

Equations

• tc.countByStatus s = (List.filter (fun (x : Interfaces.PhenomenonCoverage) => x.status == s) tc.phenomena).length

def Interfaces.TheoryCoverage.incompletePhenomena (tc : TheoryCoverage) : List PragmaticPhenomenon

List incomplete phenomena

Equations

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

def Interfaces.TheoryCoverage.outOfScopePhenomena (tc : TheoryCoverage) : List PragmaticPhenomenon

List out-of-scope phenomena

Equations

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

structure Interfaces.CoverageSummary : Type

Summary of what a theory covers vs what's incomplete.

• derivesBasicSI : Bool

  Does it derive basic SIs?

• modelsDEBlocking : Bool

  Does it model DE blocking?

• modelsTaskEffect : Bool

  Does it model task effects?

• hasBaselineRate : Bool

  Is baseline rate specified?

• incompleteNotes : List String

  Notes about incompleteness

def Interfaces.instReprCoverageSummary.repr : CoverageSummary → Nat → Std.Format

Equations

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

instance Interfaces.instReprCoverageSummary : Repr CoverageSummary

Equations

• Interfaces.instReprCoverageSummary = { reprPrec := Interfaces.instReprCoverageSummary.repr }

def Interfaces.coverageSummary (T : Type) [ImplicatureTheory T] : CoverageSummary

Generate coverage summary for a theory

Equations

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

structure Interfaces.DEBlockingTestCase : Type

A DE blocking test case derived from empirical data.

• ueDescription : String

  Description of the UE example

• deDescription : String

  Description of the DE example

• scalarTerm : String

  The scalar term

• expectedUE : Bool

  Expected: implicature arises in UE

• expectedDE : Bool

  Expected: implicature blocked in DE

def Interfaces.instReprDEBlockingTestCase.repr : DEBlockingTestCase → Nat → Std.Format

Equations

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

instance Interfaces.instReprDEBlockingTestCase : Repr DEBlockingTestCase

Equations

• Interfaces.instReprDEBlockingTestCase = { reprPrec := Interfaces.instReprDEBlockingTestCase.repr }

structure Interfaces.TaskEffectTestCase : Type

A task effect test case from @cite{geurts-pouscoulous-2009}

• inferenceRate : Nat

  Inference task rate (percentage)

• verificationRate : Nat

  Verification task rate (percentage)

• significant : Bool

  Is the difference significant?

instance Interfaces.instReprTaskEffectTestCase : Repr TaskEffectTestCase

Equations

• Interfaces.instReprTaskEffectTestCase = { reprPrec := Interfaces.instReprTaskEffectTestCase.repr }

def Interfaces.instReprTaskEffectTestCase.repr : TaskEffectTestCase → Nat → Std.Format

Equations

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

structure Interfaces.DEBlockingResult : Type

Result of testing a theory against DE blocking data

• theoryPredictsDEBlocking : Bool

  Does the theory predict DE blocking?

• datashowsDEBlocking : Bool

  Does the data show DE blocking?

• isMatch : Bool

  Do they match?

instance Interfaces.instReprDEBlockingResult : Repr DEBlockingResult

Equations

• Interfaces.instReprDEBlockingResult = { reprPrec := Interfaces.instReprDEBlockingResult.repr }

def Interfaces.instReprDEBlockingResult.repr : DEBlockingResult → Nat → Std.Format

Equations

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

def Interfaces.testDEBlocking {T : Type} [ImplicatureTheory T] (tc : DEBlockingTestCase) : DEBlockingResult

Test a theory against a DE blocking test case

Equations

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

structure Interfaces.TaskEffectResult : Type

Result of testing a theory against task effect data

• theoryPredictsTaskEffect : Bool

  Does the theory predict task effect?

• dataShowsTaskEffect : Bool

  Does the data show task effect?

• predictedRate : Nat

  Theory's predicted baseline rate

• observedRate : Nat

  Observed rate (verification task)

• rateDifference : Nat

  Difference between predicted and observed

• isMatch : Bool

  Does theory match data?

instance Interfaces.instReprTaskEffectResult : Repr TaskEffectResult

Equations

• Interfaces.instReprTaskEffectResult = { reprPrec := Interfaces.instReprTaskEffectResult.repr }

def Interfaces.instReprTaskEffectResult.repr : TaskEffectResult → Nat → Std.Format

Equations

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

def Interfaces.testTaskEffect {T : Type} [ImplicatureTheory T] (tc : TaskEffectTestCase) (tolerance : Nat := 10) : TaskEffectResult

Test a theory against task effect data

Equations

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

class Interfaces.CapturesDEBlockingPattern (T : Type) [ImplicatureTheory T] : Type

A theory captures DE blocking data if its prediction isMatch the pattern.

• testCase : DEBlockingTestCase

  The test case from empirical data

• theoryMatchesData : (testDEBlocking (testCase T)).isMatch = true

  Proof that theory isMatch data

class Interfaces.CapturesTaskEffectData (T : Type) [ImplicatureTheory T] : Type

A theory captures task effect data if its predictions match the observations

• taskEffectData : TaskEffectTestCase

  The task effect data

• tolerance : Nat

  Tolerance for rate matching

• taskEffectMatches : ((testTaskEffect (taskEffectData T) (tolerance T)).theoryPredictsTaskEffect == (testTaskEffect (taskEffectData T) (tolerance T)).dataShowsTaskEffect) = true

  Proof that theory isMatch task effect pattern

• rateWithinTolerance : (testTaskEffect (taskEffectData T) (tolerance T)).rateDifference ≤ tolerance T

  Proof that predicted rate is close to observed

def Interfaces.compareToObservedRate {T : Type} [ImplicatureTheory T] (observedRate : Nat) : Nat × Nat × Bool

Compare a theory's baseline rate to observed data.

Equations

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

def Interfaces.closerToObservedRate {T1 T2 : Type} [ImplicatureTheory T1] [ImplicatureTheory T2] (observedRate : Nat) : Bool × Bool

Which of two theories is closer to observed rate?

Equations

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