Giorgolo & Asudeh 2012: Monads for Conventional Implicatures

@cite{giorgolo-asudeh-2012}

Core Claim

Conventional implicatures are modeled as Writer monad side-effects. CI-contributing expressions (appositives, expressives) log propositions to a side-issue dimension via write, while presupposition triggers log conditions via check. The monadic type structure enforces @cite{potts-2005}'s flow restriction by construction: bind's function argument receives only the at-issue value, never the CI log.

Two-Stage Architecture

1. Compositional phase: at-issue and CI dimensions are separated; Potts's flow restrictions hold (at-issue → CI is one-way).
2. Post-compositional phase: anaphora resolution and presupposition checking can freely access both dimensions.

Two Channels via Monad Transformer (Appendix A)

The analysis requires two Writer monads combined via a monad transformer:

• Inner Writer (CI): accumulates conventional implicature propositions
• Outer Writer (Presupposition): accumulates presuppositional conditions

write and check have the same definition λt.⟨⊥, {t}⟩ (eq. 21) but operate in different monad layers (fn. 4).

Worked Example (§5): "John, who likes cats, likes dogs also."

• At-issue: like(john, dogs)
• CI: {like(john, cats)} — from the NRRC via write
• Presupposition: {∃z. like(john, z) ∧ z ≠ dogs} — from "also" via check

The presupposition is satisfied by the CI content: john likes cats, and cats ≠ dogs. This satisfaction happens post-compositionally, after both Writer logs are exposed.

Relation to @cite{shan-2001}

@cite{shan-2001} showed monads capture deep structure in NL semantics (focus, scope, questions, binding). @cite{giorgolo-asudeh-2012} apply the Writer monad specifically to CIs, arguing it is preferable to the continuation-based approach: each monad isolates one kind of side-effect, and monad transformers compose them modularly.

inductive GiorgoloAsudeh2012.E : Type

• john : E
• cats : E
• dogs : E

@[implicit_reducible]

instance GiorgoloAsudeh2012.instDecidableEqE : DecidableEq E

Equations

• GiorgoloAsudeh2012.instDecidableEqE x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GiorgoloAsudeh2012.instReprE : Repr E

Equations

• GiorgoloAsudeh2012.instReprE = { reprPrec := GiorgoloAsudeh2012.instReprE.repr }

def GiorgoloAsudeh2012.instReprE.repr : E → ℕ → Std.Format

Equations

• GiorgoloAsudeh2012.instReprE.repr GiorgoloAsudeh2012.E.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GiorgoloAsudeh2012.E.john")).group prec✝
• GiorgoloAsudeh2012.instReprE.repr GiorgoloAsudeh2012.E.cats prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GiorgoloAsudeh2012.E.cats")).group prec✝
• GiorgoloAsudeh2012.instReprE.repr GiorgoloAsudeh2012.E.dogs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GiorgoloAsudeh2012.E.dogs")).group prec✝

def GiorgoloAsudeh2012.like (x y : E) : Bool

Equations

• GiorgoloAsudeh2012.like GiorgoloAsudeh2012.E.john GiorgoloAsudeh2012.E.cats = true
• GiorgoloAsudeh2012.like GiorgoloAsudeh2012.E.john GiorgoloAsudeh2012.E.dogs = true
• GiorgoloAsudeh2012.like x y = false

inductive GiorgoloAsudeh2012.CIProp : Type

CI propositions: unevaluated semantic objects logged by write.

• likes : E → E → CIProp

def GiorgoloAsudeh2012.instDecidableEqCIProp.decEq (x✝ x✝¹ : CIProp) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance GiorgoloAsudeh2012.instDecidableEqCIProp : DecidableEq CIProp

Equations

• GiorgoloAsudeh2012.instDecidableEqCIProp = GiorgoloAsudeh2012.instDecidableEqCIProp.decEq

@[implicit_reducible]

instance GiorgoloAsudeh2012.instReprCIProp : Repr CIProp

Equations

• GiorgoloAsudeh2012.instReprCIProp = { reprPrec := GiorgoloAsudeh2012.instReprCIProp.repr }

def GiorgoloAsudeh2012.instReprCIProp.repr : CIProp → ℕ → Std.Format

Equations

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

inductive GiorgoloAsudeh2012.PresupProp : Type

Presuppositional conditions: unevaluated conditions logged by check.

• existsOtherLiked : E → E → PresupProp

  ∃z. like(subj, z) ∧ z ≠ obj — the presupposition of "also"

@[implicit_reducible]

instance GiorgoloAsudeh2012.instDecidableEqPresupProp : DecidableEq PresupProp

Equations

• GiorgoloAsudeh2012.instDecidableEqPresupProp = GiorgoloAsudeh2012.instDecidableEqPresupProp.decEq

def GiorgoloAsudeh2012.instDecidableEqPresupProp.decEq (x✝ x✝¹ : PresupProp) : Decidable (x✝ = x✝¹)

Equations

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

def GiorgoloAsudeh2012.instReprPresupProp.repr : PresupProp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GiorgoloAsudeh2012.instReprPresupProp : Repr PresupProp

Equations

• GiorgoloAsudeh2012.instReprPresupProp = { reprPrec := GiorgoloAsudeh2012.instReprPresupProp.repr }

def GiorgoloAsudeh2012.CIProp.eval : CIProp → Bool

Equations

• (GiorgoloAsudeh2012.CIProp.likes a a_1).eval = GiorgoloAsudeh2012.like a a_1

def GiorgoloAsudeh2012.PresupProp.eval : PresupProp → Bool

Evaluate a presuppositional condition over the finite entity domain.

Equations

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

structure GiorgoloAsudeh2012.TwoChannel (CI : Type u_1) (Presup : Type u_2) (A : Type u_3) : Type (max (max u_1 u_2) u_3)

Two-channel meaning: flattened Writer Presup (Writer CI A).

The outer Writer carries presuppositions; the inner carries conventional implicatures. Figure 1's result type is: ⟨⟨at-issue, {CI-props}⟩, {presup-conditions}⟩

• val : A
• ciLog : List CI
• presupLog : List Presup

def GiorgoloAsudeh2012.TwoChannel.pure {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (a : A) : TwoChannel CI Presup A

Equations

• GiorgoloAsudeh2012.TwoChannel.pure a = { val := a, ciLog := [], presupLog := [] }

def GiorgoloAsudeh2012.TwoChannel.bind {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} {B : Type u_4} (m : TwoChannel CI Presup A) (f : A → TwoChannel CI Presup B) : TwoChannel CI Presup B

Equations

• m.bind f = { val := (f m.val).val, ciLog := m.ciLog ++ (f m.val).ciLog, presupLog := m.presupLog ++ (f m.val).presupLog }

def GiorgoloAsudeh2012.TwoChannel.write {CI : Type u_1} {Presup : Type u_2} (p : CI) : TwoChannel CI Presup Unit

write(t) = ⟨⊥, {t}⟩ (eq. 21): log a proposition to the CI channel.

Equations

• GiorgoloAsudeh2012.TwoChannel.write p = { val := (), ciLog := [p], presupLog := [] }

def GiorgoloAsudeh2012.TwoChannel.check {CI : Type u_1} {Presup : Type u_2} (p : Presup) : TwoChannel CI Presup Unit

check(t) = lift(⟨⊥, {t}⟩) (eq. 21, fn. 4): log a condition to the presupposition channel. Same definition as write, different layer.

Equations

• GiorgoloAsudeh2012.TwoChannel.check p = { val := (), ciLog := [], presupLog := [p] }

@[simp]

theorem GiorgoloAsudeh2012.TwoChannel.pure_val {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (a : A) : (pure a).val = a

@[simp]

theorem GiorgoloAsudeh2012.TwoChannel.pure_ciLog {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (a : A) : (pure a).ciLog = []

@[simp]

theorem GiorgoloAsudeh2012.TwoChannel.pure_presupLog {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (a : A) : (pure a).presupLog = []

@[simp]

theorem GiorgoloAsudeh2012.TwoChannel.bind_val {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} {B : Type u_4} (m : TwoChannel CI Presup A) (f : A → TwoChannel CI Presup B) : (m.bind f).val = (f m.val).val

@[simp]

theorem GiorgoloAsudeh2012.TwoChannel.bind_ciLog {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} {B : Type u_4} (m : TwoChannel CI Presup A) (f : A → TwoChannel CI Presup B) : (m.bind f).ciLog = m.ciLog ++ (f m.val).ciLog

@[simp]

theorem GiorgoloAsudeh2012.TwoChannel.bind_presupLog {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} {B : Type u_4} (m : TwoChannel CI Presup A) (f : A → TwoChannel CI Presup B) : (m.bind f).presupLog = m.presupLog ++ (f m.val).presupLog

def GiorgoloAsudeh2012.ofNestedWriter {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (m : Semantics.Composition.WriterMonad.Writer Presup (Semantics.Composition.WriterMonad.Writer CI A)) : TwoChannel CI Presup A

Equations

• GiorgoloAsudeh2012.ofNestedWriter m = { val := m.val.val, ciLog := m.val.log, presupLog := m.log }

def GiorgoloAsudeh2012.toNestedWriter {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (m : TwoChannel CI Presup A) : Semantics.Composition.WriterMonad.Writer Presup (Semantics.Composition.WriterMonad.Writer CI A)

Equations

• GiorgoloAsudeh2012.toNestedWriter m = { val := { val := m.val, log := m.ciLog }, log := m.presupLog }

theorem GiorgoloAsudeh2012.nested_roundtrip {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (m : TwoChannel CI Presup A) : ofNestedWriter (toNestedWriter m) = m

theorem GiorgoloAsudeh2012.nested_roundtrip_inv {CI : Type u_1} {Presup : Type u_2} {A : Type u_3} (m : Semantics.Composition.WriterMonad.Writer Presup (Semantics.Composition.WriterMonad.Writer CI A)) : toNestedWriter (ofNestedWriter m) = m

All lexical items not introducing CIs or presuppositions are η-lifted: ⟦word⟧ = η(standard-meaning) (Table 1).

def GiorgoloAsudeh2012.commaOp (subj : TwoChannel CIProp PresupProp E) (nrrcPred : TwoChannel CIProp PresupProp (E → CIProp)) : TwoChannel CIProp PresupProp E

comma (Table 1): λj λl. j ⋆ λx. l ⋆ λf. write(f x) ⋆ λ_. η(x)

The prosodic comma introduces NRRC content as CI via write. Both arguments are monadic (⊸* in Glue), matching Table 1's type j ⊸* (j ⊸ l) ⊸* j.

Equations

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

def GiorgoloAsudeh2012.alsoEntry (verb : TwoChannel CIProp PresupProp (E → E → Bool)) (obj subj : TwoChannel CIProp PresupProp E) : TwoChannel CIProp PresupProp Bool

also (Table 1): λv.λo.λs. s ⋆ λx. v ⋆ λf. o ⋆ λy. check(∃z. f z x ∧ z ≠ y) ⋆ λ_. η(f y x)

Takes verb, object, subject (all monadic per ⊸*). Checks the presupposition that the subject verb-s something other than the object, then returns the at-issue content f y x.

Equations

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

def GiorgoloAsudeh2012.john_who_likes_cats : TwoChannel CIProp PresupProp E

"John, who likes cats" — comma writes like(john, cats) to CI.

Equations

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

def GiorgoloAsudeh2012.sentence : TwoChannel CIProp PresupProp Bool

Full sentence (example 20): also(likes)(dogs)(john_who_likes_cats)

Equations

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

Figure 1's result: ⟨⟨like(j, dogs), {like(j, cats)}⟩, {∃z.like(j,z) ∧ z ≠ dogs}⟩

theorem GiorgoloAsudeh2012.sentence_atIssue : sentence.val = true

At-issue: like(john, dogs) = true.

theorem GiorgoloAsudeh2012.sentence_ci : sentence.ciLog = [CIProp.likes E.john E.cats]

CI log: {like(john, cats)} from the NRRC via write.

theorem GiorgoloAsudeh2012.sentence_presup : sentence.presupLog = [PresupProp.existsOtherLiked E.john E.dogs]

Presupposition log: {∃z.like(john,z) ∧ z ≠ dogs} from also via check.

Post-compositionally, both logs are exposed. CI content and presuppositional conditions are evaluated against the model.

theorem GiorgoloAsudeh2012.ci_true_in_model : sentence.ciLog.all CIProp.eval = true

All CI content is true in the model.

theorem GiorgoloAsudeh2012.presup_satisfied : sentence.presupLog.all PresupProp.eval = true

All presuppositions are satisfied in the model.

theorem GiorgoloAsudeh2012.ci_witnesses_presup : (sentence.ciLog.any fun (ci : CIProp) => match ci with | CIProp.likes subj obj => like subj obj && !obj == E.dogs) = true

The CI log provides the witness for presupposition satisfaction.

The NRRC logs like(john, cats). Since like(john, cats) = true and cats ≠ dogs, the presupposition ∃z. like(john, z) ∧ z ≠ dogs is witnessed. This is the paper's central empirical point: the presupposition of "also" is satisfied by CI content from the NRRC, but this satisfaction is only computable post-compositionally (the log produced by write cannot be examined before the monadic computation terminates).

Why the Writer monad enforces dimensional separation

The function in bind has type A → TwoChannel CI Presup B, not TwoChannel CI Presup A → TwoChannel CI Presup B. It receives the value stripped of both logs. This means:

• At-issue → CI (allowed): The comma operator receives john (the value) and uses it to construct CI content like(john, cats).

• CI → at-issue (blocked): When also applies the verb, the function receives only x = john, f = likes, y = dogs. It cannot see that the CI log contains like(john, cats).

• Presup → at-issue (blocked): Similarly, presuppositional conditions logged by check are invisible to subsequent at-issue computation.

This structural separation IS Potts's restriction, enforced by the type system rather than stipulated as a constraint on derivations.

def GiorgoloAsudeh2012.sentence_alt_nrrc : TwoChannel CIProp PresupProp Bool

Changing the NRRC content does not affect the at-issue result: the main clause function sees only the value, never the CI log.

Equations

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

theorem GiorgoloAsudeh2012.flow_restriction : sentence.val = sentence_alt_nrrc.val

CI-contributing expressions modeled by the Writer monad — expressives, appositives, NRRCs — are exactly Class B in @cite{tonhauser-beaver-roberts-simons-2013}'s taxonomy: SCF=no (CI content can be informative), OLE=no (attributed to speaker, not attitude holder). The Writer's log threading captures this: content projects past all operators without requiring prior establishment in context.

theorem GiorgoloAsudeh2012.nrrc_is_classB : Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.nrrc.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classB

theorem GiorgoloAsudeh2012.appositive_is_classB : Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.appositive.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classB

theorem GiorgoloAsudeh2012.expressive_is_classB : Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.expressive.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classB

theorem GiorgoloAsudeh2012.classB_properties : Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classB.scf = Phenomena.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires ∧ Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classB.ole = Phenomena.Presupposition.ProjectiveContent.ObligatoryLocalEffect.notObligatory

Class B = SCF=no, OLE=no: the behavior the Writer monad models.

For intensional models where values and log entries are world-indexed propositions, the CI channel maps directly to @cite{potts-2005}'s TwoDimProp. The presupposition channel is orthogonal.

def GiorgoloAsudeh2012.twoChannelToTwoDim {W : Type u_1} (m : TwoChannel (W → Prop) (W → Prop) (W → Prop)) : Pragmatics.Expressives.TwoDimProp W

Project the CI channel to a TwoDimProp. The at-issue value becomes atIssue; the conjoined CI log becomes ci. Presuppositional content is discarded (it lives in a separate dimension).

Equations

• GiorgoloAsudeh2012.twoChannelToTwoDim m = { atIssue := m.val, ci := fun (w : W) => ∀ p ∈ m.ciLog, p w }

theorem GiorgoloAsudeh2012.bridge_preserves_atIssue {W : Type u_1} (m : TwoChannel (W → Prop) (W → Prop) (W → Prop)) : (twoChannelToTwoDim m).atIssue = m.val

Structural correspondence to PostSupp

PostSupp S A (@cite{charlow-2021}) is structurally identical to a single Writer monad: a value paired with accumulated side-effect content, composed via pure/bind with log sequencing via dseq. The Writer monad for CIs and Charlow's PostSupp for modified numerals are the same pattern applied to different side-effects (CI propositions vs cardinality tests), confirming @cite{shan-2001}'s insight that monads capture recurring compositional structure in natural language.