Continuation semantics

Starting with Philippe de Groote's work, a rich literature in formal semantics has developed which relies on continuation passing to model the truth-conditional contributions of quantifiers, like some dog and every linguist. Since de Groote's analysis, most work has focused on what are known as delimited or composable continuations; in particular, Chris Barker and Ken Shan's work (e.g., check out their 2014 book, but also Barker 2003 for something a little shorter). Composable continuations have some fixed result type, so that the meanings of natural language expressions can be modeled as functions of type \((α → o) → o\) (for some \(o\)). For example, one can model the meaning of quantifiers by choosing \(o\) to be \(t\) (the type of extensional propositions), and assigning, e.g., some dog the interpretation \[λk.∃x : dog(x) ∧ k(x)\] which is of type \((e → t) → t\). Meanwhile, other, non-quantificational expressions can be assigned meanings that use their continuation trivially, that is, by feeding themselves to it. For example, barks can be assigned the interpretation \[λk.k(bark)\] which is of type \(((e → t) → t) → t\). It takes some continuation of type \((e → t) → t\) and feeds it the property \(bark\) (of type \(e → t\)). To compose the meaning of some dog with the meaning of barks, we may used continuized (barkward) functional application:¹ \[⟦\textit{some dog}⟧ ◃ ⟦\textit{barks}⟧ =\] \[λk.⟦\textit{some dog}⟧(λx.⟦\textit{barks}⟧(λf.k(f(x)))) =\] \[λk.(λk^\prime.∃y : dog(x) ∧ k^\prime(y))(λx.(λk^\prime.k^\prime(bark))(λf.k(f(x)))) →_β^*\] \[λk.(λk^\prime.∃y : dog(y) ∧ k^\prime(y))(λx.k(bark(x))) →_β^*\] \[λk.∃y : dog(y) ∧ k(bark(y))\] Having obtained a continuized meaning for the entire sentence, we can lower it to a value of type \(t\) by feeding it the identity function: \[(λk.∃y : dog(y) ∧ k(bark(y)))(λb.b) →_β^* ∃y : dog(y) ∧ bark(y)\]

Recall our type family SemType, which takes grammatical categories of applicative categorial grammar onto types of the λ-calculus:

type family SemType (c :: Cat) where
  SemType NP = E
  SemType N = E :-> T
  SemType S = T
  SemType (c1 :\: c2) = SemType c1 :-> SemType c2
  SemType (c2 :/: c1) = SemType c1 :-> SemType c2

In terms of this map, we may implement a function interpExpr, which takes expressions of English onto λ-terms of continuized types. Rather than map an expression of category c directly onto its semantic type, we map it onto a closed term of type (SemType c :-> T) :-> T, using continuized functional application:

interpExpr :: Expr c -> Term Empty ((SemType c :-> T) :-> T)
interpExpr (Lex w) = interpWord w
interpExpr (AppL e1 e2) = Lam (App (weaken (interpExpr e1)) (Lam (App (weaken (weaken (interpExpr e2))) (Lam (App (Var (Next (Next First))) (App (Var First) (Var (Next First))))))))
interpExpr (AppR e1 e2) = Lam (App (weaken (interpExpr e1)) (Lam (App (weaken (weaken (interpExpr e2))) (Lam (App (Var (Next (Next First))) (App (Var (Next First)) (Var First)))))))

To interpret individual words (though note that we're considering some dog a word for our purposes - try to think about what difficulties we encounter if we try to compose every with dog using our current system), we may write a function interpWord taking words of some category c onto closed terms of type (SemType c :-> T) :-> T:

interpWord :: Word c -> Term Empty ((SemType c :-> T) :-> T)
interpWord (Word "some dog" IsAnNP) = Lam (App (Con Exists) (Lam (App (App (Con And) (App (Con Dog) (Var First))) (App (Var (Next First)) (Var First)))))
interpWord (Word "barks" (IsAnNP ::\:: IsAnS)) = Lam (App (Var First) (Con Bark))

Note that for this to be well typed, our constants should have the following types:

data Constant (φ :: Type) where
  Exists :: Constant ((E :-> T) :-> T)
  And :: Constant (T :-> (T :-> T))
  Dog :: Constant (E :-> T)
  Bark :: Constant (E :-> T)