Giorgolo and Asudeh (2012): ⟨M, η, ⋆⟩ Monads for Conventional Implicatures

Giorgolo and Asudeh treat conventional implicature as the side effect of a Writer monad: an expression denotes a computation that yields its at-issue value and logs the side-issue propositions of its parts. Since bind passes its continuation only the value and only extends the log, no lexical item can read or revise the side-issue dimension, as Potts's restriction on the flow of information demands and as the impossible modifier negex of Barker, Bernardi and Shan would. Presupposition triggers log their conditions in a second Writer layer. In "John, who likes cats, likes dogs also" the implicature entails the presupposition once the computation has ended, which is the paper's reply to the case of AnderBois, Brasoveanu and Henderson against multidimensionality.

Main definitions

• M: the two-channel monad, conventional implicatures over presuppositions.
• write, check: logging an implicature and a presuppositional condition.

Main results

• seq_eq_bind_bind: Shan's application (15) is the monad's <*>.
• Ex20.atIssue_sentence, Ex20.ciLog_sentence, Ex20.presupLog_sentence: the three dimensions of Figure 1.
• Ex20.presupposition_of_ci: the implicature entails the presupposition.
• Ex20.atIssue_sentence_congr: the relative clause never reaches the at-issue value.

Implementation notes

• The two channels are the transformer WriterT (List CI) (Writer (List Presup)), over the Writer surface of Semantics/Composition/Writer.lean, with check lifted from the presupposition monad as fn. 4 prescribes. The paper's logs are sets under union; these are lists.
• Glue's ⊸ elimination is the monad's <*>, and ⊸* elimination plain application to monadic arguments; the introduction rules, which reason hypothetically, are not needed.
• The extension of like is a parameter: the presupposition of also follows from the logged implicature alone, given that cats are not dogs.

References

• [GA12]
• [Sha01]
• [Pot05]
• [ABBH10]
• [BBS10]

The two channels

@[reducible, inline]

abbrev GiorgoloAsudeh2012.M (CI Presup α : Type u) : Type u

The two-channel monad logs conventional implicatures in the transformer and presuppositional conditions in the monad it transforms, so that a computation's result is the paper's ⟨⟨value, implicatures⟩, presuppositions⟩.

Equations

• GiorgoloAsudeh2012.M CI Presup = WriterT (List CI) (Writer (List Presup))

def GiorgoloAsudeh2012.atIssue {CI Presup A : Type u} (m : M CI Presup A) : A

The at-issue value of a computation.

Equations

• GiorgoloAsudeh2012.atIssue m = (WriterT.run m).val.fst

def GiorgoloAsudeh2012.ciLog {CI Presup A : Type u} (m : M CI Presup A) : List CI

The conventional implicatures a computation logs.

Equations

• GiorgoloAsudeh2012.ciLog m = (WriterT.run m).val.snd

def GiorgoloAsudeh2012.presupLog {CI Presup A : Type u} (m : M CI Presup A) : List Presup

The presuppositional conditions a computation logs.

Equations

• GiorgoloAsudeh2012.presupLog m = (WriterT.run m).log

def GiorgoloAsudeh2012.write {CI Presup : Type u} (p : CI) : M CI Presup PUnit

write t logs the conventional implicature t, the paper's write(t) = ⟨⊥, {t}⟩.

Equations

• GiorgoloAsudeh2012.write p = tell [p]

def GiorgoloAsudeh2012.check {CI Presup : Type u} (p : Presup) : M CI Presup PUnit

check t logs a condition to be checked once the computation has ended, lifted from the presupposition monad as the paper's fn. 4 prescribes.

Equations

• GiorgoloAsudeh2012.check p = monadLift (tell [p])

@[simp]

theorem GiorgoloAsudeh2012.atIssue_pure {CI Presup A : Type u} (a : A) : atIssue (pure a) = a

@[simp]

theorem GiorgoloAsudeh2012.ciLog_pure {CI Presup A : Type u} (a : A) : ciLog (pure a) = []

@[simp]

theorem GiorgoloAsudeh2012.presupLog_pure {CI Presup A : Type u} (a : A) : presupLog (pure a) = []

@[simp]

theorem GiorgoloAsudeh2012.atIssue_bind {CI Presup A B : Type u} (m : M CI Presup A) (f : A → M CI Presup B) : atIssue (m >>= f) = atIssue (f (atIssue m))

@[simp]

theorem GiorgoloAsudeh2012.ciLog_bind {CI Presup A B : Type u} (m : M CI Presup A) (f : A → M CI Presup B) : ciLog (m >>= f) = ciLog m ++ ciLog (f (atIssue m))

@[simp]

theorem GiorgoloAsudeh2012.presupLog_bind {CI Presup A B : Type u} (m : M CI Presup A) (f : A → M CI Presup B) : presupLog (m >>= f) = presupLog m ++ presupLog (f (atIssue m))

@[simp]

theorem GiorgoloAsudeh2012.ciLog_write {CI Presup : Type u} (p : CI) : ciLog (write p) = [p]

@[simp]

theorem GiorgoloAsudeh2012.presupLog_write {CI Presup : Type u} (p : CI) : presupLog (write p) = []

@[simp]

theorem GiorgoloAsudeh2012.ciLog_check {CI Presup : Type u} (p : Presup) : ciLog (check p) = []

@[simp]

theorem GiorgoloAsudeh2012.presupLog_check {CI Presup : Type u} (p : Presup) : presupLog (check p) = [p]

theorem GiorgoloAsudeh2012.ciLog_prefix_bind {CI Presup A B : Type u} (m : M CI Presup A) (f : A → M CI Presup B) : ciLog m <+: ciLog (m >>= f)

The side-issue log is only extended, so no item can revise an implicature already logged.

Shan's application

Glue's ⊸ elimination composes at-issue items by Shan's application (15), A(f)(x) = f ⋆ λg. x ⋆ λy. η(g y), which is the monad's <*>; the value is the application and both logs are threaded.

theorem GiorgoloAsudeh2012.seq_eq_bind_bind {CI Presup A B : Type u} (f : M CI Presup (A → B)) (x : M CI Presup A) : f <*> x = do let g ← f let y ← x pure (g y)

Shan's application (15) is the monad's <*>.

@[simp]

theorem GiorgoloAsudeh2012.atIssue_seq {CI Presup A B : Type u} (f : M CI Presup (A → B)) (x : M CI Presup A) : atIssue (f <*> x) = atIssue f (atIssue x)

@[simp]

theorem GiorgoloAsudeh2012.ciLog_seq {CI Presup A B : Type u} (f : M CI Presup (A → B)) (x : M CI Presup A) : ciLog (f <*> x) = ciLog f ++ ciLog x

@[simp]

theorem GiorgoloAsudeh2012.presupLog_seq {CI Presup A B : Type u} (f : M CI Presup (A → B)) (x : M CI Presup A) : presupLog (f <*> x) = presupLog f ++ presupLog x

"John, who likes cats, likes dogs also" (20)

inductive GiorgoloAsudeh2012.Ex20.E : Type

John, the cats and the dogs.

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

@[instance_reducible]

instance GiorgoloAsudeh2012.Ex20.instDecidableEqE : DecidableEq E

Equations

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

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

Equations

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

@[instance_reducible]

instance GiorgoloAsudeh2012.Ex20.instReprE : Repr E

Equations

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

def GiorgoloAsudeh2012.Ex20.comma (j : M Prop Prop E) (l : M Prop Prop (E → Prop)) : M Prop Prop E

The prosodic element comma of Table 1, λj λl. j ⋆ λx. l ⋆ λf. write(f x) ⋆ λ_. η(x), introduces the non-restrictive relative clause; it logs the clause's content about its anchor and returns the anchor.

Equations

• GiorgoloAsudeh2012.Ex20.comma j l = do let x ← j let f ← l GiorgoloAsudeh2012.write (f x) pure x

def GiorgoloAsudeh2012.Ex20.also (v : M Prop Prop (E → E → Prop)) (o s : M Prop Prop E) : M Prop Prop Prop

The presupposition trigger also of Table 1, λv λo λs. s ⋆ λx. v ⋆ λf. o ⋆ λy. check(∃z. f z x ∧ z ≠ y) ⋆ λ_. η(f y x), logs the presupposition that the subject bears the relation to something other than the object and returns the at-issue proposition.

Equations

• GiorgoloAsudeh2012.Ex20.also v o s = do let x ← s let f ← v let y ← o GiorgoloAsudeh2012.check (∃ (z : GiorgoloAsudeh2012.Ex20.E), f z x ∧ z ≠ y) pure (f y x)

def GiorgoloAsudeh2012.Ex20.john : M Prop Prop E

The at-issue items of Table 1, η-lifted.

Equations

• GiorgoloAsudeh2012.Ex20.john = pure GiorgoloAsudeh2012.Ex20.E.john

def GiorgoloAsudeh2012.Ex20.who : M Prop Prop ((E → Prop) → E → Prop)

Equations

• GiorgoloAsudeh2012.Ex20.who = pure id

def GiorgoloAsudeh2012.Ex20.likes (like : E → E → Prop) : M Prop Prop (E → E → Prop)

Equations

• GiorgoloAsudeh2012.Ex20.likes like = pure fun (y x : GiorgoloAsudeh2012.Ex20.E) => like x y

def GiorgoloAsudeh2012.Ex20.cats : M Prop Prop E

Equations

• GiorgoloAsudeh2012.Ex20.cats = pure GiorgoloAsudeh2012.Ex20.E.cats

def GiorgoloAsudeh2012.Ex20.dogs : M Prop Prop E

Equations

• GiorgoloAsudeh2012.Ex20.dogs = pure GiorgoloAsudeh2012.Ex20.E.dogs

def GiorgoloAsudeh2012.Ex20.whoLikesCats (like : E → E → Prop) : M Prop Prop (E → Prop)

"who likes cats", by ⊸ elimination.

Equations

• GiorgoloAsudeh2012.Ex20.whoLikesCats like = GiorgoloAsudeh2012.Ex20.who <*> (GiorgoloAsudeh2012.Ex20.likes like <*> GiorgoloAsudeh2012.Ex20.cats)

def GiorgoloAsudeh2012.Ex20.sentence (like : E → E → Prop) : M Prop Prop Prop

The sentence, by ⊸* elimination.

Equations

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

theorem GiorgoloAsudeh2012.Ex20.atIssue_sentence (like : E → E → Prop) : atIssue (sentence like) = like E.john E.dogs

The at-issue proposition of Figure 1 is that John likes dogs.

theorem GiorgoloAsudeh2012.Ex20.ciLog_sentence (like : E → E → Prop) : ciLog (sentence like) = [like E.john E.cats]

The side-issue log of Figure 1 holds that John likes cats.

theorem GiorgoloAsudeh2012.Ex20.presupLog_sentence (like : E → E → Prop) : presupLog (sentence like) = [∃ (z : E), like E.john z ∧ z ≠ E.dogs]

The presupposition of also in Figure 1 is that John likes something other than the dogs.

theorem GiorgoloAsudeh2012.Ex20.presupposition_of_ci (like : E → E → Prop) (h : ∀ (q : Prop), q ∈ ciLog (sentence like) → q) (p : Prop) : p ∈ presupLog (sentence like) → p

Once both logs are exposed, the conventional implicature entails the presupposition, since John likes cats and cats are not dogs.

theorem GiorgoloAsudeh2012.Ex20.atIssue_sentence_congr (like : E → E → Prop) (l l' : M Prop Prop (E → Prop)) : atIssue (also (likes like) dogs (comma john l)) = atIssue (also (likes like) dogs (comma john l'))

The relative clause never reaches the at-issue dimension, since whatever it says, the sentence's at-issue value is that John likes dogs.